The presheaf associated to a sieve

A sieve S on an object X of a category C determines a presheaf whose value at Y is the type of morphisms Y ⟶ X belonging to S. The closure condition for a sieve makes this construction functorial, and the resulting presheaf is naturally a subfunctor of the Yoneda presheaf of X.

This file defines the associated presheaf Sieve.functor, its monomorphic natural transformation Sieve.functorInclusion into yoneda.obj X, and natural transformations induced by inclusions of sieves. It also reconstructs a sieve from a subfunctor of a representable presheaf. Parallel constructions using uliftYoneda are provided for situations in which universe levels must be adjusted.

Tags

sieve, presheaf, Yoneda

def CategoryTheory.Sieve.functor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : Functor Cᵒᵖ (Type v₁)

A sieve induces a presheaf.

Equations

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

@[simp]

theorem CategoryTheory.Sieve.functor_obj {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) (Y : Cᵒᵖ) : S.functor.obj Y = { g : Opposite.unop Y ⟶ X // S.arrows g }

@[simp]

theorem CategoryTheory.Sieve.functor_map {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : S.functor.map f = TypeCat.ofHom fun (g : { g : Opposite.unop X✝ ⟶ X // S.arrows g }) => ⟨CategoryStruct.comp f.unop ↑g, ⋯⟩

def CategoryTheory.Sieve.natTransOfLe {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S T : Sieve X} (h : S ≤ T) : S.functor ⟶ T.functor

If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced presheaves.

Equations

• CategoryTheory.Sieve.natTransOfLe h = { app := fun (x : Cᵒᵖ) => TypeCat.ofHom fun (f : S.functor.obj x) => ⟨↑f, ⋯⟩, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.natTransOfLe_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S T : Sieve X} (h : S ≤ T) (x✝ : Cᵒᵖ) : (natTransOfLe h).app x✝ = TypeCat.ofHom fun (f : S.functor.obj x✝) => ⟨↑f, ⋯⟩

def CategoryTheory.Sieve.functorInclusion {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : S.functor ⟶ yoneda.obj X

The natural inclusion from the functor induced by a sieve to the yoneda embedding.

Equations

• S.functorInclusion = { app := fun (x : Cᵒᵖ) => TypeCat.ofHom fun (f : S.functor.obj x) => ↑f, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.functorInclusion_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) (x✝ : Cᵒᵖ) : S.functorInclusion.app x✝ = TypeCat.ofHom fun (f : S.functor.obj x✝) => ↑f

def CategoryTheory.Sieve.toFunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : yoneda.obj Y ⟶ S.functor

Any component f : Y ⟶ X of the sieve S induces a natural transformation from yoneda.obj Y to the presheaf induced by S.

Equations

• S.toFunctor f hf = { app := fun (Z : Cᵒᵖ) => TypeCat.ofHom fun (g : (CategoryTheory.yoneda.obj Y).obj Z) => ⟨CategoryTheory.CategoryStruct.comp g f, ⋯⟩, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.toFunctor_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) (Z : Cᵒᵖ) : (S.toFunctor f hf).app Z = TypeCat.ofHom fun (g : (yoneda.obj Y).obj Z) => ⟨CategoryStruct.comp g f, ⋯⟩

theorem CategoryTheory.Sieve.natTransOfLe_comm {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S T : Sieve X} (h : S ≤ T) : CategoryStruct.comp (natTransOfLe h) T.functorInclusion = S.functorInclusion

instance CategoryTheory.Sieve.functorInclusion_is_mono {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} : Mono S.functorInclusion

The presheaf induced by a sieve is a subobject of the yoneda embedding.

def CategoryTheory.Sieve.sieveOfSubfunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R : Functor Cᵒᵖ (Type v₁)} (f : R ⟶ yoneda.obj X) : Sieve X

A natural transformation to a representable functor induces a sieve. This is the left inverse of functorInclusion, shown in sieveOfSubfunctor_functorInclusion.

Equations

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

@[simp]

theorem CategoryTheory.Sieve.sieveOfSubfunctor_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R : Functor Cᵒᵖ (Type v₁)} (f : R ⟶ yoneda.obj X) (Y : C) (g : Y ⟶ X) : (sieveOfSubfunctor f).arrows g = ∃ (t : R.obj (Opposite.op Y)), (ConcreteCategory.hom (f.app (Opposite.op Y))) t = g

theorem CategoryTheory.Sieve.sieveOfSubfunctor_functorInclusion {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} : sieveOfSubfunctor S.functorInclusion = S

instance CategoryTheory.Sieve.functorInclusion_top_isIso {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : IsIso ⊤.functorInclusion

@[reducible, inline]

abbrev CategoryTheory.Sieve.uliftFunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : Functor Cᵒᵖ (Type (max w v₁))

A variant of Sieve.functor with universe lifting.

Equations

• S.uliftFunctor = S.functor.comp CategoryTheory.uliftFunctor.{?u.3, ?u.2}

def CategoryTheory.Sieve.uliftNatTransOfLe {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S T : Sieve X} (h : S ≤ T) : S.uliftFunctor ⟶ T.uliftFunctor

A variant of Sieve.natTransOfLe with universe lifting.

Equations

• CategoryTheory.Sieve.uliftNatTransOfLe h = { app := fun (x : Cᵒᵖ) => TypeCat.ofHom fun (f : S.uliftFunctor.obj x) => { down := ⟨↑f.down, ⋯⟩ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.uliftNatTransOfLe_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S T : Sieve X} (h : S ≤ T) (x✝ : Cᵒᵖ) : (uliftNatTransOfLe h).app x✝ = TypeCat.ofHom fun (f : S.uliftFunctor.obj x✝) => { down := ⟨↑f.down, ⋯⟩ }

def CategoryTheory.Sieve.uliftFunctorInclusion {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : S.uliftFunctor ⟶ uliftYoneda.{w, v₁, u₁}.obj X

A variant of Sieve.functorInclusion with universe lifting.

Equations

• S.uliftFunctorInclusion = CategoryTheory.Functor.whiskerRight S.functorInclusion CategoryTheory.uliftFunctor.{?u.3, ?u.2}

@[simp]

theorem CategoryTheory.Sieve.uliftFunctorInclusion_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) (X✝ : Cᵒᵖ) : S.uliftFunctorInclusion.app X✝ = TypeCat.ofHom fun (x : ULift.{w, v₁} { g : Opposite.unop X✝ ⟶ X // S.arrows g }) => { down := ↑x.down }

def CategoryTheory.Sieve.toUliftFunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : uliftYoneda.{w, v₁, u₁}.obj Y ⟶ S.uliftFunctor

A variant of Sieve.toFunctor with universe lifting.

Equations

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

@[simp]

theorem CategoryTheory.Sieve.toUliftFunctor_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) (Z : Cᵒᵖ) : (S.toUliftFunctor f hf).app Z = TypeCat.ofHom fun (g : (uliftYoneda.{w, v₁, u₁}.obj Y).obj Z) => { down := ⟨CategoryStruct.comp g.down f, ⋯⟩ }

theorem CategoryTheory.Sieve.uliftNatTransOfLe_comm {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S T : Sieve X} (h : S ≤ T) : CategoryStruct.comp (uliftNatTransOfLe h) T.uliftFunctorInclusion = S.uliftFunctorInclusion

instance CategoryTheory.Sieve.uliftFunctorInclusion_is_mono {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : Mono S.uliftFunctorInclusion

The presheaf induced by a sieve is a subobject of the yoneda embedding.

def CategoryTheory.Sieve.sieveOfUliftSubfunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R : Functor Cᵒᵖ (Type (max w v₁))} (f : R ⟶ uliftYoneda.{w, v₁, u₁}.obj X) : Sieve X

A variant of Sieve.sieveOfSubfunctor with universe lifting.

Equations

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

@[simp]

theorem CategoryTheory.Sieve.sieveOfUliftSubfunctor_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R : Functor Cᵒᵖ (Type (max w v₁))} (f : R ⟶ uliftYoneda.{w, v₁, u₁}.obj X) (Y : C) (g : Y ⟶ X) : (sieveOfUliftSubfunctor f).arrows g = ∃ (t : R.obj (Opposite.op Y)), (ConcreteCategory.hom (f.app (Opposite.op Y))) t = { down := g }

theorem CategoryTheory.Sieve.sieveOfUliftSubfunctor_uliftFunctorInclusion {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} : sieveOfUliftSubfunctor S.uliftFunctorInclusion = S

instance CategoryTheory.Sieve.uliftFunctorInclusion_top_isIso {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : IsIso ⊤.uliftFunctorInclusion