# mathlibdocumentation

category_theory.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 category_theory.presieve {C : Type u₁} (X : C) :
Type (max u₁ v₁)

A set of arrows all with codomain X.

Equations
Instances for category_theory.presieve
@[protected, instance]
def category_theory.presieve.complete_lattice {C : Type u₁} (X : C) :
@[protected, instance]
def category_theory.presieve.inhabited {C : Type u₁} {X : C} :
Equations
@[reducible]
def category_theory.presieve.diagram {C : Type u₁} {X : C} (S : category_theory.presieve X) :

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.

@[reducible]
def category_theory.presieve.cocone {C : Type u₁} {X : C} (S : category_theory.presieve X) :

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.

def category_theory.presieve.bind {C : Type u₁} {X : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S 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 }.

Equations
• S.bind R = λ (Z : C) (h : Z X), ∃ (Y : C) (g : Z Y) (f : Y X) (H : S f), R H g g f = h
@[simp]
theorem category_theory.presieve.bind_comp {C : Type u₁} {X Y Z : C} (f : Y X) {S : category_theory.presieve X} {R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S f} {g : Z Y} (h₁ : S f) (h₂ : R h₁ g) :
S.bind R (g f)
inductive category_theory.presieve.singleton {C : Type u₁} {X Y : C} (f : Y X) :
• mk : ∀ {C : Type u₁} [_inst_1 : {X Y : C} {f : Y X},

The singleton presieve.

@[simp]
theorem category_theory.presieve.singleton_eq_iff_domain {C : Type u₁} {X Y : C} (f g : Y X) :
theorem category_theory.presieve.singleton_self {C : Type u₁} {X Y : C} (f : Y X) :
inductive category_theory.presieve.pullback_arrows {C : Type u₁} {X Y : C} (f : Y X) (R : category_theory.presieve X) :
• mk : ∀ {C : Type u₁} [_inst_1 : {X Y : C} {f : Y X} [_inst_3 : {R : (Z : C) (h : Z X),

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 pullback_arrows_comm.

theorem category_theory.presieve.pullback_singleton {C : Type u₁} {X Y Z : C} (f : Y X) (g : Z X) :
inductive category_theory.presieve.of_arrows {C : Type u₁} {X : C} {ι : Type u_1} (Y : ι → C) (f : Π (i : ι), Y i X) :
• mk : ∀ {C : Type u₁} [_inst_1 : {X : C} {ι : Type u_1} {Y : ι → C} {f : Π (i : ι), Y i X} (i : ι), (f i)

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

theorem category_theory.presieve.of_arrows_punit {C : Type u₁} {X Y : C} (f : Y X) :
category_theory.presieve.of_arrows (λ (_x : punit), Y) (λ (_x : punit), f) =
theorem category_theory.presieve.of_arrows_pullback {C : Type u₁} {X Y : C} (f : Y X) {ι : Type u_1} (Z : ι → C) (g : Π (i : ι), Z i X) :
theorem category_theory.presieve.of_arrows_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 f H → C) (k : Π ⦃Y : C⦄ (f : Y X) (H : (i : j f H), W f H i Y) :
(λ (Y : C) (f : Y X) (H : , (k f H)) = category_theory.presieve.of_arrows (λ (i : Σ (i : ι), j (g i) _), W (g i.fst) _ i.snd) (λ (ij : Σ (i : ι), j (g i) _), k (g ij.fst) _ ij.snd g ij.fst)
def category_theory.presieve.functor_pullback {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.presieve (F.obj X)) :

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

Equations
• = λ (_x : C) (f : _x X), R (F.map f)
@[simp]
theorem category_theory.presieve.functor_pullback_mem {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.presieve (F.obj X)) {Y : C} (f : Y X) :
R (F.map f)
@[simp]
theorem category_theory.presieve.functor_pullback_id {C : Type u₁} {X : C} (R : category_theory.presieve X) :
def category_theory.presieve.functor_pushforward {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (S : category_theory.presieve X) :

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.

Equations
@[nolint]
structure category_theory.presieve.functor_pushforward_structure {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (S : category_theory.presieve X) {Y : D} (f : Y F.obj X) :
Type (max u₁ v₁ v₂)

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

Instances for category_theory.presieve.functor_pushforward_structure
• category_theory.presieve.functor_pushforward_structure.has_sizeof_inst
noncomputable def category_theory.presieve.get_functor_pushforward_structure {C : Type u₁} {D : Type u₂} {X : C} {F : C D} {S : category_theory.presieve X} {Y : D} {f : Y F.obj X}  :

The fixed choice of a preimage.

Equations
theorem category_theory.presieve.functor_pushforward_comp {C : Type u₁} {D : Type u₂} (F : C D) {X : C} {E : Type u₃} (G : D E) (R : category_theory.presieve X) :
theorem category_theory.presieve.image_mem_functor_pushforward {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (R : category_theory.presieve X) {f : Y X} (h : R f) :
structure category_theory.sieve {C : Type u₁} (X : C) :
Type (max u₁ v₁)
• arrows :
• downward_closed' : ∀ {Y Z : C} {f : Y X}, self.arrows f∀ (g : Z Y), self.arrows (g f)

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 category_theory.sieve
@[protected, instance]
def category_theory.sieve.has_coe_to_fun {C : Type u₁} {X : C} :
(λ (_x : ,
Equations
@[simp]
theorem category_theory.sieve.downward_closed {C : Type u₁} {X Y Z : C} (S : category_theory.sieve X) {f : Y X} (hf : S f) (g : Z Y) :
S (g f)
theorem category_theory.sieve.arrows_ext {C : Type u₁} {X : C} {R S : category_theory.sieve X} :
R.arrows = S.arrowsR = S
@[protected, ext]
theorem category_theory.sieve.ext {C : Type u₁} {X : C} {R S : category_theory.sieve X} (h : ∀ ⦃Y : C⦄ (f : Y X), R f S f) :
R = S
@[protected]
theorem category_theory.sieve.ext_iff {C : Type u₁} {X : C} {R S : category_theory.sieve X} :
R = S ∀ ⦃Y : C⦄ (f : Y X), R f S f
@[protected]
def category_theory.sieve.Sup {C : Type u₁} {X : C} (𝒮 : set ) :

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

Equations
@[protected]
def category_theory.sieve.Inf {C : Type u₁} {X : C} (𝒮 : set ) :

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

Equations
@[protected]
def category_theory.sieve.union {C : Type u₁} {X : C} (S R : category_theory.sieve X) :

The union of two sieves is a sieve.

Equations
@[protected]
def category_theory.sieve.inter {C : Type u₁} {X : C} (S R : category_theory.sieve X) :

The intersection of two sieves is a sieve.

Equations
@[protected, instance]
def category_theory.sieve.complete_lattice {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.

Equations
@[protected, instance]
def category_theory.sieve.sieve_inhabited {C : Type u₁} {X : C} :

The maximal sieve always exists.

Equations
@[simp]
theorem category_theory.sieve.Inf_apply {C : Type u₁} {X : C} {Ss : set } {Y : C} (f : Y X) :
(has_Inf.Inf Ss) f ∀ (S : , S SsS f
@[simp]
theorem category_theory.sieve.Sup_apply {C : Type u₁} {X : C} {Ss : set } {Y : C} (f : Y X) :
(has_Sup.Sup Ss) f ∃ (S : (H : S Ss), S f
@[simp]
theorem category_theory.sieve.inter_apply {C : Type u₁} {X : C} {R S : category_theory.sieve X} {Y : C} (f : Y X) :
(R S) f R f S f
@[simp]
theorem category_theory.sieve.union_apply {C : Type u₁} {X : C} {R S : category_theory.sieve X} {Y : C} (f : Y X) :
(R S) f R f S f
@[simp]
theorem category_theory.sieve.top_apply {C : Type u₁} {X Y : C} (f : Y X) :
def category_theory.sieve.generate {C : Type u₁} {X : C} (R : category_theory.presieve X) :

Generate the smallest sieve containing the given set of arrows.

Equations
@[simp]
theorem category_theory.sieve.generate_apply {C : Type u₁} {X : C} (R : category_theory.presieve X) (Z : C) (f : Z X) :
= ∃ (Y : C) (h : Z Y) (g : Y X), R g h g = f
@[simp]
theorem category_theory.sieve.bind_apply {C : Type u₁} {X : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S f) :
= S.bind (λ (Y : C) (f : Y X) (h : S f), (R h))
def category_theory.sieve.bind {C : Type u₁} {X : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S 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.

Equations

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

Equations
theorem category_theory.sieve.le_generate {C : Type u₁} {X : C} (R : category_theory.presieve X) :
@[simp]
theorem category_theory.sieve.generate_sieve {C : Type u₁} {X : C} (S : category_theory.sieve X) :
theorem category_theory.sieve.id_mem_iff_eq_top {C : Type u₁} {X : C} {S : category_theory.sieve X} :
S (𝟙 X) S =

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

theorem category_theory.sieve.generate_of_contains_is_split_epi {C : Type u₁} {X Y : C} {R : category_theory.presieve X} (f : Y X) (hf : R f) :

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

@[simp]
theorem category_theory.sieve.generate_of_singleton_is_split_epi {C : Type u₁} {X Y : C} (f : Y X)  :
@[simp]
theorem category_theory.sieve.generate_top {C : Type u₁} {X : C} :
def category_theory.sieve.pullback {C : Type u₁} {X Y : C} (h : Y X) (S : category_theory.sieve X) :

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.

Equations
@[simp]
theorem category_theory.sieve.pullback_apply {C : Type u₁} {X Y : C} (h : Y X) (S : category_theory.sieve X) (Y_1 : C) (sl : Y_1 Y) :
sl = S (sl h)
@[simp]
theorem category_theory.sieve.pullback_id {C : Type u₁} {X : C} {S : category_theory.sieve X} :
= S
@[simp]
theorem category_theory.sieve.pullback_top {C : Type u₁} {X Y : C} {f : Y X} :
theorem category_theory.sieve.pullback_comp {C : Type u₁} {X Y Z : C} {f : Y X} {g : Z Y} (S : category_theory.sieve X) :
@[simp]
theorem category_theory.sieve.pullback_inter {C : Type u₁} {X Y : C} {f : Y X} (S R : category_theory.sieve X) :
theorem category_theory.sieve.pullback_eq_top_iff_mem {C : Type u₁} {X Y : C} {S : category_theory.sieve X} (f : Y X) :
S f
theorem category_theory.sieve.pullback_eq_top_of_mem {C : Type u₁} {X Y : C} (S : category_theory.sieve X) {f : Y X} :
S f
def category_theory.sieve.pushforward {C : Type u₁} {X Y : C} (f : Y X) (R : category_theory.sieve Y) :

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.

Equations
@[simp]
theorem category_theory.sieve.pushforward_apply {C : Type u₁} {X Y : C} (f : Y X) (R : category_theory.sieve Y) (Z : C) (gf : Z X) :
= ∃ (g : Z Y), g f = gf R g
theorem category_theory.sieve.pushforward_apply_comp {C : Type u₁} {X Y : C} {R : category_theory.sieve Y} {Z : C} {g : Z Y} (hg : R g) (f : Y X) :
(g f)
theorem category_theory.sieve.pushforward_comp {C : Type u₁} {X Y Z : C} {f : Y X} {g : Z Y} (R : category_theory.sieve Z) :
theorem category_theory.sieve.galois_connection {C : Type u₁} {X Y : C} (f : Y X) :
theorem category_theory.sieve.pullback_monotone {C : Type u₁} {X Y : C} (f : Y X) :
theorem category_theory.sieve.pushforward_monotone {C : Type u₁} {X Y : C} (f : Y X) :
theorem category_theory.sieve.le_pushforward_pullback {C : Type u₁} {X Y : C} (f : Y X) (R : category_theory.sieve Y) :
theorem category_theory.sieve.pullback_pushforward_le {C : Type u₁} {X Y : C} (f : Y X) (R : category_theory.sieve X) :
theorem category_theory.sieve.pushforward_union {C : Type u₁} {X Y : C} {f : Y X} (S R : category_theory.sieve Y) :
theorem category_theory.sieve.pushforward_le_bind_of_mem {C : Type u₁} {X Y : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S f) (f : Y X) (h : S f) :
theorem category_theory.sieve.le_pullback_bind {C : Type u₁} {X Y : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S f) (f : Y X) (h : S f) :
def category_theory.sieve.galois_coinsertion_of_mono {C : Type u₁} {X Y : C} (f : Y X)  :

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

Equations
def category_theory.sieve.galois_insertion_of_is_split_epi {C : Type u₁} {X Y : C} (f : Y X)  :

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

Equations
theorem category_theory.sieve.pullback_arrows_comm {C : Type u₁} {X Y : C} (f : Y X) (R : category_theory.presieve X) :
def category_theory.sieve.functor_pullback {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.sieve (F.obj X)) :

If R is a sieve, then the category_theory.presieve.functor_pullback of R is actually a sieve.

Equations
@[simp]
theorem category_theory.sieve.functor_pullback_apply {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.sieve (F.obj X)) :
@[simp]
theorem category_theory.sieve.functor_pullback_arrows {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.sieve (F.obj X)) :
@[simp]
theorem category_theory.sieve.functor_pullback_id {C : Type u₁} {X : C} (R : category_theory.sieve X) :
theorem category_theory.sieve.functor_pullback_comp {C : Type u₁} {D : Type u₂} (F : C D) {X : C} {E : Type u₃} (G : D E) (R : category_theory.sieve ((F G).obj X)) :
theorem category_theory.sieve.functor_pushforward_extend_eq {C : Type u₁} {D : Type u₂} (F : C D) {X : C} {R : category_theory.presieve X} :
@[simp]
theorem category_theory.sieve.functor_pushforward_apply {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.sieve X) :
def category_theory.sieve.functor_pushforward {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.sieve X) :

The sieve generated by the image of R under F.

Equations
@[simp]
theorem category_theory.sieve.functor_pushforward_id {C : Type u₁} {X : C} (R : category_theory.sieve X) :
theorem category_theory.sieve.functor_pushforward_comp {C : Type u₁} {D : Type u₂} (F : C D) {X : C} {E : Type u₃} (G : D E) (R : category_theory.sieve X) :
theorem category_theory.sieve.functor_galois_connection {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
theorem category_theory.sieve.functor_pullback_monotone {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
theorem category_theory.sieve.functor_pushforward_monotone {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
theorem category_theory.sieve.le_functor_pushforward_pullback {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.sieve X) :
theorem category_theory.sieve.functor_pullback_pushforward_le {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.sieve (F.obj X)) :
theorem category_theory.sieve.functor_pushforward_union {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (S R : category_theory.sieve X) :
theorem category_theory.sieve.functor_pullback_union {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (S R : category_theory.sieve (F.obj X)) :
theorem category_theory.sieve.functor_pullback_inter {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (S R : category_theory.sieve (F.obj X)) :
@[simp]
theorem category_theory.sieve.functor_pushforward_bot {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
@[simp]
theorem category_theory.sieve.functor_pushforward_top {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
@[simp]
theorem category_theory.sieve.functor_pullback_bot {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
@[simp]
theorem category_theory.sieve.functor_pullback_top {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
theorem category_theory.sieve.image_mem_functor_pushforward {C : Type u₁} {D : Type u₂} (F : C D) {X : C} (R : category_theory.sieve X) {V : C} {f : V X} (h : R f) :
(F.map f)
def category_theory.sieve.ess_surj_full_functor_galois_insertion {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :

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

Equations
def category_theory.sieve.fully_faithful_functor_galois_coinsertion {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :

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

Equations
def category_theory.sieve.functor {C : Type u₁} {X : C} (S : category_theory.sieve X) :
Cᵒᵖ Type v₁

A sieve induces a presheaf.

Equations
@[simp]
theorem category_theory.sieve.functor_obj {C : Type u₁} {X : C} (S : category_theory.sieve X) (Y : Cᵒᵖ) :
S.functor.obj Y = {g // S g}
@[simp]
theorem category_theory.sieve.functor_map_coe {C : Type u₁} {X : C} (S : category_theory.sieve X) (Y Z : Cᵒᵖ) (f : Y Z) (g : {g // S g}) :
(S.functor.map f g) = f.unop g.val
@[simp]
theorem category_theory.sieve.nat_trans_of_le_app_coe {C : Type u₁} {X : C} {S T : category_theory.sieve X} (h : S T) (Y : Cᵒᵖ) (f : S.functor.obj Y) :
f) = f.val
def category_theory.sieve.nat_trans_of_le {C : Type u₁} {X : C} {S T : category_theory.sieve X} (h : S T) :

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

Equations
@[simp]
theorem category_theory.sieve.functor_inclusion_app {C : Type u₁} {X : C} (S : category_theory.sieve X) (Y : Cᵒᵖ) (f : S.functor.obj Y) :
f = f.val
def category_theory.sieve.functor_inclusion {C : Type u₁} {X : C} (S : category_theory.sieve X) :

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

Equations
Instances for category_theory.sieve.functor_inclusion
theorem category_theory.sieve.nat_trans_of_le_comm {C : Type u₁} {X : C} {S T : category_theory.sieve X} (h : S T) :
@[protected, instance]

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

def category_theory.sieve.sieve_of_subfunctor {C : Type u₁} {X : C} {R : Cᵒᵖ Type v₁} (f : R ) :

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

Equations
@[simp]
theorem category_theory.sieve.sieve_of_subfunctor_apply {C : Type u₁} {X : C} {R : Cᵒᵖ Type v₁} (f : R ) (Y : C) (g : Y X) :
= ∃ (t : R.obj (opposite.op Y)), f.app (opposite.op Y) t = g
@[protected, instance]