Fibers of a functors

In this file we define, for a functor p : 𝒳 ⥤ 𝒴, the fiber categories Fiber p S for every S : 𝒮 as follows

• An object in Fiber p S is a pair (a, ha) where a : 𝒳 and ha : p.obj a = S.
• A morphism in Fiber p S is a morphism φ : a ⟶ b in 𝒳 such that p.map φ = 𝟙 S.

For any category C equipped with a functor F : C ⥤ 𝒳 such that F ⋙ p is constant at S, we define a functor inducedFunctor : C ⥤ Fiber p S that F factors through.

def CategoryTheory.Functor.Fiber {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) (S : 𝒮) : Type u₂

Fiber p S is the type of elements of 𝒳 mapping to S via p.

instance CategoryTheory.Functor.Fiber.fiberCategory {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} : Category.{v₂, u₂} (p.Fiber S)

Fiber p S has the structure of a category with morphisms being those lying over 𝟙 S.

def CategoryTheory.Functor.Fiber.fiberInclusion {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} : Functor (p.Fiber S) 𝒳

The functor including Fiber p S into 𝒳.

instance CategoryTheory.Functor.Fiber.instIsHomLiftIdMapFiberInclusion {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {a b : p.Fiber S} (φ : a ⟶ b) : p.IsHomLift (CategoryStruct.id S) (fiberInclusion.map φ)

theorem CategoryTheory.Functor.Fiber.hom_ext {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {a b : p.Fiber S} {φ ψ : a ⟶ b} (h : fiberInclusion.map φ = fiberInclusion.map ψ) : φ = ψ

theorem CategoryTheory.Functor.Fiber.hom_ext_iff {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {a b : p.Fiber S} {φ ψ : a ⟶ b} : φ = ψ ↔ fiberInclusion.map φ = fiberInclusion.map ψ

instance CategoryTheory.Functor.Fiber.instFaithfulFiberInclusion {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} : fiberInclusion.Faithful

theorem CategoryTheory.Functor.Fiber.fiberInclusion_obj_inj {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} : Function.Injective fiberInclusion.obj

def CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} : fiberInclusion.comp p ≅ (const (p.Fiber S)).obj S

For fixed S : 𝒮 this is the natural isomorphism between fiberInclusion ⋙ p and the constant function valued at S.

@[simp]

theorem CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst_hom_app {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} (X : p.Fiber S) : fiberInclusionCompIsoConst.hom.app X = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst_inv_app {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} (X : p.Fiber S) : fiberInclusionCompIsoConst.inv.app X = eqToHom ⋯

theorem CategoryTheory.Functor.Fiber.fiberInclusion_comp_eq_const {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} : fiberInclusion.comp p = (const (p.Fiber S)).obj S

def CategoryTheory.Functor.Fiber.mk {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {a : 𝒳} (ha : p.obj a = S) : p.Fiber S

The object of the fiber over S corresponding to a a : 𝒳 such that p(a) = S.

@[simp]

theorem CategoryTheory.Functor.Fiber.fiberInclusion_mk {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {a : 𝒳} (ha : p.obj a = S) : fiberInclusion.obj (mk ha) = a

def CategoryTheory.Functor.Fiber.homMk {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) (S : 𝒮) {a b : 𝒳} (φ : a ⟶ b) [p.IsHomLift (CategoryStruct.id S) φ] : mk ⋯ ⟶ mk ⋯

The morphism in the fiber over S corresponding to a morphism in 𝒳 lifting 𝟙 S.

@[simp]

theorem CategoryTheory.Functor.Fiber.fiberInclusion_homMk {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) (S : 𝒮) {a b : 𝒳} (φ : a ⟶ b) [p.IsHomLift (CategoryStruct.id S) φ] : fiberInclusion.map (homMk p S φ) = φ

@[simp]

theorem CategoryTheory.Functor.Fiber.homMk_id {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) (S : 𝒮) (a : 𝒳) [p.IsHomLift (CategoryStruct.id S) (CategoryStruct.id a)] : homMk p S (CategoryStruct.id a) = CategoryStruct.id (mk ⋯)

@[simp]

theorem CategoryTheory.Functor.Fiber.homMk_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c) [p.IsHomLift (CategoryStruct.id S) φ] [p.IsHomLift (CategoryStruct.id S) ψ] : CategoryStruct.comp (homMk p S φ) (homMk p S ψ) = homMk p S (CategoryStruct.comp φ ψ)

def CategoryTheory.Functor.Fiber.inducedFunctor {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor C 𝒳} (hF : F.comp p = (const C).obj S) : Functor C (p.Fiber S)

Given a functor F : C ⥤ 𝒳 such that F ⋙ p is constant at some S : 𝒮, then we get an induced functor C ⥤ Fiber p S that F factors through.

def CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor C 𝒳} (hF : F.comp p = (const C).obj S) : (inducedFunctor hF).comp fiberInclusion ≅ F

Given a functor F : C ⥤ 𝒳 such that F ⋙ p is constant at some S : 𝒮, then we get a natural isomorphism between inducedFunctor _ ⋙ fiberInclusion and F.

@[simp]

theorem CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf_inv_app {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor C 𝒳} (hF : F.comp p = (const C).obj S) (X : C) : (inducedFunctorCompIsoSelf hF).inv.app X = CategoryStruct.id (fiberInclusion.obj ((inducedFunctor hF).obj X))

@[simp]

theorem CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf_hom_app {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor C 𝒳} (hF : F.comp p = (const C).obj S) (X : C) : (inducedFunctorCompIsoSelf hF).hom.app X = CategoryStruct.id (fiberInclusion.obj ((inducedFunctor hF).obj X))

theorem CategoryTheory.Functor.Fiber.inducedFunctor_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor C 𝒳} (hF : F.comp p = (const C).obj S) : (inducedFunctor hF).comp fiberInclusion = F

@[simp]

theorem CategoryTheory.Functor.Fiber.inducedFunctor_comp_obj {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor C 𝒳} (hF : F.comp p = (const C).obj S) (X : C) : fiberInclusion.obj ((inducedFunctor hF).obj X) = F.obj X

@[simp]

theorem CategoryTheory.Functor.Fiber.inducedFunctor_comp_map {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] {p : Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor C 𝒳} (hF : F.comp p = (const C).obj S) {X Y : C} (f : X ⟶ Y) : fiberInclusion.map ((inducedFunctor hF).map f) = F.map f