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₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) (S : 𝒮) : Type (max 0 u₂)

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

Equations

• p.Fiber S = { a : 𝒳 // p.obj a = S }

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

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

Equations

• CategoryTheory.Functor.Fiber.fiberCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

The functor including Fiber p S into 𝒳.

Equations

• CategoryTheory.Functor.Fiber.fiberInclusion = { obj := fun (a : p.Fiber S) => ↑a, map := fun {X Y : p.Fiber S} (φ : X ⟶ Y) => ↑φ, map_id := ⋯, map_comp := ⋯ }

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst = CategoryTheory.NatIso.ofComponents (fun (X : p.Fiber S) => CategoryTheory.eqToIso ⋯) ⋯

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

def CategoryTheory.Functor.Fiber.mk {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.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.

Equations

• CategoryTheory.Functor.Fiber.mk ha = ⟨a, ha⟩

@[simp]

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

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

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

Equations

• CategoryTheory.Functor.Fiber.homMk p S φ = ⟨φ, ⋯⟩

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Functor.Fiber.inducedFunctor hF = { obj := fun (x : C) => ⟨F.obj x, ⋯⟩, map := fun {X Y : C} (φ : X ⟶ Y) => ⟨F.map φ, ⋯⟩, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor C 𝒳} (hF : F.comp p = (CategoryTheory.Functor.const C).obj S) : (CategoryTheory.Functor.Fiber.inducedFunctor hF).comp CategoryTheory.Functor.Fiber.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.

Equations

• CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf hF = CategoryTheory.Iso.refl ((CategoryTheory.Functor.Fiber.inducedFunctor hF).comp CategoryTheory.Functor.Fiber.fiberInclusion)

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