mathlib documentation

category_theory.sites.sieves

Theory of sieves

Tags

sieve, pullback

def category_theory.presieve {C : Type u} [category_theory.category C] (X : C) :
Type (max u v)

A set of arrows all with codomain X.

Equations
def category_theory.presieve.bind {C : Type u} [category_theory.category C] {X : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S fcategory_theory.presieve Y) :

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} [category_theory.category C] {X Y Z : C} (f : Y X) {S : category_theory.presieve X} {R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S fcategory_theory.presieve Y} {g : Z Y} (h₁ : S f) (h₂ : R h₁ g) :
S.bind R (g f)

The singleton presieve.

Equations
structure category_theory.sieve {C : Type u} [category_theory.category C] (X : C) :
Type (max u v)

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

@[simp]
theorem category_theory.sieve.downward_closed {C : Type u} [category_theory.category C] {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} [category_theory.category C] {X : C} {R S : category_theory.sieve X} :
R.arrows = S.arrowsR = S

@[ext]
theorem category_theory.sieve.ext {C : Type u} [category_theory.category C] {X : C} {R S : category_theory.sieve X} (h : ∀ ⦃Y : C⦄ (f : Y X), R f S f) :
R = S

theorem category_theory.sieve.ext_iff {C : Type u} [category_theory.category C] {X : C} {R S : category_theory.sieve X} :
R = S ∀ ⦃Y : C⦄ (f : Y X), R f S f

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

Equations

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

Equations

The union of two sieves is a sieve.

Equations

The intersection of two sieves is a sieve.

Equations
@[instance]

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

Equations
@[instance]

The maximal sieve always exists.

Equations
@[simp]
theorem category_theory.sieve.mem_Inf {C : Type u} [category_theory.category C] {X : C} {Ss : set (category_theory.sieve X)} {Y : C} (f : Y X) :
(Inf Ss) f ∀ (S : category_theory.sieve X), S SsS f

@[simp]
theorem category_theory.sieve.mem_Sup {C : Type u} [category_theory.category C] {X : C} {Ss : set (category_theory.sieve X)} {Y : C} (f : Y X) :
(Sup Ss) f ∃ (S : category_theory.sieve X) (H : S Ss), S f

@[simp]
theorem category_theory.sieve.mem_inter {C : Type u} [category_theory.category C] {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.mem_union {C : Type u} [category_theory.category C] {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.mem_top {C : Type u} [category_theory.category C] {X Y : C} (f : Y X) :

Generate the smallest sieve containing the given set of arrows.

Equations
theorem category_theory.sieve.mem_generate {C : Type u} [category_theory.category C] {X Z : C} (R : category_theory.presieve X) (f : Z X) :
(category_theory.sieve.generate R) f ∃ (Y : C) (h : Z Y) (g : Y X), R g h g = f

def category_theory.sieve.bind {C : Type u} [category_theory.category C] {X : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S fcategory_theory.sieve Y) :

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

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

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

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.mem_pullback {C : Type u} [category_theory.category C] {X Y Z : C} {S : category_theory.sieve X} (h : Y X) {f : Z 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.mem_pushforward_of_comp {C : Type u} [category_theory.category C] {X Y : C} {R : category_theory.sieve Y} {Z : C} {g : Z Y} (hg : R g) (f : Y X) :

theorem category_theory.sieve.pushforward_le_bind_of_mem {C : Type u} [category_theory.category C] {X Y : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S fcategory_theory.sieve Y) (f : Y X) (h : S f) :

theorem category_theory.sieve.le_pullback_bind {C : Type u} [category_theory.category C] {X Y : C} (S : category_theory.presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y X⦄, S fcategory_theory.sieve Y) (f : Y X) (h : S f) :

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

Equations

A sieve induces a presheaf.

Equations
@[simp]
theorem category_theory.sieve.functor_obj {C : Type u} [category_theory.category C] {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} [category_theory.category C] {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

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

Equations

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

Equations
@[instance]

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

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]