Fibers of functors

In this file we introduce a typeclass HasFibers for a functor p : 𝒳 ⥤ 𝒮, consisting of:

• A collection of categories Fib S for every S in 𝒮 (the fiber categories)
• Functors ι : Fib S ⥤ 𝒳 such that `ι ⋙ p = const (Fib S) S
• The induced functor Fib S ⥤ Fiber p S is an equivalence.

We also provide a canonical HasFibers instance, which uses the standard fibers Fiber p S (see Fiber.lean). This makes it so that any result proven about HasFibers can be used for the standard fibers as well.

The reason for introducing this typeclass is that in practice, when working with (pre)fibered categories one often already has a collection of categories Fib S for every S that are equivalent to the fibers Fiber p S. One would then like to use these categories Fib S directly, instead of working through this equivalence of categories. By developing an API for the HasFibers typeclass, this will be possible.

Here is an example of when this typeclass is useful. Suppose we have a presheaf of types F : 𝒮ᵒᵖ ⥤ Type _. The associated fibered category then has objects (S, a) where S : 𝒮 and a is an element of F(S). The fiber category Fiber p S is then equivalent to the discrete category Fib S with objects a in F(S). In this case, the HasFibers instance is given by the categories F(S) and the functor ι sends a : F(S) to (S, a) in the fibered category.

Main API

The following API is developed so that the fibers from a HasFibers instance can be used analogously to the standard fibers.

• Fib.homMk φ is a lift of a morphism φ : (ι S).obj a ⟶ (ι S).obj b in 𝒳, which lies over 𝟙 S, to a morphism in the fiber over S.
• Fib.mk gives an object in the fiber over S which is isomorphic to a given a : 𝒳 that satisfies p(a) = S. The isomorphism is given by Fib.mkIsoSelf.
• HasFibers.mkPullback is a version of IsPreFibered.mkPullback which ensures that the object lies in a given fiber. The corresponding cartesian morphism is given by HasFibers.pullbackMap.
• HasFibers.inducedMap is a version of IsCartesian.inducedMap which gives the corresponding morphism in the fiber category.
• fiber_factorization is the statement that any morphism in 𝒳 can be factored as a morphism in some fiber followed by a pullback.

class HasFibers {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) : Type (max (max (max (max u₁ u₂) (u₃ + 1)) v₂) (v₃ + 1))

HasFibers is an extrinsic notion of fibers on a functor p : 𝒳 ⥤ 𝒮. It is given by a collection of categories Fib S for every S : 𝒮 (the fiber categories), each equipped with a functors ι : Fib S ⥤ 𝒳 which map constantly to S on the base such that the induced functor Fib S ⥤ Fiber p S is an equivalence.

• Fib (S : 𝒮) : Type u₃

  The type of objects of the category Fib S for each S.

• category (S : 𝒮) : CategoryTheory.Category.{v₃, u₃} (Fib p S)

  Fib S is a category.

• ι (S : 𝒮) : CategoryTheory.Functor (Fib p S) 𝒳

  The functor ι : Fib S ⥤ 𝒳.

• comp_const (S : 𝒮) : (ι S).comp p = (CategoryTheory.Functor.const (Fib p S)).obj S

  The composition with the functor p is equal to the constant functor mapping to S.

• equiv (S : 𝒮) : (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).IsEquivalence

  The induced functor from Fib S to the fiber of 𝒳 ⥤ 𝒮 over S is an equivalence.

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

The HasFibers on p : 𝒳 ⥤ 𝒮 given by the fibers of p

Equations

• HasFibers.canonical p = { Fib := p.Fiber, category := inferInstance, ι := fun (S : 𝒮) => CategoryTheory.Functor.Fiber.fiberInclusion, comp_const := ⋯, equiv := ⋯ }

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

The induced functor from Fib p S to the standard fiber.

Equations

• HasFibers.inducedFunctor p S = CategoryTheory.Functor.Fiber.inducedFunctor ⋯

@[simp]

theorem HasFibers.inducedFunctor_map_coe {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) [HasFibers p] (S : 𝒮) {X✝ Y✝ : Fib p S} (φ : X✝ ⟶ Y✝) : ↑((inducedFunctor p S).map φ) = (ι S).map φ

@[simp]

theorem HasFibers.inducedFunctor_obj_coe {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) [HasFibers p] (S : 𝒮) (x : Fib p S) : ↑((inducedFunctor p S).obj x) = (ι S).obj x

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

The natural transformation ι S ≅ (inducedFunctor p S) ⋙ (fiberInclusion p S)

Equations

• HasFibers.inducedFunctor.natIso p S = CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf ⋯

theorem HasFibers.inducedFunctor_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) [HasFibers p] (S : 𝒮) : ι S = (inducedFunctor p S).comp CategoryTheory.Functor.Fiber.fiberInclusion

instance HasFibers.instIsEquivalenceFibFiberInducedFunctor {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) [HasFibers p] (S : 𝒮) : (inducedFunctor p S).IsEquivalence

instance HasFibers.instFaithfulFibι {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) [HasFibers p] (S : 𝒮) : (ι S).Faithful

@[simp]

theorem HasFibers.proj_eq {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} (a : Fib p S) : p.obj ((ι S).obj a) = S

def HasFibers.projMap {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {R S : 𝒮} {a : Fib p R} {b : Fib p S} (φ : (ι R).obj a ⟶ (ι S).obj b) : R ⟶ S

The morphism R ⟶ S in 𝒮 obtained by projecting a morphism φ : (ι R).obj a ⟶ (ι S).obj b.

Equations

• HasFibers.projMap φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (p.map φ) (CategoryTheory.eqToHom ⋯))

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

For any homomorphism φ in a fiber Fib S, its image under ι S lies over 𝟙 S.

noncomputable def HasFibers.Fib.homMk {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} {a b : Fib p S} (φ : (ι S).obj a ⟶ (ι S).obj b) [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ] : a ⟶ b

A version of fullness of the functor Fib S ⥤ Fiber p S that can be used inside the category 𝒳.

Equations

• HasFibers.Fib.homMk φ = (HasFibers.inducedFunctor p S).preimage (CategoryTheory.Functor.Fiber.homMk p S φ)

@[simp]

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

theorem HasFibers.Fib.hom_ext {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} {a b : Fib p S} {f g : a ⟶ b} (h : (ι S).map f = (ι S).map g) : f = g

theorem HasFibers.Fib.hom_ext_iff {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} {a b : Fib p S} {f g : a ⟶ b} : f = g ↔ (ι S).map f = (ι S).map g

noncomputable def HasFibers.Fib.isoMk {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} {a b : Fib p S} (Φ : (ι S).obj a ≅ (ι S).obj b) (hΦ : p.IsHomLift (CategoryTheory.CategoryStruct.id S) Φ.hom) : a ≅ b

The lift of an isomorphism Φ : (ι S).obj a ≅ (ι S).obj b lying over 𝟙 S to an isomorphism in Fib S.

Equations

• HasFibers.Fib.isoMk Φ hΦ = { hom := HasFibers.Fib.homMk Φ.hom, inv := HasFibers.Fib.homMk Φ.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem HasFibers.Fib.isoMk_hom {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} {a b : Fib p S} (Φ : (ι S).obj a ≅ (ι S).obj b) (hΦ : p.IsHomLift (CategoryTheory.CategoryStruct.id S) Φ.hom) : (isoMk Φ hΦ).hom = homMk Φ.hom

@[simp]

theorem HasFibers.Fib.isoMk_inv {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} {a b : Fib p S} (Φ : (ι S).obj a ≅ (ι S).obj b) (hΦ : p.IsHomLift (CategoryTheory.CategoryStruct.id S) Φ.hom) : (isoMk Φ hΦ).inv = homMk Φ.inv

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

An object in Fib p S isomorphic in 𝒳 to a given object a : 𝒳 such that p(a) = S.

Equations

• HasFibers.Fib.mk ha = (HasFibers.inducedFunctor p S).objPreimage (CategoryTheory.Functor.Fiber.mk ha)

noncomputable def HasFibers.Fib.mkIsoSelf {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} {a : 𝒳} (ha : p.obj a = S) : (ι S).obj (mk ha) ≅ a

Applying ι S to the preimage of a : 𝒳 in Fib p S yields an object isomorphic to a.

Equations

• HasFibers.Fib.mkIsoSelf ha = CategoryTheory.Functor.Fiber.fiberInclusion.mapIso ((HasFibers.inducedFunctor p S).objObjPreimageIso (CategoryTheory.Functor.Fiber.mk ha))

instance HasFibers.Fib.mkIsoSelfIsHomLift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {S : 𝒮} {a : 𝒳} (ha : p.obj a = S) : p.IsHomLift (CategoryTheory.CategoryStruct.id S) (mkIsoSelf ha).hom

noncomputable def HasFibers.mkPullback {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] [p.IsPreFibered] {R S : 𝒮} {a : 𝒳} (f : R ⟶ S) (ha : p.obj a = S) : Fib p R

The domain, taken in Fib p R, of some cartesian morphism lifting a given f : R ⟶ S in 𝒮

Equations

• HasFibers.mkPullback f ha = HasFibers.Fib.mk ⋯

noncomputable def HasFibers.pullbackMap {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] [p.IsPreFibered] {R S : 𝒮} {a : 𝒳} (f : R ⟶ S) (ha : p.obj a = S) : (ι R).obj (mkPullback f ha) ⟶ a

A cartesian morphism lifting f : R ⟶ S with domain in the image of Fib p R

Equations

• HasFibers.pullbackMap f ha = CategoryTheory.CategoryStruct.comp (HasFibers.Fib.mkIsoSelf ⋯).hom (CategoryTheory.Functor.IsPreFibered.pullbackMap ha f)

instance HasFibers.pullbackMap.isCartesian {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] [p.IsPreFibered] {R S : 𝒮} {a : 𝒳} (f : R ⟶ S) (ha : p.obj a = S) : p.IsCartesian f (pullbackMap f ha)

noncomputable def HasFibers.inducedMap {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {R S : 𝒮} {a : 𝒳} {b b' : Fib p R} (f : R ⟶ S) (ψ : (ι R).obj b' ⟶ a) [p.IsCartesian f ψ] (φ : (ι R).obj b ⟶ a) [p.IsHomLift f φ] : b ⟶ b'

Given a fibered category p, b' b in Fib R, and a pullback ψ : b ⟶ a in 𝒳, i.e.

b'       b --ψ--> a
|        |        |
v        v        v
R ====== R --f--> S

Then the induced map τ : b' ⟶ b can be lifted to the fiber over R

Equations

• HasFibers.inducedMap f ψ φ = HasFibers.Fib.homMk (CategoryTheory.Functor.IsCartesian.map p f ψ φ)

theorem HasFibers.inducedMap_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {R S : 𝒮} {a : 𝒳} {b b' : Fib p R} (f : R ⟶ S) (ψ : (ι R).obj b' ⟶ a) [p.IsCartesian f ψ] (φ : (ι R).obj b ⟶ a) [p.IsHomLift f φ] : CategoryTheory.CategoryStruct.comp ((ι R).map (inducedMap f ψ φ)) ψ = φ

theorem HasFibers.inducedMap_comp_assoc {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] {R S : 𝒮} {a : 𝒳} {b b' : Fib p R} (f : R ⟶ S) (ψ : (ι R).obj b' ⟶ a) [p.IsCartesian f ψ] (φ : (ι R).obj b ⟶ a) [p.IsHomLift f φ] {Z : 𝒳} (h : a ⟶ Z) : CategoryTheory.CategoryStruct.comp ((ι R).map (inducedMap f ψ φ)) (CategoryTheory.CategoryStruct.comp ψ h) = CategoryTheory.CategoryStruct.comp φ h

theorem HasFibers.fiber_factorization {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} [HasFibers p] [p.IsFibered] {R S : 𝒮} {a : 𝒳} (ha : p.obj a = S) {b : Fib p R} (f : R ⟶ S) (φ : (ι R).obj b ⟶ a) [p.IsHomLift f φ] : ∃ (b' : Fib p R), ∃ (τ : b ⟶ b'), ∃ (ψ : (ι R).obj b' ⟶ a), p.IsStronglyCartesian f ψ ∧ CategoryTheory.CategoryStruct.comp ((ι R).map τ) ψ = φ

Given a : 𝒳, b : Fib p R, and a diagram

  b --φ--> a
  -        -
  |        |
  v        v
  R --f--> S

It can be factorized as

  b --τ--> b'--ψ--> a
  -        -        -
  |        |        |
  v        v        v
  R ====== R --f--> S

with ψ cartesian over f and τ a map in Fib p R.