Basic

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.

We provide the following notations:

• P ⁻¹ c for the fiber of P at c.

@[reducible, inline]

abbrev CategoryTheory.FiberCat {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) (c : C) : Type u_2

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

Equations

• (P ⁻¹ c) = Fiber P.obj c

def CategoryTheory.FiberCat_stx : Lean.TrailingParserDescr

Equations

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

instance CategoryTheory.FiberCat.instCategoryFiber {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} : CategoryTheory.Category.{u_4, u_2} (P ⁻¹ c)

The category structure on the fibers of a functor.

Equations

• CategoryTheory.FiberCat.instCategoryFiber = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

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

@[simp]

theorem CategoryTheory.FiberCat.fiber_hom_over {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} (x : P ⁻¹ c) (y : P ⁻¹ c) (g : x ⟶ y) : P.map ↑g = CategoryTheory.eqToHom ⋯

@[simp]

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

@[simp]

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

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

The forgetful functor from a fiber to the domain category.

Equations

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

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.FiberCat.hom_ext {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {x : P ⁻¹ c} {y : P ⁻¹ c} {f : x ⟶ y} {g : x ⟶ y} (h : ↑f = ↑g) : f = g

theorem CategoryTheory.FiberCat.is_iso {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {x : P ⁻¹ c} {y : P ⁻¹ c} (f : x ⟶ y) : CategoryTheory.IsIso f ↔ CategoryTheory.IsIso ↑f

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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.