Theory of sieves #
- For an object
X
of a categoryC
, asieve X
is a set of morphisms toX
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 onC
together with a monomorphism to the yoneda embedding ofX
.
Tags #
sieve, pullback
A set of arrows all with codomain X
.
Equations
- category_theory.presieve X = Π ⦃Y : C⦄, set (Y ⟶ X)
Equations
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 }
.
- mk : ∀ {C : Type u} [_inst_1 : category_theory.category C] {X Y : C} (f : Y ⟶ X), category_theory.presieve.singleton f f
The singleton presieve.
Equations
- category_theory.sieve.has_coe_to_fun = {F := λ (x : category_theory.sieve X), category_theory.presieve X, coe := category_theory.sieve.arrows X}
The supremum of a collection of sieves: the union of them all.
Equations
- category_theory.sieve.Sup 𝒮 = {arrows := λ (Y : C), {f : Y ⟶ X | ∃ (S : category_theory.sieve X) (H : S ∈ 𝒮), S.arrows f}, downward_closed' := _}
The infimum of a collection of sieves: the intersection of them all.
Equations
- category_theory.sieve.Inf 𝒮 = {arrows := λ (Y : C), {f : Y ⟶ X | ∀ (S : category_theory.sieve X), S ∈ 𝒮 → S.arrows f}, downward_closed' := _}
The union of two sieves is a sieve.
The intersection of two sieves is a sieve.
Sieves on an object X
form a complete lattice.
We generate this directly rather than using the galois insertion for nicer definitional properties.
Equations
- category_theory.sieve.complete_lattice = {sup := category_theory.sieve.union X, le := λ (S R : category_theory.sieve X), ∀ ⦃Y : C⦄ (f : Y ⟶ X), ⇑S f → ⇑R f, lt := bounded_lattice.lt._default (λ (S R : category_theory.sieve X), ∀ ⦃Y : C⦄ (f : Y ⟶ X), ⇑S f → ⇑R f), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := category_theory.sieve.inter X, inf_le_left := _, inf_le_right := _, le_inf := _, top := {arrows := λ (_x : C), set.univ, downward_closed' := _}, le_top := _, bot := {arrows := λ (_x : C), ∅, downward_closed' := _}, bot_le := _, Sup := category_theory.sieve.Sup X, Inf := category_theory.sieve.Inf X, le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
The maximal sieve always exists.
Equations
Generate the smallest sieve containing the given set of arrows.
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
- category_theory.sieve.bind S R = {arrows := S.bind (λ (Y : C) (f : Y ⟶ X) (h : S f), ⇑(R h)), downward_closed' := _}
Show that there is a galois insertion (generate, set_over).
Equations
- category_theory.sieve.gi_generate = {choice := λ (𝒢 : category_theory.presieve X) (_x : (category_theory.sieve.generate 𝒢).arrows ≤ 𝒢), category_theory.sieve.generate 𝒢, gc := _, le_l_u := _, choice_eq := _}
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
- category_theory.sieve.pullback h S = {arrows := λ (Y_1 : C) (sl : Y_1 ⟶ Y), ⇑S (sl ≫ h), downward_closed' := _}
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
.
If f
is a monomorphism, the pushforward-pullback adjunction on sieves is coreflective.
Equations
If f
is a split epi, the pushforward-pullback adjunction on sieves is reflective.
Equations
A sieve induces a presheaf.
If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced presheaves.
Equations
- category_theory.sieve.nat_trans_of_le h = {app := λ (Y : Cᵒᵖ) (f : S.functor.obj Y), ⟨f.val, _⟩, naturality' := _}
The natural inclusion from the functor induced by a sieve to the yoneda embedding.
Equations
- S.functor_inclusion = {app := λ (Y : Cᵒᵖ) (f : S.functor.obj Y), f.val, naturality' := _}
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
- category_theory.sieve.sieve_of_subfunctor f = {arrows := λ (Y : C) (g : Y ⟶ X), ∃ (t : R.obj (opposite.op Y)), f.app (opposite.op Y) t = g, downward_closed' := _}
Equations
- category_theory.sieve.functor_inclusion_top_is_iso = {inv := {app := λ (Y : Cᵒᵖ) (a : (category_theory.yoneda.obj X).obj Y), ⟨a, true.intro⟩, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}