mathlib documentation

category_theory.sites.sieves

Theory of sieves #

Tags #

sieve, pullback

source
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
source
@[instance]
def category_theory.presieve.complete_lattice {C : Type u} [category_theory.category C] (X : C) :
complete_lattice (category_theory.presieve X)
source
@[instance]
def category_theory.presieve.inhabited {C : Type u} [category_theory.category C] {X : C} :
inhabited (category_theory.presieve X)
Equations
source
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 f → category_theory.presieve Y) :
category_theory.presieve X

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
source
@[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 f → category_theory.presieve Y} {g : Z ⟶ Y} (h₁ : S f) (h₂ : R h₁ g) :
S.bind R (g ≫ f)
source
inductive category_theory.presieve.singleton {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :
category_theory.presieve X

The singleton presieve.

source
@[simp]
theorem category_theory.presieve.singleton_eq_iff_domain {C : Type u} [category_theory.category C] {X Y : C} (f g : Y ⟶ X) :
category_theory.presieve.singleton f g ↔ f = g
source
theorem category_theory.presieve.singleton_self {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :
category_theory.presieve.singleton f f
source
inductive category_theory.presieve.pullback_arrows {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) [category_theory.limits.has_pullbacks C] (R : category_theory.presieve X) :
category_theory.presieve Y

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.

source
theorem category_theory.presieve.pullback_singleton {C : Type u} [category_theory.category C] {X Y Z : C} (f : Y ⟶ X) [category_theory.limits.has_pullbacks C] (g : Z ⟶ X) :
category_theory.presieve.pullback_arrows f (category_theory.presieve.singleton g) = category_theory.presieve.singleton category_theory.limits.pullback.snd
source
inductive category_theory.presieve.of_arrows {C : Type u} [category_theory.category C] {X : C} {ι : Type u_1} (Y : ι → C) (f : Π (i : ι), Y i ⟶ X) :
category_theory.presieve X

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

source
theorem category_theory.presieve.of_arrows_punit {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :
category_theory.presieve.of_arrows (λ (_x : punit), Y) (λ (_x : punit), f) = category_theory.presieve.singleton f
source
theorem category_theory.presieve.of_arrows_pullback {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) [category_theory.limits.has_pullbacks C] {ι : Type u_1} (Z : ι → C) (g : Π (i : ι), Z i ⟶ X) :
category_theory.presieve.of_arrows (λ (i : ι), category_theory.limits.pullback (g i) f) (λ (i : ι), category_theory.limits.pullback.snd) = category_theory.presieve.pullback_arrows f (category_theory.presieve.of_arrows Z g)
source
theorem category_theory.presieve.of_arrows_bind {C : Type u} [category_theory.category C] {X : C} {ι : Type u_1} (Z : ι → C) (g : Π (i : ι), Z i ⟶ X) (j : Π ⦃Y : C⦄ (f : Y ⟶ X), category_theory.presieve.of_arrows Z g f → Type u_2) (W : Π ⦃Y : C⦄ (f : Y ⟶ X) (H : category_theory.presieve.of_arrows Z g f), j f H → C) (k : Π ⦃Y : C⦄ (f : Y ⟶ X) (H : category_theory.presieve.of_arrows Z g f) (i : j f H), W f H i ⟶ Y) :
(category_theory.presieve.of_arrows Z g).bind (λ (Y : C) (f : Y ⟶ X) (H : category_theory.presieve.of_arrows Z g f), category_theory.presieve.of_arrows (W f 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)
source
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.

source
@[instance]
def category_theory.sieve.has_coe_to_fun {C : Type u} [category_theory.category C] {X : C} :
has_coe_to_fun (category_theory.sieve X)
Equations
source
@[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)
source
theorem category_theory.sieve.arrows_ext {C : Type u} [category_theory.category C] {X : C} {R S : category_theory.sieve X} :
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 f ↔ ⇑S 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 f ↔ ⇑S 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.Inf_apply {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 ∈ Ss → ⇑S f
source
@[simp]
theorem category_theory.sieve.Sup_apply {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
source
@[simp]
theorem category_theory.sieve.inter_apply {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
source
@[simp]
theorem category_theory.sieve.union_apply {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
source
@[simp]
theorem category_theory.sieve.top_apply {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :
⇑⊤ f
source
def category_theory.sieve.generate {C : Type u} [category_theory.category C] {X : C} (R : category_theory.presieve X) :
category_theory.sieve X

Generate the smallest sieve containing the given set of arrows.

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

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
source
theorem category_theory.sieve.sets_iff_generate {C : Type u} [category_theory.category C] {X : C} (R : category_theory.presieve X) (S : category_theory.sieve X) :
category_theory.sieve.generate R ≤ S ↔ R ≤ ⇑S
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.arrows

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

Equations
source
theorem category_theory.sieve.le_generate {C : Type u} [category_theory.category C] {X : C} (R : category_theory.presieve X) :
R ≤ ⇑(category_theory.sieve.generate R)
source
@[simp]
theorem category_theory.sieve.generate_sieve {C : Type u} [category_theory.category C] {X : C} (S : category_theory.sieve X) :
category_theory.sieve.generate ⇑S = S
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 (𝟙 X) ↔ S = ⊤

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

source
theorem category_theory.sieve.generate_of_contains_split_epi {C : Type u} [category_theory.category C] {X Y : C} {R : category_theory.presieve X} (f : Y ⟶ X) [category_theory.split_epi f] (hf : R f) :
category_theory.sieve.generate R = ⊤

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

source
@[simp]
theorem category_theory.sieve.generate_of_singleton_split_epi {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) [category_theory.split_epi f] :
category_theory.sieve.generate (category_theory.presieve.singleton f) = ⊤
source
@[simp]
theorem category_theory.sieve.generate_top {C : Type u} [category_theory.category C] {X : C} :
category_theory.sieve.generate ⊤ = ⊤
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.pullback_apply {C : Type u} [category_theory.category C] {X Y : C} (h : Y ⟶ X) (S : category_theory.sieve X) (Y_1 : C) (sl : Y_1 ⟶ Y) :
⇑(category_theory.sieve.pullback h S) sl = ⇑S (sl ≫ h)
source
@[simp]
theorem category_theory.sieve.pullback_id {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} :
category_theory.sieve.pullback (𝟙 X) S = S
source
@[simp]
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
@[simp]
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.pullback_eq_top_iff_mem {C : Type u} [category_theory.category C] {X Y : C} {S : category_theory.sieve X} (f : Y ⟶ X) :
⇑S f ↔ category_theory.sieve.pullback f S = ⊤
source
theorem category_theory.sieve.pullback_eq_top_of_mem {C : Type u} [category_theory.category C] {X Y : C} (S : category_theory.sieve X) {f : Y ⟶ X} :
⇑S 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.pushforward_apply {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) (R : category_theory.sieve Y) (Z : C) (gf : Z ⟶ X) :
⇑(category_theory.sieve.pushforward f R) gf = ∃ (g : Z ⟶ Y), g ≫ f = gf ∧ ⇑R g
source
theorem category_theory.sieve.pushforward_apply_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) :
⇑(category_theory.sieve.pushforward f R) (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
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 f → category_theory.sieve Y) (f : Y ⟶ X) (h : S f) :
category_theory.sieve.pushforward f (R h) ≤ category_theory.sieve.bind S R
source
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 f → category_theory.sieve Y) (f : Y ⟶ X) (h : S f) :
R h ≤ category_theory.sieve.pullback f (category_theory.sieve.bind S 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
theorem category_theory.sieve.pullback_arrows_comm {C : Type u} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y : C} (f : Y ⟶ X) (R : category_theory.presieve X) :
category_theory.sieve.generate (category_theory.presieve.pullback_arrows f R) = category_theory.sieve.pullback f (category_theory.sieve.generate R)
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 g}
source
@[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
source
@[simp]
theorem category_theory.sieve.nat_trans_of_le_app_coe {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) = 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.

source
def category_theory.sieve.sieve_of_subfunctor {C : Type u} [category_theory.category C] {X : C} {R : Cᵒᵖ ⥤ Type v} (f : R ⟶ category_theory.yoneda.obj X) :
category_theory.sieve X

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
source
@[simp]
theorem category_theory.sieve.sieve_of_subfunctor_apply {C : Type u} [category_theory.category C] {X : C} {R : Cᵒᵖ ⥤ Type v} (f : R ⟶ category_theory.yoneda.obj X) (Y : C) (g : Y ⟶ X) :
⇑(category_theory.sieve.sieve_of_subfunctor f) g = ∃ (t : R.obj (opposite.op Y)), f.app (opposite.op Y) t = g
source
theorem category_theory.sieve.sieve_of_subfunctor_functor_inclusion {C : Type u} [category_theory.category C] {X : C} {S : category_theory.sieve X} :
category_theory.sieve.sieve_of_subfunctor S.functor_inclusion = S
source
@[instance]
def category_theory.sieve.functor_inclusion_top_is_iso {C : Type u} [category_theory.category C] {X : C} :
category_theory.is_iso ⊤.functor_inclusion