Fibers of a functor

This files define the type Fiber of a functor at a given object in the base category.

We provide the category instance on the fibers of a functor. We show that for a functor P, the fiber of the opposite functor P.op are isomorphic to the opposites of the fiber categories of P.

Notation

We provide the following notations:

• P ⁻¹ I for the fiber of functor P at I.

def CategoryTheory.Fiber {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] (P : Functor E C) (I : C) : Type u_2

The fiber of a functor at a given object in the codomain category.

Equations

• (P ⁻¹ I) = { X : E // P.obj X = I }

structure CategoryTheory.EFiber {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] (P : Functor E C) (I : C) : Type (max u_2 u_3)

The essential fiber of a functor at a given object in the codomain category.

• obj : E
• iso : P.obj self.obj ≅ I

structure CategoryTheory.LaxFiber {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] (P : Functor E C) (I : C) : Type (max u_2 u_3)

The lax fiber of a functor at a given object in the codomain category.

• obj : E
• from_base : I ⟶ P.obj self.obj

def CategoryTheory.Fiber_stx : Lean.TrailingParserDescr

Equations

• CategoryTheory.Fiber_stx = Lean.ParserDescr.trailingNode `CategoryTheory.Fiber_stx 75 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹ ") (Lean.ParserDescr.cat `term 0))

def CategoryTheory.EFiber_stx : Lean.TrailingParserDescr

Equations

• CategoryTheory.EFiber_stx = Lean.ParserDescr.trailingNode `CategoryTheory.EFiber_stx 75 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹ᵉ ") (Lean.ParserDescr.cat `term 0))

def CategoryTheory.LaxFiber_stx : Lean.TrailingParserDescr

Equations

• CategoryTheory.LaxFiber_stx = Lean.ParserDescr.trailingNode `CategoryTheory.LaxFiber_stx 75 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹ˡ ") (Lean.ParserDescr.cat `term 0))

theorem CategoryTheory.Fiber.ext {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (X Y : P ⁻¹ I) (h : ↑X = ↑Y) : X = Y

theorem CategoryTheory.Fiber.ext_iff {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} {X Y : P ⁻¹ I} : X = Y ↔ ↑X = ↑Y

instance CategoryTheory.Fiber.instCoeOut {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} : CoeOut (P ⁻¹ I) E

Coercion from the fiber to the domain.

Equations

• CategoryTheory.Fiber.instCoeOut = { coe := fun (x : P ⁻¹ I) => ↑x }

theorem CategoryTheory.Fiber.coe_mk {C : Type u_1} {E : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} E] {P : Functor E C} {I : C} {X : E} (h : P.obj X = I) : ↑⟨X, h⟩ = X

theorem CategoryTheory.Fiber.mk_coe {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} {X : P ⁻¹ I} : ⟨↑X, ⋯⟩ = X

theorem CategoryTheory.Fiber.coe_inj {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (X Y : P ⁻¹ I) : ↑X = ↑Y ↔ X = Y

theorem CategoryTheory.Fiber.over {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (X : P ⁻¹ I) : P.obj ↑X = I

theorem CategoryTheory.Fiber.over_eq {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (X Y : P ⁻¹ I) : P.obj ↑X = P.obj ↑Y

def CategoryTheory.Fiber.tauto {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (X : E) : P ⁻¹ P.obj X

A tautological construction of an element in the fiber of the image of a domain element.

Equations

• CategoryTheory.Fiber.tauto X = ⟨X, ⋯⟩

instance CategoryTheory.Fiber.instTautoFib {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (X : E) : CoeDep E X (P ⁻¹ P.obj X)

Regarding an element of the domain as an element in the Fiber of its image.

Equations

• CategoryTheory.Fiber.instTautoFib X = { coe := CategoryTheory.Fiber.tauto X }

theorem CategoryTheory.Fiber.tauto_over {C : Type u_1} {E : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} E] {P : Functor E C} (X : E) : ↑(tauto X) = X

structure CategoryTheory.Fiber.Total {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} : Type (max u_1 u_2)

The total space of a map.

• base : C

  The base object in C

• fiber : P ⁻¹ self.base

  The object in the fiber of the base object.

theorem CategoryTheory.Fiber.Total.ext_iff {C : Type u_1} {E : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} E} {P : Functor E C} {x y : Total} : x = y ↔ x.base = y.base ∧ HEq x.fiber y.fiber

theorem CategoryTheory.Fiber.Total.ext {C : Type u_1} {E : Type u_2} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Category.{u_4, u_2} E} {P : Functor E C} {x y : Total} (base : x.base = y.base) (fiber : HEq x.fiber y.fiber) : x = y

instance CategoryTheory.Fiber.category {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} : Category.{u_4, u_2} (P ⁻¹ I)

The category structure on the fibers of a functor.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Fiber.id_coe {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (X : P ⁻¹ I) : ↑(CategoryStruct.id X) = CategoryStruct.id ↑X

theorem CategoryTheory.Fiber.comp_coe {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {c : C} {X Y Z : P ⁻¹ c} (f : X ⟶ Y) (g : Y ⟶ Z) : ↑(CategoryStruct.comp f g) = CategoryStruct.comp ↑f ↑g

@[simp]

theorem CategoryTheory.Fiber.fiber_hom_over {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (X Y : P ⁻¹ I) (g : X ⟶ Y) : P.map ↑g = eqToHom ⋯

def CategoryTheory.Fiber.forget {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} : Functor (P ⁻¹ I) E

The forgetful functor from a fiber to the domain category.

Equations

• CategoryTheory.Fiber.forget = { obj := fun (x : P ⁻¹ I) => ↑x, map := fun (x y : P ⁻¹ I) (f : x ⟶ y) => ↑f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Fiber.forget_map {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (x y : P ⁻¹ I) (f : x ⟶ y) : forget.map f = ↑f

@[simp]

theorem CategoryTheory.Fiber.forget_obj {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (x : P ⁻¹ I) : forget.obj x = ↑x

theorem CategoryTheory.Fiber.fiber_comp_obj {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {c : C} (X Y Z : P ⁻¹ c) (f : X ⟶ Y) (g : Y ⟶ Z) : ↑(CategoryStruct.comp f g) = CategoryStruct.comp ↑f ↑g

@[simp]

theorem CategoryTheory.Fiber.fiber_comp_obj_eq {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {c : C} {X Y Z : P ⁻¹ c} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} : CategoryStruct.comp f g = h ↔ CategoryStruct.comp ↑f ↑g = ↑h

@[simp]

theorem CategoryTheory.Fiber.fiber_id_obj {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (X : P ⁻¹ I) : ↑(CategoryStruct.id X) = CategoryStruct.id ↑X

theorem CategoryTheory.Fiber.hom_ext {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} {X Y : P ⁻¹ I} {f g : X ⟶ Y} (h : ↑f = ↑g) : f = g

theorem CategoryTheory.Fiber.is_iso {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} {X Y : P ⁻¹ I} (f : X ⟶ Y) : IsIso f ↔ IsIso ↑f

instance CategoryTheory.EFiber.instCoeOut {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} : CoeOut (P ⁻¹ᵉ I) E

Coercion from the fiber to the domain.

Equations

• CategoryTheory.EFiber.instCoeOut = { coe := fun (X : P ⁻¹ᵉ I) => X.obj }

def CategoryTheory.EFiber.tauto {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (X : E) : P ⁻¹ᵉ P.obj X

A tautological construction of an element in the fiber of the image of a domain element.

Equations

• CategoryTheory.EFiber.tauto X = { obj := X, iso := CategoryTheory.Iso.refl (P.obj X) }

@[simp]

theorem CategoryTheory.EFiber.tauto_obj {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (X : E) : (tauto X).obj = X

@[simp]

theorem CategoryTheory.EFiber.tauto_iso_hom {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (X : E) : (tauto X).iso.hom = CategoryStruct.id (P.obj X)

@[simp]

theorem CategoryTheory.EFiber.tauto_iso_inv {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (X : E) : (tauto X).iso.inv = CategoryStruct.id (P.obj X)

instance CategoryTheory.EFiber.instTautoFib {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (X : E) : CoeDep E X (P ⁻¹ᵉ P.obj X)

Regarding an element of the domain as an element in the essential fiber of its image.

Equations

• CategoryTheory.EFiber.instTautoFib X = { coe := CategoryTheory.EFiber.tauto X }

instance CategoryTheory.EFiber.category {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} : Category.{u_4, max u_3 u_2} (P ⁻¹ᵉ I)

The category structure on the essential fibers of a functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Fiber.Op.obj_over {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} (X : P.op ⁻¹ Opposite.op I) : P.obj (Opposite.unop ↑X) = I

def CategoryTheory.Fiber.Op.equiv {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (I : C) : (P.op ⁻¹ Opposite.op I) ≃ P ⁻¹ I

The Fibers of the opposite functor P.op are in bijection with the the Fibers of P.

Equations

• CategoryTheory.Fiber.Op.equiv I = { toFun := fun (X : P.op ⁻¹ Opposite.op I) => ⟨Opposite.unop ↑X, ⋯⟩, invFun := fun (X : P ⁻¹ I) => ⟨Opposite.op ↑X, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.Fiber.Op.equiv_apply_coe {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (I : C) (X : P.op ⁻¹ Opposite.op I) : ↑((equiv I) X) = Opposite.unop ↑X

@[simp]

theorem CategoryTheory.Fiber.Op.equiv_symm_apply_coe {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (I : C) (X : P ⁻¹ I) : ↑((equiv I).symm X) = Opposite.op ↑X

def CategoryTheory.Fiber.Op.iso {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (I : C) : (P.op ⁻¹ Opposite.op I) ≅ P ⁻¹ I

The Fibers of the opposite functor P.op are isomorphic to the the Fibers of P.

Equations

• CategoryTheory.Fiber.Op.iso I = { hom := fun (X : P.op ⁻¹ Opposite.op I) => ⟨Opposite.unop ↑X, ⋯⟩, inv := fun (X : P ⁻¹ I) => ⟨Opposite.op ↑X, ⋯⟩, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Fiber.Op.iso_inv_coe {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (I : C) (X : P ⁻¹ I) : ↑((iso I).inv X) = Opposite.op ↑X

@[simp]

theorem CategoryTheory.Fiber.Op.iso_hom_coe {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} (I : C) (X : P.op ⁻¹ Opposite.op I) : ↑((iso I).hom X) = Opposite.unop ↑X

theorem CategoryTheory.Fiber.Op.unop_op_map {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} {X Y : P.op ⁻¹ Opposite.op I} (f : X ⟶ Y) : Opposite.unop (P.op.map ↑f) = P.map (↑f).unop

theorem CategoryTheory.Fiber.Op.op_map_unop {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] {P : Functor E C} {I : C} {X Y : (P ⁻¹ I)ᵒᵖ} (f : X ⟶ Y) : P.op.map (↑f.unop).op = (P.map ↑f.unop).op

def CategoryTheory.Fiber.Op.Iso {C : Type u_1} {E : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} E] (P : Functor E C) (I : C) : Cat.of (P.op ⁻¹ Opposite.op I) ≅ Cat.of (P ⁻¹ I)ᵒᵖ

The fiber categories of the opposite functor P.op are isomorphic to the opposites of the fiber categories of P.

Equations

• One or more equations did not get rendered due to their size.