# Documentation

Mathlib.CategoryTheory.Sites.Sieves

# Theory of sieves #

• For an object X of a category C, a Sieve X is a set of morphisms to X which is closed under left-composition.
• The complete lattice structure on sieves is given, as well as the Galois insertion given by downward-closing.
• A Sieve X (functorially) induces a presheaf on C together with a monomorphism to the yoneda embedding of X.

## Tags #

sieve, pullback

def CategoryTheory.Presieve {C : Type u₁} [] (X : C) :
Type (max u₁ v₁)

A set of arrows all with codomain X.

Instances For
noncomputable instance CategoryTheory.Presieve.instInhabitedPresieve {C : Type u₁} [] {X : C} :
@[inline, reducible]
abbrev CategoryTheory.Presieve.diagram {C : Type u₁} [] {X : C} (S : ) :
CategoryTheory.Functor (CategoryTheory.FullSubcategory fun f => S (().obj f.left) f.hom) C

Given a sieve S on X : C, its associated diagram S.diagram is defined to be the natural functor from the full subcategory of the over category C/X consisting of arrows in S to C.

Instances For
@[inline, reducible]
abbrev CategoryTheory.Presieve.cocone {C : Type u₁} [] {X : C} (S : ) :

Given a sieve S on X : C, its associated cocone S.cocone is defined to be the natural cocone over the diagram defined above with cocone point X.

Instances For
def CategoryTheory.Presieve.bind {C : Type u₁} [] {X : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S Y f) :

Given a set of arrows S all with codomain X, and a set of arrows with codomain Y for each f : Y ⟶ X in S, produce a set of arrows with codomain X: { g ≫ f | (f : Y ⟶ X) ∈ S, (g : Z ⟶ Y) ∈ R f }.

Instances For
@[simp]
theorem CategoryTheory.Presieve.bind_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : Y X) {S : } {R : Y : C⦄ → f : Y X⦄ → S Y f} {g : Z Y} (h₁ : S Y f) (h₂ : R Y f h₁ Z g) :
inductive CategoryTheory.Presieve.singleton' {C : Type u₁} [] {X : C} {Y : C} (f : Y X) ⦃Y : C :
(Y X) → Prop
• mk: ∀ {C : Type u₁} [inst : ] {X Y : C} {f : Y X},

The singleton presieve.

Instances For
def CategoryTheory.Presieve.singleton {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :

The singleton presieve.

Instances For
theorem CategoryTheory.Presieve.singleton.mk {C : Type u₁} [] {X : C} {Y : C} {f : Y X} :
@[simp]
theorem CategoryTheory.Presieve.singleton_eq_iff_domain {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (g : Y X) :
theorem CategoryTheory.Presieve.singleton_self {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
inductive CategoryTheory.Presieve.pullbackArrows {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :

Pullback a set of arrows with given codomain along a fixed map, by taking the pullback in the category. This is not the same as the arrow set of Sieve.pullback, but there is a relation between them in pullbackArrows_comm.

Instances For
theorem CategoryTheory.Presieve.pullback_singleton {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : Y X) (g : Z X) :
= CategoryTheory.Presieve.singleton CategoryTheory.Limits.pullback.snd
inductive CategoryTheory.Presieve.ofArrows {C : Type u₁} [] {X : C} {ι : Type u_1} (Y : ιC) (f : (i : ι) → Y i X) :
• mk: ∀ {C : Type u₁} [inst : ] {X : C} {ι : Type u_1} {Y : ιC} {f : (i : ι) → Y i X} (i : ι),

Construct the presieve given by the family of arrows indexed by ι.

Instances For
theorem CategoryTheory.Presieve.ofArrows_pUnit {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
(CategoryTheory.Presieve.ofArrows (fun x => Y) fun x => f) =
theorem CategoryTheory.Presieve.ofArrows_pullback {C : Type u₁} [] {X : C} {Y : C} (f : Y X) {ι : Type u_1} (Z : ιC) (g : (i : ι) → Z i X) :
(CategoryTheory.Presieve.ofArrows (fun i => ) fun i => CategoryTheory.Limits.pullback.snd) =
theorem CategoryTheory.Presieve.ofArrows_bind {C : Type u₁} [] {X : C} {ι : Type u_1} (Z : ιC) (g : (i : ι) → Z i X) (j : Y : C⦄ → (f : Y X) → Type u_2) (W : Y : C⦄ → (f : Y X) → (H : ) → j Y f HC) (k : Y : C⦄ → (f : Y X) → (H : ) → (i : j Y f H) → W Y f H i Y) :
(CategoryTheory.Presieve.bind () fun Y f H => CategoryTheory.Presieve.ofArrows (W Y f H) (k Y f H)) = CategoryTheory.Presieve.ofArrows (fun i => W (Z i.fst) (g i.fst) (_ : CategoryTheory.Presieve.ofArrows Z g (g i.fst)) i.snd) fun ij => CategoryTheory.CategoryStruct.comp (k (Z ij.fst) (g ij.fst) (_ : CategoryTheory.Presieve.ofArrows Z g (g ij.fst)) ij.snd) (g ij.fst)
def CategoryTheory.Presieve.functorPullback {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Presieve (F.obj X)) :

Given a presieve on F(X), we can define a presieve on X by taking the preimage via F.

Instances For
@[simp]
theorem CategoryTheory.Presieve.functorPullback_mem {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Presieve (F.obj X)) {Y : C} (f : Y X) :
R (F.obj Y) (F.map f)
@[simp]
theorem CategoryTheory.Presieve.functorPullback_id {C : Type u₁} [] {X : C} (R : ) :
class CategoryTheory.Presieve.hasPullbacks {C : Type u₁} [] {X : C} (R : ) :
• has_pullbacks : ∀ {Y Z : C} {f : Y X}, R f∀ {g : Z X},

For all arrows f and g in R, the pullback of f and g exists.

Given a presieve R on X, the predicate R.hasPullbacks means that for all arrows f and g in R, the pullback of f and g exists.

Instances
instance CategoryTheory.Presieve.instHasPullbacks {C : Type u₁} [] {X : C} (R : ) :
def CategoryTheory.Presieve.functorPushforward {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : ) :

Given a presieve on X, we can define a presieve on F(X) (which is actually a sieve) by taking the sieve generated by the image via F.

Instances For
structure CategoryTheory.Presieve.FunctorPushforwardStructure {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : ) {Y : D} (f : Y F.obj X) :
Type (max (max u₁ v₁) v₂)
• preobj : C

an object in the source category

• premap : s.preobj X

a map in the source category which has to be in the presieve

• lift : Y F.obj s.preobj

the morphism which appear in the factorisation

• cover : S s.premap

the condition that premap is in the presieve

• fac : f = CategoryTheory.CategoryStruct.comp s.lift (F.map s.premap)

the factorisation of the morphism

An auxiliary definition in order to fix the choice of the preimages between various definitions.

Instances For
noncomputable def CategoryTheory.Presieve.getFunctorPushforwardStructure {C : Type u₁} [] {D : Type u₂} [] {X : C} {F : } {S : } {Y : D} {f : Y F.obj X} (h : ) :

The fixed choice of a preimage.

Instances For
theorem CategoryTheory.Presieve.functorPushforward_comp {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {E : Type u₃} [] (G : ) (R : ) :
theorem CategoryTheory.Presieve.image_mem_functorPushforward {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (R : ) {f : Y X} (h : R Y f) :
structure CategoryTheory.Sieve {C : Type u₁} [] (X : C) :
Type (max u₁ v₁)
• arrows :

the underlying presieve

• downward_closed : ∀ {Y Z : C} {f : Y X}, s.arrows f∀ (g : Z Y), s.arrows ()

stability by precomposition

For an object X of a category C, a Sieve X is a set of morphisms to X which is closed under left-composition.

Instances For
instance CategoryTheory.Sieve.instCoeFunSievePresieve {C : Type u₁} [] {X : C} :
CoeFun () fun x =>
theorem CategoryTheory.Sieve.arrows_ext {C : Type u₁} [] {X : C} {R : } {S : } :
R.arrows = S.arrowsR = S
theorem CategoryTheory.Sieve.ext {C : Type u₁} [] {X : C} {R : } {S : } (h : ∀ ⦃Y : C⦄ (f : Y X), R.arrows f S.arrows f) :
R = S
theorem CategoryTheory.Sieve.ext_iff {C : Type u₁} [] {X : C} {R : } {S : } :
R = S ∀ ⦃Y : C⦄ (f : Y X), R.arrows f S.arrows f
def CategoryTheory.Sieve.sup {C : Type u₁} [] {X : C} (𝒮 : ) :

The supremum of a collection of sieves: the union of them all.

Instances For
def CategoryTheory.Sieve.inf {C : Type u₁} [] {X : C} (𝒮 : ) :

The infimum of a collection of sieves: the intersection of them all.

Instances For
def CategoryTheory.Sieve.union {C : Type u₁} [] {X : C} (S : ) (R : ) :

The union of two sieves is a sieve.

Instances For
def CategoryTheory.Sieve.inter {C : Type u₁} [] {X : C} (S : ) (R : ) :

The intersection of two sieves is a sieve.

Instances For
instance CategoryTheory.Sieve.instCompleteLatticeSieve {C : Type u₁} [] {X : C} :

Sieves on an object X form a complete lattice. We generate this directly rather than using the galois insertion for nicer definitional properties.

instance CategoryTheory.Sieve.sieveInhabited {C : Type u₁} [] {X : C} :

The maximal sieve always exists.

@[simp]
theorem CategoryTheory.Sieve.sInf_apply {C : Type u₁} [] {X : C} {Ss : } {Y : C} (f : Y X) :
(sInf Ss).arrows f ∀ (S : ), S SsS.arrows f
@[simp]
theorem CategoryTheory.Sieve.sSup_apply {C : Type u₁} [] {X : C} {Ss : } {Y : C} (f : Y X) :
(sSup Ss).arrows f S x, S.arrows f
@[simp]
theorem CategoryTheory.Sieve.inter_apply {C : Type u₁} [] {X : C} {R : } {S : } {Y : C} (f : Y X) :
(R S).arrows f R.arrows f S.arrows f
@[simp]
theorem CategoryTheory.Sieve.union_apply {C : Type u₁} [] {X : C} {R : } {S : } {Y : C} (f : Y X) :
(R S).arrows f R.arrows f S.arrows f
@[simp]
theorem CategoryTheory.Sieve.top_apply {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
.arrows f
@[simp]
theorem CategoryTheory.Sieve.generate_apply {C : Type u₁} [] {X : C} (R : ) (Z : C) (f : Z X) :
().arrows f = Y h g, R Y g
def CategoryTheory.Sieve.generate {C : Type u₁} [] {X : C} (R : ) :

Generate the smallest sieve containing the given set of arrows.

Instances For
@[simp]
theorem CategoryTheory.Sieve.bind_apply {C : Type u₁} [] {X : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S Y f) :
().arrows = CategoryTheory.Presieve.bind S fun Y f h => (R Y f h).arrows
def CategoryTheory.Sieve.bind {C : Type u₁} [] {X : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S Y f) :

Given a presieve on X, and a sieve on each domain of an arrow in the presieve, we can bind to produce a sieve on X.

Instances For
theorem CategoryTheory.Sieve.sets_iff_generate {C : Type u₁} [] {X : C} (R : ) (S : ) :
R S.arrows
def CategoryTheory.Sieve.giGenerate {C : Type u₁} [] {X : C} :
GaloisInsertion CategoryTheory.Sieve.generate CategoryTheory.Sieve.arrows

Show that there is a galois insertion (generate, set_over).

Instances For
theorem CategoryTheory.Sieve.le_generate {C : Type u₁} [] {X : C} (R : ) :
R ().arrows
@[simp]
theorem CategoryTheory.Sieve.generate_sieve {C : Type u₁} [] {X : C} (S : ) :
theorem CategoryTheory.Sieve.id_mem_iff_eq_top {C : Type u₁} [] {X : C} {S : } :
S.arrows () S =

If the identity arrow is in a sieve, the sieve is maximal.

theorem CategoryTheory.Sieve.generate_of_contains_isSplitEpi {C : Type u₁} [] {X : C} {Y : C} {R : } (f : Y X) (hf : R Y f) :

If an arrow set contains a split epi, it generates the maximal sieve.

@[simp]
theorem CategoryTheory.Sieve.generate_of_singleton_isSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
@[simp]
theorem CategoryTheory.Sieve.generate_top {C : Type u₁} [] {X : C} :
@[simp]
theorem CategoryTheory.Sieve.pullback_apply {C : Type u₁} [] {X : C} {Y : C} (h : Y X) (S : ) (Y : C) (sl : Y Y) :
().arrows sl = S.arrows ()
def CategoryTheory.Sieve.pullback {C : Type u₁} [] {X : C} {Y : C} (h : Y X) (S : ) :

Given a morphism h : Y ⟶ X, send a sieve S on X to a sieve on Y as the inverse image of S with _ ≫ h. That is, Sieve.pullback S h := (≫ h) '⁻¹ S.

Instances For
@[simp]
theorem CategoryTheory.Sieve.pullback_id {C : Type u₁} [] {X : C} {S : } :
@[simp]
theorem CategoryTheory.Sieve.pullback_top {C : Type u₁} [] {X : C} {Y : C} {f : Y X} :
theorem CategoryTheory.Sieve.pullback_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : Y X} {g : Z Y} (S : ) :
@[simp]
theorem CategoryTheory.Sieve.pullback_inter {C : Type u₁} [] {X : C} {Y : C} {f : Y X} (S : ) (R : ) :
theorem CategoryTheory.Sieve.pullback_eq_top_iff_mem {C : Type u₁} [] {X : C} {Y : C} {S : } (f : Y X) :
S.arrows f
theorem CategoryTheory.Sieve.pullback_eq_top_of_mem {C : Type u₁} [] {X : C} {Y : C} (S : ) {f : Y X} :
S.arrows f
@[simp]
theorem CategoryTheory.Sieve.pushforward_apply {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) (Z : C) (gf : Z X) :
().arrows gf = g, R.arrows g
def CategoryTheory.Sieve.pushforward {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :

Push a sieve R on Y forward along an arrow f : Y ⟶ X: gf : Z ⟶ X is in the sieve if gf factors through some g : Z ⟶ Y which is in R.

Instances For
theorem CategoryTheory.Sieve.pushforward_apply_comp {C : Type u₁} [] {X : C} {Y : C} {R : } {Z : C} {g : Z Y} (hg : R.arrows g) (f : Y X) :
().arrows ()
theorem CategoryTheory.Sieve.pushforward_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : Y X} {g : Z Y} (R : ) :
theorem CategoryTheory.Sieve.galoisConnection {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
theorem CategoryTheory.Sieve.pullback_monotone {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
theorem CategoryTheory.Sieve.pushforward_monotone {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
theorem CategoryTheory.Sieve.le_pushforward_pullback {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :
theorem CategoryTheory.Sieve.pullback_pushforward_le {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :
theorem CategoryTheory.Sieve.pushforward_union {C : Type u₁} [] {X : C} {Y : C} {f : Y X} (S : ) (R : ) :
theorem CategoryTheory.Sieve.pushforward_le_bind_of_mem {C : Type u₁} [] {X : C} {Y : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S Y f) (f : Y X) (h : S Y f) :
theorem CategoryTheory.Sieve.le_pullback_bind {C : Type u₁} [] {X : C} {Y : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S Y f) (f : Y X) (h : S Y f) :
R Y f h
def CategoryTheory.Sieve.galoisCoinsertionOfMono {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :

If f is a monomorphism, the pushforward-pullback adjunction on sieves is coreflective.

Instances For
def CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :

If f is a split epi, the pushforward-pullback adjunction on sieves is reflective.

Instances For
theorem CategoryTheory.Sieve.pullbackArrows_comm {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :
@[simp]
theorem CategoryTheory.Sieve.functorPullback_apply {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Sieve (F.obj X)) :
().arrows =
def CategoryTheory.Sieve.functorPullback {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Sieve (F.obj X)) :

If R is a sieve, then the CategoryTheory.Presieve.functorPullback of R is actually a sieve.

Instances For
@[simp]
theorem CategoryTheory.Sieve.functorPullback_arrows {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Sieve (F.obj X)) :
().arrows =
@[simp]
theorem CategoryTheory.Sieve.functorPullback_id {C : Type u₁} [] {X : C} (R : ) :
theorem CategoryTheory.Sieve.functorPullback_comp {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {E : Type u₃} [] (G : ) (R : CategoryTheory.Sieve (().obj X)) :
theorem CategoryTheory.Sieve.functorPushforward_extend_eq {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {R : } :
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_apply {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : ) :
().arrows =
def CategoryTheory.Sieve.functorPushforward {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : ) :

The sieve generated by the image of R under F.

Instances For
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_id {C : Type u₁} [] {X : C} (R : ) :
theorem CategoryTheory.Sieve.functorPushforward_comp {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {E : Type u₃} [] (G : ) (R : ) :
theorem CategoryTheory.Sieve.functor_galoisConnection {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
theorem CategoryTheory.Sieve.functorPullback_monotone {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
theorem CategoryTheory.Sieve.functorPushforward_monotone {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
theorem CategoryTheory.Sieve.le_functorPushforward_pullback {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : ) :
theorem CategoryTheory.Sieve.functorPullback_pushforward_le {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Sieve (F.obj X)) :
theorem CategoryTheory.Sieve.functorPushforward_union {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : ) (R : ) :
theorem CategoryTheory.Sieve.functorPullback_union {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : CategoryTheory.Sieve (F.obj X)) (R : CategoryTheory.Sieve (F.obj X)) :
theorem CategoryTheory.Sieve.functorPullback_inter {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : CategoryTheory.Sieve (F.obj X)) (R : CategoryTheory.Sieve (F.obj X)) :
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_bot {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_top {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
@[simp]
theorem CategoryTheory.Sieve.functorPullback_bot {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
@[simp]
theorem CategoryTheory.Sieve.functorPullback_top {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
theorem CategoryTheory.Sieve.image_mem_functorPushforward {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : ) {V : C} {f : V X} (h : R.arrows f) :
().arrows (F.map f)
def CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :

When F is essentially surjective and full, the galois connection is a galois insertion.

Instances For
def CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :

When F is fully faithful, the galois connection is a galois coinsertion.

Instances For
@[simp]
theorem CategoryTheory.Sieve.functor_obj {C : Type u₁} [] {X : C} (S : ) (Y : Cᵒᵖ) :
().obj Y = { g // S.arrows g }
@[simp]
theorem CategoryTheory.Sieve.functor_map_coe {C : Type u₁} [] {X : C} (S : ) :
∀ {X Y : Cᵒᵖ} (f : X Y) (g : { g // S.arrows g }), ↑(().map f g) =
def CategoryTheory.Sieve.functor {C : Type u₁} [] {X : C} (S : ) :

A sieve induces a presheaf.

Instances For
@[simp]
theorem CategoryTheory.Sieve.natTransOfLe_app_coe {C : Type u₁} [] {X : C} {S : } {T : } (h : S T) (Y : Cᵒᵖ) (f : ().obj Y) :
↑(().app Y f) = f
def CategoryTheory.Sieve.natTransOfLe {C : Type u₁} [] {X : C} {S : } {T : } (h : S T) :

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

Instances For
@[simp]
theorem CategoryTheory.Sieve.functorInclusion_app {C : Type u₁} [] {X : C} (S : ) (Y : Cᵒᵖ) (f : ().obj Y) :
Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types () (CategoryTheory.yoneda.obj X) () Y f = f
def CategoryTheory.Sieve.functorInclusion {C : Type u₁} [] {X : C} (S : ) :
CategoryTheory.yoneda.obj X

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

Instances For
theorem CategoryTheory.Sieve.natTransOfLe_comm {C : Type u₁} [] {X : C} {S : } {T : } (h : S T) :
instance CategoryTheory.Sieve.functorInclusion_is_mono {C : Type u₁} [] {X : C} {S : } :

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

@[simp]
theorem CategoryTheory.Sieve.sieveOfSubfunctor_apply {C : Type u₁} [] {X : C} {R : } (f : R CategoryTheory.yoneda.obj X) (Y : C) (g : Y X) :
().arrows g = t, Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types R (CategoryTheory.yoneda.obj X) f () t = g
def CategoryTheory.Sieve.sieveOfSubfunctor {C : Type u₁} [] {X : C} {R : } (f : R CategoryTheory.yoneda.obj X) :

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

Instances For