Shrinking sieve functors

The presheaf associated to a sieve naturally takes values in the universe containing the hom-sets of the ambient category. For a locally small category, the Yoneda shrinking construction allows this presheaf to be represented in a chosen smaller universe.

This file defines Sieve.shrinkFunctor, the universe-shrunk presheaf associated to a sieve, and constructs its comparison isomorphism with the lifted sieve presheaf. It also records the compatibility of this isomorphism with the inclusion into the corresponding Yoneda presheaf.

Tags

sieve, presheaf, universe

def CategoryTheory.Sieve.shrinkFunctor {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] {X : C} (S : Sieve X) : Subfunctor (shrinkYoneda.{w, v₁, u₁}.obj X)

If C is w-locally small, any sieve induces a subfunctor of shrinkYoneda.{w}.obj X.

Equations

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

@[simp]

theorem CategoryTheory.Sieve.shrinkFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] {X : C} (S : Sieve X) (Y : Cᵒᵖ) : (shrinkFunctor.{w, v₁, u₁} S).obj Y = {f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y | S.arrows (shrinkYonedaObjObjEquiv f)}

noncomputable def CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{max w' w, v₁, u₁} C] : (shrinkFunctor.{w, v₁, u₁} S).toFunctor.comp CategoryTheory.uliftFunctor.{w', w} ≅ (shrinkFunctor.{max w' w, v₁, u₁} S).toFunctor

Sieve.shrinkFunctor is compatible with universe lifting.

Equations

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

theorem CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{max w' w, v₁, u₁} C] : CategoryStruct.comp S.shrinkFunctorUliftFunctorIso.inv (Functor.whiskerRight (shrinkFunctor.{w, v₁, u₁} S).ι CategoryTheory.uliftFunctor.{w', w}) = CategoryStruct.comp (shrinkFunctor.{max w' w, v₁, u₁} S).ι (shrinkYonedaUliftFunctorIso.inv.app X)

theorem CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{max w' w, v₁, u₁} C] {Z : Functor Cᵒᵖ (Type (max w w'))} (h : (shrinkYoneda.{w, v₁, u₁}.obj X).comp CategoryTheory.uliftFunctor.{w', w} ⟶ Z) : CategoryStruct.comp S.shrinkFunctorUliftFunctorIso.inv (CategoryStruct.comp (Functor.whiskerRight (shrinkFunctor.{w, v₁, u₁} S).ι CategoryTheory.uliftFunctor.{w', w}) h) = CategoryStruct.comp (shrinkFunctor.{max w' w, v₁, u₁} S).ι (CategoryStruct.comp (shrinkYonedaUliftFunctorIso.inv.app X) h)

noncomputable def CategoryTheory.Sieve.shrinkFunctorIsoFunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ≅ S.functor

Shrinking does nothing for the same universe level.

Equations

• S.shrinkFunctorIsoFunctor = CategoryTheory.NatIso.ofComponents (fun (Y : Cᵒᵖ) => (CategoryTheory.shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso) ⋯

@[simp]

theorem CategoryTheory.Sieve.shrinkFunctorIsoFunctor_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) (X✝ : Cᵒᵖ) : S.shrinkFunctorIsoFunctor.hom.app X✝ = (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom

@[simp]

theorem CategoryTheory.Sieve.shrinkFunctorIsoFunctor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) (X✝ : Cᵒᵖ) : S.shrinkFunctorIsoFunctor.inv.app X✝ = (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.inv