# Theory of sieves #

• For an object X of a category C, a Sieve X is a set of morphisms to X 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 on C together with a monomorphism to the yoneda embedding of X.

## Tags #

sieve, pullback

def CategoryTheory.Presieve {C : Type u₁} [] (X : C) :
Type (max u₁ v₁)

A set of arrows all with codomain X.

Equations
Instances For
instance CategoryTheory.instCompleteLatticePresieve {C : Type u₁} [] {X : C} :
Equations
• CategoryTheory.instCompleteLatticePresieve = id inferInstance
noncomputable instance CategoryTheory.Presieve.instInhabited {C : Type u₁} [] {X : C} :
Equations
• CategoryTheory.Presieve.instInhabited = { default := }
@[reducible, inline]
abbrev CategoryTheory.Presieve.category {C : Type u₁} [] {X : C} (P : ) :
Type (max u₁ v₁)

The full subcategory of the over category C/X consisting of arrows which belong to a presieve on X.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Presieve.categoryMk {C : Type u₁} [] {X : C} (P : ) {Y : C} (f : Y X) (hf : P f) :
P.category

Construct an object of P.category.

Equations
• P.categoryMk f hf = { obj := , property := hf }
Instances For
@[reducible, inline]
abbrev CategoryTheory.Presieve.diagram {C : Type u₁} [] {X : C} (S : ) :

Given a sieve S on X : C, its associated diagram S.diagram is defined to be the natural functor from the full subcategory of the over category C/X consisting of arrows in S to C.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Presieve.cocone {C : Type u₁} [] {X : C} (S : ) :

Given a sieve S on X : C, its associated cocone S.cocone is defined to be the natural cocone over the diagram defined above with cocone point X.

Equations
• S.cocone =
Instances For
def CategoryTheory.Presieve.bind {C : Type u₁} [] {X : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S f) :

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 h = ∃ (Y : C) (g : Z Y) (f : Y X) (H : S f), R H g
Instances For
@[simp]
theorem CategoryTheory.Presieve.bind_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : Y X) {S : } {R : Y : C⦄ → f : Y X⦄ → S f} {g : Z Y} (h₁ : S f) (h₂ : R h₁ g) :
S.bind R
inductive CategoryTheory.Presieve.singleton' {C : Type u₁} [] {X : C} {Y : C} (f : Y✝ X) ⦃Y : C :
(Y X)Prop

The singleton presieve.

• mk: ∀ {C : Type u₁} [inst : ] {X Y : C} {f : Y X},
Instances For
def CategoryTheory.Presieve.singleton {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :

The singleton presieve.

Equations
Instances For
theorem CategoryTheory.Presieve.singleton.mk {C : Type u₁} [] {X : C} {Y : C} {f : Y X} :
@[simp]
theorem CategoryTheory.Presieve.singleton_eq_iff_domain {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (g : Y X) :
theorem CategoryTheory.Presieve.singleton_self {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
inductive CategoryTheory.Presieve.pullbackArrows {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :

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

Instances For
theorem CategoryTheory.Presieve.pullback_singleton {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : Y X) (g : Z X) :
= CategoryTheory.Presieve.singleton CategoryTheory.Limits.pullback.snd
inductive CategoryTheory.Presieve.ofArrows {C : Type u₁} [] {X : C} {ι : Type u_1} (Y : ιC) (f : (i : ι) → Y i X) :

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

• mk: ∀ {C : Type u₁} [inst : ] {X : C} {ι : Type u_1} {Y : ιC} {f : (i : ι) → Y i X} (i : ι),
Instances For
theorem CategoryTheory.Presieve.ofArrows_pUnit {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
theorem CategoryTheory.Presieve.ofArrows_pullback {C : Type u₁} [] {X : C} {Y : C} (f : Y X) {ι : Type u_1} (Z : ιC) (g : (i : ι) → Z i X) :
(CategoryTheory.Presieve.ofArrows (fun (i : ι) => ) fun (i : ι) => CategoryTheory.Limits.pullback.snd) =
theorem CategoryTheory.Presieve.ofArrows_bind {C : Type u₁} [] {X : C} {ι : Type u_1} (Z : ιC) (g : (i : ι) → Z i X) (j : Y : C⦄ → (f : Y X) → Type u_2) (W : Y : C⦄ → (f : Y X) → (H : ) → j f HC) (k : Y : C⦄ → (f : Y X) → (H : ) → (i : j f H) → W f H i Y) :
(.bind fun (Y : C) (f : Y X) (H : ) => CategoryTheory.Presieve.ofArrows (W f H) (k f H)) = CategoryTheory.Presieve.ofArrows (fun (i : (i : ι) × j (g i) ) => W (g i.fst) i.snd) fun (ij : (i : ι) × j (g i) ) => CategoryTheory.CategoryStruct.comp (k (g ij.fst) ij.snd) (g ij.fst)
theorem CategoryTheory.Presieve.ofArrows_surj {C : Type u₁} [] {X : C} {ι : Type u_1} {Y : ιC} (f : (i : ι) → Y i X) {Z : C} (g : Z X) (hg : ) :
∃ (i : ι) (h : Y i = Z),
def CategoryTheory.Presieve.functorPullback {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Presieve (F.obj X)) :

Given a presieve on F(X), we can define a presieve on X by taking the preimage via F.

Equations
• = R (F.map f)
Instances For
@[simp]
theorem CategoryTheory.Presieve.functorPullback_mem {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Presieve (F.obj X)) {Y : C} (f : Y X) :
R (F.map f)
@[simp]
theorem CategoryTheory.Presieve.functorPullback_id {C : Type u₁} [] {X : C} (R : ) :
class CategoryTheory.Presieve.hasPullbacks {C : Type u₁} [] {X : C} (R : ) :

Given a presieve R on X, the predicate R.hasPullbacks means that for all arrows f and g in R, the pullback of f and g exists.

• has_pullbacks : ∀ {Y Z : C} {f : Y X}, R f∀ {g : Z X},

For all arrows f and g in R, the pullback of f and g exists.

Instances
theorem CategoryTheory.Presieve.hasPullbacks.has_pullbacks {C : Type u₁} [] {X : C} {R : } [self : R.hasPullbacks] {Y : C} {Z : C} {f : Y X} :
R f∀ {g : Z X},

For all arrows f and g in R, the pullback of f and g exists.

instance CategoryTheory.Presieve.instHasPullbacksOfHasPullbacks {C : Type u₁} [] {X : C} (R : ) :
R.hasPullbacks
Equations
• =
instance CategoryTheory.Presieve.instHasPullbackOfHasPullbacksOfArrows {C : Type u₁} [] {α : Type v₂} {X : αC} {B : C} (π : (a : α) → X a B) [.hasPullbacks] (a : α) (b : α) :
Equations
• =
def CategoryTheory.Presieve.functorPushforward {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : ) :

Given a presieve on X, we can define a presieve on F(X) (which is actually a sieve) by taking the sieve generated by the image via F.

Equations
Instances For
structure CategoryTheory.Presieve.FunctorPushforwardStructure {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : ) {Y : D} (f : Y F.obj X) :
Type (max (max u₁ v₁) v₂)

An auxiliary definition in order to fix the choice of the preimages between various definitions.

• preobj : C

an object in the source category

• premap : self.preobj X

a map in the source category which has to be in the presieve

• lift : Y F.obj self.preobj

the morphism which appear in the factorisation

• cover : S self.premap

the condition that premap is in the presieve

• fac : f = CategoryTheory.CategoryStruct.comp self.lift (F.map self.premap)

the factorisation of the morphism

Instances For
theorem CategoryTheory.Presieve.FunctorPushforwardStructure.cover {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} {S : } {Y : D} {f : Y F.obj X} (self : ) :
S self.premap

the condition that premap is in the presieve

theorem CategoryTheory.Presieve.FunctorPushforwardStructure.fac {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} {S : } {Y : D} {f : Y F.obj X} (self : ) :
f = CategoryTheory.CategoryStruct.comp self.lift (F.map self.premap)

the factorisation of the morphism

noncomputable def CategoryTheory.Presieve.getFunctorPushforwardStructure {C : Type u₁} [] {D : Type u₂} [] {X : C} {F : } {S : } {Y : D} {f : Y F.obj X} (h : ) :

The fixed choice of a preimage.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Presieve.functorPushforward_comp {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {E : Type u₃} [] (G : ) (R : ) :
theorem CategoryTheory.Presieve.image_mem_functorPushforward {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (R : ) {f : Y X} (h : R f) :
structure CategoryTheory.Sieve {C : Type u₁} [] (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.

• arrows :

the underlying presieve

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

stability by precomposition

Instances For
@[simp]
theorem CategoryTheory.Sieve.downward_closed {C : Type u₁} [] {X : C} (self : ) {Y : C} {Z : C} {f : Y X} :
self.arrows f∀ (g : Z Y), self.arrows

stability by precomposition

instance CategoryTheory.Sieve.instCoeFunPresieve {C : Type u₁} [] {X : C} :
CoeFun fun (x : ) =>
Equations
• CategoryTheory.Sieve.instCoeFunPresieve = { coe := CategoryTheory.Sieve.arrows }
theorem CategoryTheory.Sieve.arrows_ext {C : Type u₁} [] {X : C} {R : } {S : } :
R.arrows = S.arrowsR = S
theorem CategoryTheory.Sieve.ext {C : Type u₁} [] {X : C} {R : } {S : } (h : ∀ ⦃Y : C⦄ (f : Y X), R.arrows f S.arrows f) :
R = S
theorem CategoryTheory.Sieve.ext_iff {C : Type u₁} [] {X : C} {R : } {S : } :
R = S ∀ ⦃Y : C⦄ (f : Y X), R.arrows f S.arrows f
def CategoryTheory.Sieve.sup {C : Type u₁} [] {X : C} (𝒮 : ) :

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

Equations
• = { arrows := fun (Y : C) => {f : Y X | S𝒮, S.arrows f}, downward_closed := }
Instances For
def CategoryTheory.Sieve.inf {C : Type u₁} [] {X : C} (𝒮 : ) :

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

Equations
• = { arrows := fun (x : C) => {f : x X | S𝒮, S.arrows f}, downward_closed := }
Instances For
def CategoryTheory.Sieve.union {C : Type u₁} [] {X : C} (S : ) (R : ) :

The union of two sieves is a sieve.

Equations
• S.union R = { arrows := fun (Y : C) (f : Y X) => S.arrows f R.arrows f, downward_closed := }
Instances For
def CategoryTheory.Sieve.inter {C : Type u₁} [] {X : C} (S : ) (R : ) :

The intersection of two sieves is a sieve.

Equations
• S.inter R = { arrows := fun (Y : C) (f : Y X) => S.arrows f R.arrows f, downward_closed := }
Instances For
instance CategoryTheory.Sieve.instCompleteLattice {C : Type u₁} [] {X : C} :

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

Equations
instance CategoryTheory.Sieve.sieveInhabited {C : Type u₁} [] {X : C} :

The maximal sieve always exists.

Equations
• CategoryTheory.Sieve.sieveInhabited = { default := }
@[simp]
theorem CategoryTheory.Sieve.sInf_apply {C : Type u₁} [] {X : C} {Ss : } {Y : C} (f : Y X) :
(sInf Ss).arrows f SSs, S.arrows f
@[simp]
theorem CategoryTheory.Sieve.sSup_apply {C : Type u₁} [] {X : C} {Ss : } {Y : C} (f : Y X) :
(sSup Ss).arrows f ∃ (S : ) (_ : S Ss), S.arrows f
@[simp]
theorem CategoryTheory.Sieve.inter_apply {C : Type u₁} [] {X : C} {R : } {S : } {Y : C} (f : Y X) :
(R S).arrows f R.arrows f S.arrows f
@[simp]
theorem CategoryTheory.Sieve.union_apply {C : Type u₁} [] {X : C} {R : } {S : } {Y : C} (f : Y X) :
(R S).arrows f R.arrows f S.arrows f
@[simp]
theorem CategoryTheory.Sieve.top_apply {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
.arrows f
@[simp]
theorem CategoryTheory.Sieve.generate_apply {C : Type u₁} [] {X : C} (R : ) (Z : C) (f : Z X) :
.arrows f = ∃ (Y : C) (h : Z Y) (g : Y X), R g
def CategoryTheory.Sieve.generate {C : Type u₁} [] {X : C} (R : ) :

Generate the smallest sieve containing the given set of arrows.

Equations
• = { arrows := fun (Z : C) (f : Z X) => ∃ (Y : C) (h : Z Y) (g : Y X), R g , downward_closed := }
Instances For
@[simp]
theorem CategoryTheory.Sieve.bind_apply {C : Type u₁} [] {X : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S f) :
.arrows = S.bind fun (Y : C) (f : Y X) (h : S f) => (R h).arrows
def CategoryTheory.Sieve.bind {C : Type u₁} [] {X : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S f) :

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
• = { arrows := S.bind fun (Y : C) (f : Y X) (h : S f) => (R h).arrows, downward_closed := }
Instances For
theorem CategoryTheory.Sieve.sets_iff_generate {C : Type u₁} [] {X : C} (R : ) (S : ) :
R S.arrows
def CategoryTheory.Sieve.giGenerate {C : Type u₁} [] {X : C} :
GaloisInsertion CategoryTheory.Sieve.generate CategoryTheory.Sieve.arrows

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Sieve.le_generate {C : Type u₁} [] {X : C} (R : ) :
R .arrows
@[simp]
theorem CategoryTheory.Sieve.generate_sieve {C : Type u₁} [] {X : C} (S : ) :
theorem CategoryTheory.Sieve.id_mem_iff_eq_top {C : Type u₁} [] {X : C} {S : } :
S.arrows S =

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

theorem CategoryTheory.Sieve.generate_of_contains_isSplitEpi {C : Type u₁} [] {X : C} {Y : C} {R : } (f : Y X) (hf : R f) :

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

@[simp]
theorem CategoryTheory.Sieve.generate_of_singleton_isSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
@[simp]
theorem CategoryTheory.Sieve.generate_top {C : Type u₁} [] {X : C} :
@[reducible, inline]
abbrev CategoryTheory.Sieve.ofArrows {C : Type u₁} [] {I : Type u_1} {X : C} (Y : IC) (f : (i : I) → Y i X) :

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

Equations
Instances For
theorem CategoryTheory.Sieve.ofArrows_mk {C : Type u₁} [] {I : Type u_1} {X : C} (Y : IC) (f : (i : I) → Y i X) (i : I) :
.arrows (f i)
theorem CategoryTheory.Sieve.mem_ofArrows_iff {C : Type u₁} [] {I : Type u_1} {X : C} (Y : IC) (f : (i : I) → Y i X) {W : C} (g : W X) :
.arrows g ∃ (i : I) (a : W Y i), g =
def CategoryTheory.Sieve.ofObjects {C : Type u₁} [] {I : Type u_1} (Y : IC) (X : C) :

The sieve of X : C that is generated by a family of objects Y : I → C: it consists of morphisms to X which factor through at least one of the Y i.

Equations
• = { arrows := fun (Z : C) (x : Z X) => ∃ (i : I), Nonempty (Z Y i), downward_closed := }
Instances For
theorem CategoryTheory.Sieve.mem_ofObjects_iff {C : Type u₁} [] {I : Type u_1} (Y : IC) {Z : C} {X : C} (g : Z X) :
.arrows g ∃ (i : I), Nonempty (Z Y i)
theorem CategoryTheory.Sieve.ofArrows_le_ofObjects {C : Type u₁} [] {I : Type u_1} (Y : IC) {X : C} (f : (i : I) → Y i X) :
theorem CategoryTheory.Sieve.ofArrows_eq_ofObjects {C : Type u₁} [] {X : C} (hX : ) {I : Type u_1} (Y : IC) (f : (i : I) → Y i X) :
@[simp]
theorem CategoryTheory.Sieve.pullback_apply {C : Type u₁} [] {X : C} {Y : C} (h : Y✝ X) (S : ) (Y : C) (sl : Y Y✝) :
.arrows sl = S.arrows
def CategoryTheory.Sieve.pullback {C : Type u₁} [] {X : C} {Y : C} (h : Y X) (S : ) :

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
• = { arrows := fun (Y_1 : C) (sl : Y_1 Y) => S.arrows , downward_closed := }
Instances For
@[simp]
theorem CategoryTheory.Sieve.pullback_id {C : Type u₁} [] {X : C} {S : } :
@[simp]
theorem CategoryTheory.Sieve.pullback_top {C : Type u₁} [] {X : C} {Y : C} {f : Y X} :
theorem CategoryTheory.Sieve.pullback_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : Y X} {g : Z Y} (S : ) :
@[simp]
theorem CategoryTheory.Sieve.pullback_inter {C : Type u₁} [] {X : C} {Y : C} {f : Y X} (S : ) (R : ) :
theorem CategoryTheory.Sieve.pullback_eq_top_iff_mem {C : Type u₁} [] {X : C} {Y : C} {S : } (f : Y X) :
S.arrows f
theorem CategoryTheory.Sieve.pullback_eq_top_of_mem {C : Type u₁} [] {X : C} {Y : C} (S : ) {f : Y X} :
S.arrows f
theorem CategoryTheory.Sieve.pullback_ofObjects_eq_top {C : Type u₁} [] {I : Type u_1} (Y : IC) {X : C} {i : I} (g : X Y i) :
@[simp]
theorem CategoryTheory.Sieve.pushforward_apply {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) (Z : C) (gf : Z X) :
.arrows gf = ∃ (g : Z Y), R.arrows g
def CategoryTheory.Sieve.pushforward {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :

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
• = { arrows := fun (Z : C) (gf : Z X) => ∃ (g : Z Y), R.arrows g, downward_closed := }
Instances For
theorem CategoryTheory.Sieve.pushforward_apply_comp {C : Type u₁} [] {X : C} {Y : C} {R : } {Z : C} {g : Z Y} (hg : R.arrows g) (f : Y X) :
.arrows
theorem CategoryTheory.Sieve.pushforward_comp {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : Y X} {g : Z Y} (R : ) :
theorem CategoryTheory.Sieve.galoisConnection {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
theorem CategoryTheory.Sieve.pullback_monotone {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
theorem CategoryTheory.Sieve.pushforward_monotone {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :
theorem CategoryTheory.Sieve.le_pushforward_pullback {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :
theorem CategoryTheory.Sieve.pullback_pushforward_le {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :
theorem CategoryTheory.Sieve.pushforward_union {C : Type u₁} [] {X : C} {Y : C} {f : Y X} (S : ) (R : ) :
theorem CategoryTheory.Sieve.pushforward_le_bind_of_mem {C : Type u₁} [] {X : C} {Y : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S f) (f : Y X) (h : S f) :
theorem CategoryTheory.Sieve.le_pullback_bind {C : Type u₁} [] {X : C} {Y : C} (S : ) (R : Y : C⦄ → f : Y X⦄ → S f) (f : Y X) (h : S f) :
def CategoryTheory.Sieve.galoisCoinsertionOfMono {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :

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

Equations
• = .toGaloisCoinsertion
Instances For
def CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : Y X) :

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

Equations
• = .toGaloisInsertion
Instances For
theorem CategoryTheory.Sieve.pullbackArrows_comm {C : Type u₁} [] {X : C} {Y : C} (f : Y X) (R : ) :
@[simp]
theorem CategoryTheory.Sieve.functorPullback_apply {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Sieve (F.obj X)) :
.arrows =
def CategoryTheory.Sieve.functorPullback {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Sieve (F.obj X)) :

If R is a sieve, then the CategoryTheory.Presieve.functorPullback of R is actually a sieve.

Equations
• = { arrows := , downward_closed := }
Instances For
@[simp]
theorem CategoryTheory.Sieve.functorPullback_arrows {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Sieve (F.obj X)) :
.arrows =
@[simp]
theorem CategoryTheory.Sieve.functorPullback_id {C : Type u₁} [] {X : C} (R : ) :
theorem CategoryTheory.Sieve.functorPullback_comp {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {E : Type u₃} [] (G : ) (R : CategoryTheory.Sieve ((F.comp G).obj X)) :
theorem CategoryTheory.Sieve.functorPushforward_extend_eq {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {R : } :
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_apply {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : ) :
.arrows =
def CategoryTheory.Sieve.functorPushforward {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : ) :

The sieve generated by the image of R under F.

Equations
• = { arrows := , downward_closed := }
Instances For
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_id {C : Type u₁} [] {X : C} (R : ) :
theorem CategoryTheory.Sieve.functorPushforward_comp {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {E : Type u₃} [] (G : ) (R : ) :
theorem CategoryTheory.Sieve.functor_galoisConnection {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
theorem CategoryTheory.Sieve.functorPullback_monotone {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
theorem CategoryTheory.Sieve.functorPushforward_monotone {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
theorem CategoryTheory.Sieve.le_functorPushforward_pullback {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : ) :
theorem CategoryTheory.Sieve.functorPullback_pushforward_le {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : CategoryTheory.Sieve (F.obj X)) :
theorem CategoryTheory.Sieve.functorPushforward_union {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : ) (R : ) :
theorem CategoryTheory.Sieve.functorPullback_union {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : CategoryTheory.Sieve (F.obj X)) (R : CategoryTheory.Sieve (F.obj X)) :
theorem CategoryTheory.Sieve.functorPullback_inter {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (S : CategoryTheory.Sieve (F.obj X)) (R : CategoryTheory.Sieve (F.obj X)) :
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_bot {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_top {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
@[simp]
theorem CategoryTheory.Sieve.functorPullback_bot {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
@[simp]
theorem CategoryTheory.Sieve.functorPullback_top {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
theorem CategoryTheory.Sieve.image_mem_functorPushforward {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} (R : ) {V : C} {f : V X} (h : R.arrows f) :
.arrows (F.map f)
def CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.EssSurj] [F.Full] (X : C) :

When F is essentially surjective and full, the galois connection is a galois insertion.

Equations
• = .toGaloisInsertion
Instances For
def CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.Full] [F.Faithful] (X : C) :

When F is fully faithful, the galois connection is a galois coinsertion.

Equations
• = .toGaloisCoinsertion
Instances For
@[simp]
theorem CategoryTheory.Sieve.functor_obj {C : Type u₁} [] {X : C} (S : ) (Y : Cᵒᵖ) :
S.functor.obj Y = { g : Y.unop X // S.arrows g }
@[simp]
theorem CategoryTheory.Sieve.functor_map_coe {C : Type u₁} [] {X : C} (S : ) :
∀ {X_1 Y : Cᵒᵖ} (f : X_1 Y) (g : { g : X_1.unop X // S.arrows g }), (S.functor.map f g) =
def CategoryTheory.Sieve.functor {C : Type u₁} [] {X : C} (S : ) :

A sieve induces a presheaf.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Sieve.natTransOfLe_app_coe {C : Type u₁} [] {X : C} {S : } {T : } (h : S T) (Y : Cᵒᵖ) (f : S.functor.obj Y) :
( Y f) = f
def CategoryTheory.Sieve.natTransOfLe {C : Type u₁} [] {X : C} {S : } {T : } (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
• = { app := fun (Y : Cᵒᵖ) (f : S.functor.obj Y) => f, , naturality := }
Instances For
@[simp]
theorem CategoryTheory.Sieve.functorInclusion_app {C : Type u₁} [] {X : C} (S : ) (Y : Cᵒᵖ) (f : S.functor.obj Y) :
S.functorInclusion.app Y f = f
def CategoryTheory.Sieve.functorInclusion {C : Type u₁} [] {X : C} (S : ) :
S.functor CategoryTheory.yoneda.obj X

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

Equations
• S.functorInclusion = { app := fun (Y : Cᵒᵖ) (f : S.functor.obj Y) => f, naturality := }
Instances For
theorem CategoryTheory.Sieve.natTransOfLe_comm {C : Type u₁} [] {X : C} {S : } {T : } (h : S T) :
CategoryTheory.CategoryStruct.comp T.functorInclusion = S.functorInclusion
instance CategoryTheory.Sieve.functorInclusion_is_mono {C : Type u₁} [] {X : C} {S : } :
CategoryTheory.Mono S.functorInclusion

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

Equations
• =
@[simp]
theorem CategoryTheory.Sieve.sieveOfSubfunctor_apply {C : Type u₁} [] {X : C} {R : } (f : R CategoryTheory.yoneda.obj X) (Y : C) (g : Y X) :
.arrows g = ∃ (t : R.obj { unop := Y }), f.app { unop := Y } t = g
def CategoryTheory.Sieve.sieveOfSubfunctor {C : Type u₁} [] {X : C} {R : } (f : R CategoryTheory.yoneda.obj X) :

A natural transformation to a representable functor induces a sieve. This is the left inverse of functorInclusion, shown in sieveOfSubfunctor_functorInclusion.

Equations
• = { arrows := fun (Y : C) (g : Y X) => ∃ (t : R.obj { unop := Y }), f.app { unop := Y } t = g, downward_closed := }
Instances For
instance CategoryTheory.Sieve.functorInclusion_top_isIso {C : Type u₁} [] {X : C} :
CategoryTheory.IsIso .functorInclusion
Equations
• =