mathlib documentation

category_theory.sites.sieves

Theory of sieves

Tags

sieve, pullback

source
structure category_theory.sieve {C : Type u} [category_theory.category C] (X : C) :
Type (max u v)
  • arrows : Π {Y : C}, set (Y ⟶ X)
  • downward_closed : ∀ {Y Z : C} {f : Y ⟶ X}, c.arrows f → ∀ (g : Z ⟶ Y), c.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.

source
def category_theory.sieve.set_over {C : Type u} [category_theory.category C] {X : C} (S : category_theory.sieve X) :
set (category_theory.over X)

A sieve gives a subset of the over category of X.

Equations
source
theorem category_theory.sieve.arrows_ext {C : Type u} [category_theory.category C] {X : C} {R S : category_theory.sieve X} (a : R.arrows = S.arrows) :
R = S

source
@[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.arrows f ↔ S.arrows f) :
R = S

source
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.arrows f ↔ S.arrows f

source
def category_theory.sieve.Sup {C : Type u} [category_theory.category C] {X : C} (𝒮 : set (category_theory.sieve X)) :
category_theory.sieve X

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

Equations
source
def category_theory.sieve.Inf {C : Type u} [category_theory.category C] {X : C} (𝒮 : set (category_theory.sieve X)) :
category_theory.sieve X

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

Equations
source
def category_theory.sieve.union {C : Type u} [category_theory.category C] {X : C} (S R : category_theory.sieve X) :
category_theory.sieve X

The union of two sieves is a sieve.

Equations
source
def category_theory.sieve.inter {C : Type u} [category_theory.category C] {X : C} (S R : category_theory.sieve X) :
category_theory.sieve X

The intersection of two sieves is a sieve.

Equations
source
@[instance]
def category_theory.sieve.complete_lattice {C : Type u} [category_theory.category C] {X : C} :
complete_lattice (category_theory.sieve X)

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

Equations
source
@[instance]
def category_theory.sieve.sieve_inhabited {C : Type u} [category_theory.category C] {X : C} :
inhabited (category_theory.sieve X)

The maximal sieve always exists.

Equations
source
@[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).arrows f ↔ ∀ (S : category_theory.sieve X), S ∈ Ss → S.arrows f

source
@[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).arrows f ↔ ∃ (S : category_theory.sieve X) (H : S ∈ Ss), S.arrows f

source
@[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).arrows f ↔ R.arrows f ∧ S.arrows f

source
@[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).arrows f ↔ R.arrows f ∨ S.arrows f

source
@[simp]
theorem category_theory.sieve.mem_top {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :
⊤.arrows f

source
inductive category_theory.sieve.generate_sets {C : Type u} [category_theory.category C] {X : C} (𝒢 : set (category_theory.over X)) (Y : C) :
set (Y ⟶ X)

Take the downward-closure of a set of morphisms to X.

source
def category_theory.sieve.generate {C : Type u} [category_theory.category C] {X : C} (𝒢 : set (category_theory.over X)) :
category_theory.sieve X

Generate the smallest sieve containing the given set of arrows.

Equations
source
theorem category_theory.sieve.sets_iff_generate {C : Type u} [category_theory.category C] {X : C} (S : set (category_theory.over X)) (S' : category_theory.sieve X) :
category_theory.sieve.generate S ≤ S' ↔ S ≤ S'.set_over

source
def category_theory.sieve.gi_generate {C : Type u} [category_theory.category C] {X : C} :
galois_insertion category_theory.sieve.generate category_theory.sieve.set_over

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

Equations
source
def category_theory.sieve.pullback {C : Type u} [category_theory.category C] {X Y : C} (h : Y ⟶ X) (S : category_theory.sieve X) :
category_theory.sieve Y

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
source
@[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} :
(category_theory.sieve.pullback h S).arrows f ↔ S.arrows (f ≫ h)

source
theorem category_theory.sieve.pullback_top {C : Type u} [category_theory.category C] {X Y : C} {f : Y ⟶ X} :
category_theory.sieve.pullback f ⊤ = ⊤

source
theorem category_theory.sieve.pullback_comp {C : Type u} [category_theory.category C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (S : category_theory.sieve X) :
category_theory.sieve.pullback (g ≫ f) S = category_theory.sieve.pullback g (category_theory.sieve.pullback f S)

source
theorem category_theory.sieve.pullback_inter {C : Type u} [category_theory.category C] {X Y : C} {f : Y ⟶ X} (S R : category_theory.sieve X) :
category_theory.sieve.pullback f (S ⊓ R) = category_theory.sieve.pullback f S ⊓ category_theory.sieve.pullback f R

source
theorem category_theory.sieve.id_mem_iff_eq_top {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} :
S.arrows (𝟙 X) ↔ S = ⊤

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

source
theorem category_theory.sieve.pullback_eq_top_iff_mem {C : Type u} [category_theory.category C] {X Y : C} {S : category_theory.sieve X} (f : Y ⟶ X) :
S.arrows f ↔ category_theory.sieve.pullback f S = ⊤

source
def category_theory.sieve.pushforward {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) (R : category_theory.sieve Y) :
category_theory.sieve X

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
source
@[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.arrows g) (f : Y ⟶ X) :
(category_theory.sieve.pushforward f R).arrows (g ≫ f)

source
theorem category_theory.sieve.pushforward_comp {C : Type u} [category_theory.category C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (R : category_theory.sieve Z) :
category_theory.sieve.pushforward (g ≫ f) R = category_theory.sieve.pushforward f (category_theory.sieve.pushforward g R)

source
theorem category_theory.sieve.galois_connection {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :
galois_connection (category_theory.sieve.pushforward f) (category_theory.sieve.pullback f)

source
theorem category_theory.sieve.pullback_monotone {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :
monotone (category_theory.sieve.pullback f)

source
theorem category_theory.sieve.pushforward_monotone {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :
monotone (category_theory.sieve.pushforward f)

source
theorem category_theory.sieve.le_pushforward_pullback {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) (R : category_theory.sieve Y) :
R ≤ category_theory.sieve.pullback f (category_theory.sieve.pushforward f R)

source
theorem category_theory.sieve.pullback_pushforward_le {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) (R : category_theory.sieve X) :
category_theory.sieve.pushforward f (category_theory.sieve.pullback f R) ≤ R

source
theorem category_theory.sieve.pushforward_union {C : Type u} [category_theory.category C] {X Y : C} {f : Y ⟶ X} (S R : category_theory.sieve Y) :
category_theory.sieve.pushforward f (S ⊔ R) = category_theory.sieve.pushforward f S ⊔ category_theory.sieve.pushforward f R

source
def category_theory.sieve.galois_coinsertion_of_mono {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) [category_theory.mono f] :
galois_coinsertion (category_theory.sieve.pushforward f) (category_theory.sieve.pullback f)

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

Equations
source
def category_theory.sieve.galois_insertion_of_split_epi {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) [category_theory.split_epi f] :
galois_insertion (category_theory.sieve.pushforward f) (category_theory.sieve.pullback f)

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

Equations
source
def category_theory.sieve.functor {C : Type u} [category_theory.category C] {X : C} (S : category_theory.sieve X) :
Cᵒᵖ ⥤ Type v

A sieve induces a presheaf.

Equations
source
@[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.arrows g}

source
@[simp]
theorem category_theory.sieve.functor_map_val {C : Type u} [category_theory.category C] {X : C} (S : category_theory.sieve X) (Y Z : Cᵒᵖ) (f : Y ⟶ Z) (g : {g // S.arrows g}) :
(S.functor.map f g).val = f.unop ≫ g.val

source
@[simp]
theorem category_theory.sieve.nat_trans_of_le_app_val {C : Type u} [category_theory.category C] {X : C} {S T : category_theory.sieve X} (h : S ≤ T) (Y : Cᵒᵖ) (f : S.functor.obj Y) :
((category_theory.sieve.nat_trans_of_le h).app Y f).val = f.val

source
def category_theory.sieve.nat_trans_of_le {C : Type u} [category_theory.category C] {X : C} {S T : category_theory.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
source
@[simp]
theorem category_theory.sieve.functor_inclusion_app {C : Type u} [category_theory.category C] {X : C} (S : category_theory.sieve X) (Y : Cᵒᵖ) (f : S.functor.obj Y) :
S.functor_inclusion.app Y f = f.val

source
def category_theory.sieve.functor_inclusion {C : Type u} [category_theory.category C] {X : C} (S : category_theory.sieve X) :
S.functor ⟶ category_theory.yoneda.obj X

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

Equations
source
theorem category_theory.sieve.nat_trans_of_le_comm {C : Type u} [category_theory.category C] {X : C} {S T : category_theory.sieve X} (h : S ≤ T) :
category_theory.sieve.nat_trans_of_le h ≫ T.functor_inclusion = S.functor_inclusion

source
@[instance]
def category_theory.sieve.functor_inclusion_is_mono {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} :
category_theory.mono S.functor_inclusion

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