mathlib docs: category_theory.sites.sieves

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

category_theory.presieve X = Π ⦃Y : C⦄, set (Y ⟶ X)

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

category_theory.presieve.inhabited = {default := ⊤}

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

def category_theory.presieve.singleton {C : Type u} [category_theory.category C] {X Y : C} (f : Y ⟶ X) :

category_theory.presieve X

The singleton presieve.

Equations

category_theory.presieve.singleton f = λ (Z : C) (g : Z ⟶ X), ∃ (H : Z = Y), category_theory.eq_to_hom H ≫ f = g

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

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

Type (max u v)

arrows : category_theory.presieve 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

@[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

category_theory.sieve.has_coe_to_fun = {F := λ (x : category_theory.sieve X), category_theory.presieve X, coe := category_theory.sieve.arrows X}

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

category_theory.sieve.Sup 𝒮 = {arrows := λ (Y : C), {f : Y ⟶ X | ∃ (S : category_theory.sieve X) (H : S ∈ 𝒮), S.arrows f}, downward_closed' := _}

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

category_theory.sieve.Inf 𝒮 = {arrows := λ (Y : C), {f : Y ⟶ X | ∀ (S : category_theory.sieve X), S ∈ 𝒮 → S.arrows f}, downward_closed' := _}

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

S.union R = {arrows := λ (Y : C) (f : Y ⟶ X), ⇑S f ∨ ⇑R f, downward_closed' := _}

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

S.inter R = {arrows := λ (Y : C) (f : Y ⟶ X), ⇑S f ∧ ⇑R f, downward_closed' := _}

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

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 := _}

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

category_theory.sieve.sieve_inhabited = {default := ⊤}

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) f ↔ ∀ (S : category_theory.sieve X), S ∈ Ss → ⇑S 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) f ↔ ∃ (S : category_theory.sieve X) (H : S ∈ Ss), ⇑S 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) f ↔ ⇑R f ∧ ⇑S 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) f ↔ ⇑R f ∨ ⇑S f

source

@[simp]

theorem category_theory.sieve.mem_top {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

category_theory.sieve.generate R = {arrows := λ (Z : C) (f : Z ⟶ X), ∃ (Y : C) (h : Z ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f, downward_closed' := _}

source

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

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

category_theory.sieve.bind S R = {arrows := S.bind (λ (Y : C) (f : Y ⟶ X) (h : S f), ⇑(R h)), downward_closed' := _}

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

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 := _}

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

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

category_theory.sieve.pullback h S = {arrows := λ (Y_1 : C) (sl : Y_1 ⟶ Y), ⇑S (sl ≫ h), downward_closed' := _}

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) f ↔ ⇑S (f ≫ 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

category_theory.sieve.pushforward f R = {arrows := λ (Z : C) (gf : Z ⟶ X), ∃ (g : Z ⟶ Y), g ≫ f = gf ∧ ⇑R g, downward_closed' := _}

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

category_theory.sieve.galois_coinsertion_of_mono f = _.to_galois_coinsertion _

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

category_theory.sieve.galois_insertion_of_split_epi f = _.to_galois_insertion _

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

S.functor = {obj := λ (Y : Cᵒᵖ), {g // ⇑S g}, map := λ (Y Z : Cᵒᵖ) (f : Y ⟶ Z) (g : {g // ⇑S g}), ⟨f.unop ≫ g.val, _⟩, map_id' := _, map_comp' := _}

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

category_theory.sieve.nat_trans_of_le h = {app := λ (Y : Cᵒᵖ) (f : S.functor.obj Y), ⟨f.val, _⟩, naturality' := _}

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

S.functor_inclusion = {app := λ (Y : Cᵒᵖ) (f : S.functor.obj Y), f.val, naturality' := _}

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

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' := _}

source

@[simp]

theorem category_theory.sieve.sieve_of_subfunctor_apply {C : Type u} [category_theory.category C] {X Y : C} {R : Cᵒᵖ ⥤ Type v} (f : R ⟶ category_theory.yoneda.obj X) (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

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' := _}

mathlib documentation

Theory of sieves

Tags