Sieves

For an object X of a category C, a sieve on X is a presieve on X, i.e. a predicate on morphisms with codomain X, with the additional property of being closed under precomposition. Thus a sieve records a collection of arrows into X that is stable under passing to further refinements.

This file develops the basic theory of sieves. It gives Sieve X its complete lattice structure and defines Sieve.generate, the smallest sieve containing a presieve. Generation and the underlying-arrow presieve form a Galois insertion. The file also constructs sieves from indexed families of arrows or objects, and defines pullback and pushforward along a fixed morphism together with their Galois connection.

Operations induced by functors between categories are developed in Mathlib.CategoryTheory.Sites.Sieves.Functoriality, while the presheaf associated to a sieve is developed in Mathlib.CategoryTheory.Sites.Sieves.Presheaf.

Tags

sieve, pullback

structure CategoryTheory.Sieve {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : Type (max u₁ v₁)

For an object X of a category C, a Sieve X is a predicate on morphisms to X which is closed under left-composition.

• arrows : Presieve X

  the underlying presieve

• downward_closed {Y Z : C} {f : Y ⟶ X} : self.arrows f → ∀ (g : Z ⟶ Y), self.arrows (CategoryStruct.comp g f)

  stability by precomposition

@[instance_reducible]

instance CategoryTheory.Sieve.instCoeFunPresieve {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : CoeFun (Sieve X) fun (x : Sieve X) => Presieve X

Equations

• CategoryTheory.Sieve.instCoeFunPresieve = { coe := CategoryTheory.Sieve.arrows }

theorem CategoryTheory.Sieve.arrows_ext {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R S : Sieve X} : R.arrows = S.arrows → R = S

theorem CategoryTheory.Sieve.ext {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R S : Sieve X} (h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f) : R = S

theorem CategoryTheory.Sieve.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R S : Sieve X} : R = S ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f

def CategoryTheory.Sieve.sup {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (𝒮 : Set (Sieve X)) : Sieve X

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

Equations

• CategoryTheory.Sieve.sup 𝒮 = { arrows := fun (x : C) (f : x ⟶ X) => ∃ S ∈ 𝒮, S.arrows f, downward_closed := ⋯ }

def CategoryTheory.Sieve.inf {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (𝒮 : Set (Sieve X)) : Sieve X

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

Equations

• CategoryTheory.Sieve.inf 𝒮 = { arrows := fun (x : C) (f : x ⟶ X) => ∀ S ∈ 𝒮, S.arrows f, downward_closed := ⋯ }

def CategoryTheory.Sieve.union {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S R : Sieve X) : Sieve X

The union of two sieves is a sieve.

Equations

• S.union R = { arrows := fun (x : C) (f : x ⟶ X) => S.arrows f ∨ R.arrows f, downward_closed := ⋯ }

def CategoryTheory.Sieve.inter {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S R : Sieve X) : Sieve X

The intersection of two sieves is a sieve.

Equations

• S.inter R = { arrows := fun (x : C) (f : x ⟶ X) => S.arrows f ∧ R.arrows f, downward_closed := ⋯ }

@[instance_reducible]

instance CategoryTheory.Sieve.instCompleteLattice {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : CompleteLattice (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

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance CategoryTheory.Sieve.sieveInhabited {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : Inhabited (Sieve X)

The maximal sieve always exists.

Equations

• CategoryTheory.Sieve.sieveInhabited = { default := ⊤ }

@[simp]

theorem CategoryTheory.Sieve.sInf_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {Ss : Set (Sieve X)} {Y : C} (f : Y ⟶ X) : (sInf Ss).arrows f ↔ ∀ S ∈ Ss, S.arrows f

@[simp]

theorem CategoryTheory.Sieve.sSup_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {Ss : Set (Sieve X)} {Y : C} (f : Y ⟶ X) : (sSup Ss).arrows f ↔ ∃ (S : Sieve X) (_ : S ∈ Ss), S.arrows f

@[simp]

theorem CategoryTheory.Sieve.inter_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R S : Sieve X} {Y : C} (f : Y ⟶ X) : (R ⊓ S).arrows f ↔ R.arrows f ∧ S.arrows f

@[simp]

theorem CategoryTheory.Sieve.union_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R S : Sieve X} {Y : C} (f : Y ⟶ X) : (R ⊔ S).arrows f ↔ R.arrows f ∨ S.arrows f

theorem CategoryTheory.Sieve.top_apply {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : ⊤.arrows f

@[simp]

theorem CategoryTheory.Sieve.bot_apply {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : ⊥.arrows f ↔ False

@[simp]

theorem CategoryTheory.Sieve.arrows_top {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : ⊤.arrows = ⊤

theorem CategoryTheory.Sieve.arrows_eq_top_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} : S.arrows = ⊤ ↔ S = ⊤

@[simp]

theorem CategoryTheory.Sieve.arrows_bot {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : ⊥.arrows = ⊥

theorem CategoryTheory.Sieve.arrows_eq_bot_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} : S.arrows = ⊥ ↔ S = ⊥

instance CategoryTheory.Sieve.instNontrivial {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : Nontrivial (Sieve X)

def CategoryTheory.Sieve.generate {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) : Sieve X

Generate the smallest sieve containing the given presieve.

Equations

• CategoryTheory.Sieve.generate R = { arrows := fun (Z : C) (f : Z ⟶ X) => ∃ (Y : C) (h : Z ⟶ Y) (g : Y ⟶ X), R g ∧ CategoryTheory.CategoryStruct.comp h g = f, downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.generate_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) (Z : C) (f : Z ⟶ X) : (generate R).arrows f = ∃ (Y : C) (h : Z ⟶ Y) (g : Y ⟶ X), R g ∧ CategoryStruct.comp h g = f

def CategoryTheory.Sieve.bind {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y) : 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

• CategoryTheory.Sieve.bind S R = { arrows := S.bind fun (x : C) (x_1 : x ⟶ X) (h : S x_1) => (R h).arrows, downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.bind_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y) : (bind S R).arrows = S.bind fun (x : C) (x_1 : x ⟶ X) (h : S x_1) => (R h).arrows

@[reducible, inline]

abbrev CategoryTheory.Sieve.BindStruct {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y) {Z : C} (h : Z ⟶ X) : Type (max u₁ v₁)

Structure which contains the data and properties for a morphism h satisfying Sieve.bind S R h.

Equations

• CategoryTheory.Sieve.BindStruct S R h = S.BindStruct (fun (x : C) (x_1 : x ⟶ X) (hf : S x_1) => (R hf).arrows) h

theorem CategoryTheory.Sieve.generate_le_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) (S : Sieve X) : generate R ≤ S ↔ R ≤ S.arrows

def CategoryTheory.Sieve.giGenerate {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : GaloisInsertion generate arrows

Show that there is a Galois insertion (generate, underlying presieve).

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Sieve.le_generate {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) : R ≤ (generate R).arrows

@[simp]

theorem CategoryTheory.Sieve.generate_sieve {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : generate S.arrows = S

theorem CategoryTheory.Sieve.generate_mono {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : Monotone generate

theorem CategoryTheory.Sieve.arrows_mono {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : Monotone arrows

theorem CategoryTheory.Sieve.id_mem_iff_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} : S.arrows (CategoryStruct.id X) ↔ S = ⊤

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

theorem CategoryTheory.Sieve.generate_of_contains_isSplitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {R : Presieve X} (f : Y ⟶ X) [IsSplitEpi f] (hf : R f) : generate R = ⊤

If a presieve contains a split epi, it generates the maximal sieve.

@[simp]

theorem CategoryTheory.Sieve.generate_of_singleton_isSplitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [IsSplitEpi f] : generate (Presieve.singleton f) = ⊤

@[simp]

theorem CategoryTheory.Sieve.generate_top {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : generate ⊤ = ⊤

@[simp]

theorem CategoryTheory.Sieve.generate_bot {C : Type u₁} [Category.{v₁, u₁} C] {X : C} : generate ⊥ = ⊥

@[simp]

theorem CategoryTheory.Sieve.generate_eq_bot_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) : generate R = ⊥ ↔ R = ⊥

@[simp]

theorem CategoryTheory.Sieve.comp_mem_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (i : X ⟶ Y) (f : Y ⟶ Z) [IsIso i] (S : Sieve Z) : S.arrows (CategoryStruct.comp i f) ↔ S.arrows f

@[reducible, inline]

abbrev CategoryTheory.Sieve.ofArrows {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X) : Sieve X

The sieve of X generated by family of morphisms Y i ⟶ X.

Equations

• CategoryTheory.Sieve.ofArrows Y f = CategoryTheory.Sieve.generate (CategoryTheory.Presieve.ofArrows Y f)

theorem CategoryTheory.Sieve.ofArrows_mk {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X) (i : I) : (ofArrows Y f).arrows (f i)

theorem CategoryTheory.Sieve.mem_ofArrows_iff {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X) {W : C} (g : W ⟶ X) : (ofArrows Y f).arrows g ↔ ∃ (i : I) (a : W ⟶ Y i), g = CategoryStruct.comp a (f i)

theorem CategoryTheory.Sieve.ofArrows.exists {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (ofArrows Y f).arrows g) : ∃ (i : I) (h : W ⟶ Y i), g = CategoryStruct.comp h (f i)

noncomputable def CategoryTheory.Sieve.ofArrows.i {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (ofArrows Y f).arrows g) : I

When hg : Sieve.ofArrows Y f g, this is a choice of i such that g factors through f i.

Equations

• CategoryTheory.Sieve.ofArrows.i hg = ⋯.choose

noncomputable def CategoryTheory.Sieve.ofArrows.h {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (ofArrows Y f).arrows g) : W ⟶ Y (i hg)

When hg : Sieve.ofArrows Y f g, this is a morphism h : W ⟶ Y (i hg) such that h ≫ f (i hg) = g.

Equations

• CategoryTheory.Sieve.ofArrows.h hg = ⋯.choose

@[simp]

theorem CategoryTheory.Sieve.ofArrows.fac {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (ofArrows Y f).arrows g) : CategoryStruct.comp (h hg) (f (i hg)) = g

@[simp]

theorem CategoryTheory.Sieve.ofArrows.fac_assoc {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X} {W : C} {g : W ⟶ X} (hg : (ofArrows Y f).arrows g) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (ofArrows.h hg) (CategoryStruct.comp (f (i hg)) h) = CategoryStruct.comp g h

theorem CategoryTheory.Sieve.ofArrows_category' {C : Type u₁} [Category.{v₁, u₁} C] {S : C} (R : Presieve S) : (ofArrows (fun (f : R.category) => f.obj.left) fun (f : R.category) => f.obj.hom) = generate R

The sieve generated by the morphisms in R.category for a presieve R is the sieve generated by R.

theorem CategoryTheory.Sieve.ofArrows_category {C : Type u₁} [Category.{v₁, u₁} C] {S : C} (R : Sieve S) : (ofArrows (fun (f : R.arrows.category) => f.obj.left) fun (f : R.arrows.category) => f.obj.hom) = R

theorem CategoryTheory.Sieve.exists_eq_ofArrows {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Sieve X) : ∃ (I : Type (max u₁ v₁)) (Y : I → C) (f : (i : I) → Y i ⟶ X), R = ofArrows Y f

@[reducible, inline]

abbrev CategoryTheory.Sieve.ofTwoArrows {C : Type u₁} [Category.{v₁, u₁} C] {U V X : C} (i : U ⟶ X) (j : V ⟶ X) : Sieve X

The sieve generated by two morphisms.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Sieve.ofObjects {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) (X : C) : Sieve X

The sieve of X : C that is generated by a family of objects Y : I → C: it consists of morphisms p : Z ⟶ X such that there exists a morphism Z ⟶ Y i for some i (note that this does not depend on p, only on the object Z).

Equations

• CategoryTheory.Sieve.ofObjects Y X = { arrows := fun (Z : C) (x : Z ⟶ X) => ∃ (i : I), Nonempty (Z ⟶ Y i), downward_closed := ⋯ }

theorem CategoryTheory.Sieve.mem_ofObjects_iff {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {Z X : C} (g : Z ⟶ X) : (ofObjects Y X).arrows g ↔ ∃ (i : I), Nonempty (Z ⟶ Y i)

theorem CategoryTheory.Sieve.ofArrows_le_ofObjects {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {X : C} (f : (i : I) → Y i ⟶ X) : ofArrows Y f ≤ ofObjects Y X

theorem CategoryTheory.Sieve.ofArrows_eq_ofObjects {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (hX : Limits.IsTerminal X) {I : Type u_1} (Y : I → C) (f : (i : I) → Y i ⟶ X) : ofArrows Y f = ofObjects Y X

theorem CategoryTheory.Sieve.ofObjects_mono {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : I → C} {I' : Type u_2} {X' : I' → C} {Y : C} (h : Set.range X ⊆ Set.range X') : ofObjects X Y ≤ ofObjects X' Y

def CategoryTheory.Sieve.pullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (h : Y ⟶ X) (S : Sieve X) : 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

• CategoryTheory.Sieve.pullback h S = { arrows := fun (x : C) (sl : x ⟶ Y) => S.arrows (CategoryTheory.CategoryStruct.comp sl h), downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.pullback_apply {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (h : Y ⟶ X) (S : Sieve X) (x✝ : C) (sl : x✝ ⟶ Y) : (pullback h S).arrows sl = S.arrows (CategoryStruct.comp sl h)

@[simp]

theorem CategoryTheory.Sieve.pullback_id {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} : pullback (CategoryStruct.id X) S = S

@[simp]

theorem CategoryTheory.Sieve.pullback_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} : pullback f ⊤ = ⊤

theorem CategoryTheory.Sieve.pullback_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (S : Sieve X) : pullback (CategoryStruct.comp g f) S = pullback g (pullback f S)

@[simp]

theorem CategoryTheory.Sieve.pullback_inter {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (S R : Sieve X) : pullback f (S ⊓ R) = pullback f S ⊓ pullback f R

theorem CategoryTheory.Sieve.pullback_ofArrows_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Z : I → C) (f : (i : I) → Z i ⟶ X) {X' : C} (e : X' ≅ X) : pullback e.hom (ofArrows Z f) = ofArrows Z fun (i : I) => CategoryStruct.comp (f i) e.inv

theorem CategoryTheory.Sieve.mem_iff_pullback_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {S : Sieve X} (f : Y ⟶ X) : S.arrows f ↔ pullback f S = ⊤

theorem CategoryTheory.Sieve.pullback_eq_top_of_mem {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (S : Sieve X) {f : Y ⟶ X} : S.arrows f → pullback f S = ⊤

theorem CategoryTheory.Sieve.pullback_ofObjects_eq_top {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {X : C} {i : I} (g : X ⟶ Y i) : ofObjects Y X = ⊤

@[simp]

theorem CategoryTheory.Sieve.pullback_ofObjects {C : Type u₁} [Category.{v₁, u₁} C] {I : Type u_1} (X : I → C) {Y Z : C} (f : Z ⟶ Y) : pullback f (ofObjects X Y) = ofObjects X Z

@[simp]

theorem CategoryTheory.Sieve.ofObjects_id {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : ofObjects id X = ⊤

def CategoryTheory.Sieve.pushforward {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : Sieve Y) : 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

• CategoryTheory.Sieve.pushforward f R = { arrows := fun (x : C) (gf : x ⟶ X) => ∃ (g : x ⟶ Y), CategoryTheory.CategoryStruct.comp g f = gf ∧ R.arrows g, downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.pushforward_apply {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : Sieve Y) (x✝ : C) (gf : x✝ ⟶ X) : (pushforward f R).arrows gf = ∃ (g : x✝ ⟶ Y), CategoryStruct.comp g f = gf ∧ R.arrows g

theorem CategoryTheory.Sieve.pushforward_apply_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {R : Sieve Y} {Z : C} {g : Z ⟶ Y} (hg : R.arrows g) (f : Y ⟶ X) : (pushforward f R).arrows (CategoryStruct.comp g f)

theorem CategoryTheory.Sieve.pushforward_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y} (R : Sieve Z) : pushforward (CategoryStruct.comp g f) R = pushforward f (pushforward g R)

theorem CategoryTheory.Sieve.galoisConnection {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : GaloisConnection (pushforward f) (pullback f)

theorem CategoryTheory.Sieve.pullback_monotone {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : Monotone (pullback f)

theorem CategoryTheory.Sieve.pushforward_monotone {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : Monotone (pushforward f)

theorem CategoryTheory.Sieve.le_pushforward_pullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : Sieve Y) : R ≤ pullback f (pushforward f R)

theorem CategoryTheory.Sieve.pullback_pushforward_le {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : Sieve X) : pushforward f (pullback f R) ≤ R

theorem CategoryTheory.Sieve.pushforward_union {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (S R : Sieve Y) : pushforward f (S ⊔ R) = pushforward f S ⊔ pushforward f R

@[simp]

theorem CategoryTheory.Sieve.pullback_bot {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : pullback f ⊥ = ⊥

@[simp]

theorem CategoryTheory.Sieve.pushforward_bot {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : pushforward f ⊥ = ⊥

theorem CategoryTheory.Sieve.pushforward_eq_bot_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} {S : Sieve Y} : pushforward f S = ⊥ ↔ S = ⊥

theorem CategoryTheory.Sieve.pushforward_le_bind_of_mem {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (S : Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y) (f : Y ⟶ X) (h : S f) : pushforward f (R h) ≤ bind S R

theorem CategoryTheory.Sieve.le_pullback_bind {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (S : Presieve X) (R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y) (f : Y ⟶ X) (h : S f) : R h ≤ pullback f (bind S R)

def CategoryTheory.Sieve.galoisCoinsertionOfMono {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [Mono f] : GaloisCoinsertion (pushforward f) (pullback f)

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

Equations

• CategoryTheory.Sieve.galoisCoinsertionOfMono f = ⋯.toGaloisCoinsertion ⋯

def CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [IsSplitEpi f] : GaloisInsertion (pushforward f) (pullback f)

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

Equations

• CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi f = ⋯.toGaloisInsertion ⋯

theorem CategoryTheory.Sieve.pullbackArrows_comm {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : Presieve X) [R.HasPullbacks f] : generate (Presieve.pullbackArrows f R) = pullback f (generate R)

theorem CategoryTheory.Sieve.pullback_arrows {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (S : Sieve Y) : (pullback f S).arrows = Presieve.pullback f S.arrows

theorem CategoryTheory.Sieve.pushforward_arrows {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (S : Sieve X) : (pushforward f S).arrows = Presieve.pushforward f S.arrows

theorem CategoryTheory.Sieve.generate_pushforward {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (R : Presieve X) : generate (Presieve.pushforward f R) = pushforward f (generate R)

theorem CategoryTheory.Sieve.ofArrows_eq_pullback_of_isPullback {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {Y : C} {g : Y ⟶ S} {P : ι → C} {p₁ : (i : ι) → P i ⟶ Y} {p₂ : (i : ι) → P i ⟶ X i} (h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)) : ofArrows P p₁ = pullback g (ofArrows X f)

theorem CategoryTheory.Presieve.bind_ofArrows_le_bindOfArrows {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {X : C} (Z : ι → C) (f : (i : ι) → Z i ⟶ X) (R : (i : ι) → Presieve (Z i)) : (Sieve.bind (Sieve.ofArrows Z f).arrows fun (x : C) (x_1 : x ⟶ X) (hg : (Sieve.ofArrows Z f).arrows x_1) => Sieve.pullback (Sieve.ofArrows.h hg) (Sieve.generate (R (Sieve.ofArrows.i hg)))) ≤ Sieve.generate (bindOfArrows Z f R)