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

A set of arrows all with codomain X.

instance CategoryTheory.instCompleteLatticePresieve {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CompleteLattice (CategoryTheory.Presieve X)

noncomputable instance CategoryTheory.Presieve.instInhabitedPresieve {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : Inhabited (CategoryTheory.Presieve X)

@[inline, reducible]

abbrev CategoryTheory.Presieve.diagram {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Presieve X) : CategoryTheory.Functor (CategoryTheory.FullSubcategory fun f => S ((CategoryTheory.Functor.id C).obj f.left) f.hom) C

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.

@[inline, reducible]

abbrev CategoryTheory.Presieve.cocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Presieve X) : CategoryTheory.Limits.Cocone (CategoryTheory.Presieve.diagram 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.

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

@[simp]

theorem CategoryTheory.Presieve.bind_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : Y ⟶ X) {S : CategoryTheory.Presieve X} {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S Y f → CategoryTheory.Presieve Y} {g : Z ⟶ Y} (h₁ : S Y f) (h₂ : R Y f h₁ Z g) : CategoryTheory.Presieve.bind S R (CategoryTheory.CategoryStruct.comp g f)

inductive CategoryTheory.Presieve.singleton' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y ⟶ X) ⦃Y : C⦄ : (Y ⟶ X) → Prop

• mk: ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X}, CategoryTheory.Presieve.singleton' f f

The singleton presieve.

def CategoryTheory.Presieve.singleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y ⟶ X) : CategoryTheory.Presieve X

The singleton presieve.

theorem CategoryTheory.Presieve.singleton.mk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {f : Y ⟶ X} : CategoryTheory.Presieve.singleton f f

@[simp]

theorem CategoryTheory.Presieve.singleton_eq_iff_domain {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y ⟶ X) (g : Y ⟶ X) : CategoryTheory.Presieve.singleton f g ↔ f = g

theorem CategoryTheory.Presieve.singleton_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y ⟶ X) : CategoryTheory.Presieve.singleton f f

inductive CategoryTheory.Presieve.pullbackArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y ⟶ X) [CategoryTheory.Limits.HasPullbacks C] (R : CategoryTheory.Presieve X) : CategoryTheory.Presieve Y

• mk: ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} [inst_1 : CategoryTheory.Limits.HasPullbacks C] {R : CategoryTheory.Presieve X} (Z : C) (h : Z ⟶ X), R h → CategoryTheory.Presieve.pullbackArrows f R CategoryTheory.Limits.pullback.snd

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.

theorem CategoryTheory.Presieve.pullback_singleton {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : Y ⟶ X) [CategoryTheory.Limits.HasPullbacks C] (g : Z ⟶ X) : CategoryTheory.Presieve.pullbackArrows f (CategoryTheory.Presieve.singleton g) = CategoryTheory.Presieve.singleton CategoryTheory.Limits.pullback.snd

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

• mk: ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} (i : ι), CategoryTheory.Presieve.ofArrows Y f (f i)

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

theorem CategoryTheory.Presieve.ofArrows_pUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y ⟶ X) : (CategoryTheory.Presieve.ofArrows (fun x => Y) fun x => f) = CategoryTheory.Presieve.singleton f

theorem CategoryTheory.Presieve.ofArrows_pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Y ⟶ X) [CategoryTheory.Limits.HasPullbacks C] {ι : Type u_1} (Z : ι → C) (g : (i : ι) → Z i ⟶ X) : (CategoryTheory.Presieve.ofArrows (fun i => CategoryTheory.Limits.pullback (g i) f) fun i => CategoryTheory.Limits.pullback.snd) = CategoryTheory.Presieve.pullbackArrows f (CategoryTheory.Presieve.ofArrows Z g)

theorem CategoryTheory.Presieve.ofArrows_bind {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} (Z : ι → C) (g : (i : ι) → Z i ⟶ X) (j : ⦃Y : C⦄ → (f : Y ⟶ X) → CategoryTheory.Presieve.ofArrows Z g f → Type u_2) (W : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → j Y f H → C) (k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → (i : j Y f H) → W Y f H i ⟶ Y) : (CategoryTheory.Presieve.bind (CategoryTheory.Presieve.ofArrows Z g) fun Y f H => CategoryTheory.Presieve.ofArrows (W Y f H) (k Y f H)) = CategoryTheory.Presieve.ofArrows (fun i => W (Z i.fst) (g i.fst) (_ : CategoryTheory.Presieve.ofArrows Z g (g i.fst)) i.snd) fun ij => CategoryTheory.CategoryStruct.comp (k (Z ij.fst) (g ij.fst) (_ : CategoryTheory.Presieve.ofArrows Z g (g ij.fst)) ij.snd) (g ij.fst)

def CategoryTheory.Presieve.functorPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Presieve (F.obj X)) : CategoryTheory.Presieve X

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

@[simp]

theorem CategoryTheory.Presieve.functorPullback_mem {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Presieve (F.obj X)) {Y : C} (f : Y ⟶ X) : CategoryTheory.Presieve.functorPullback F R f ↔ R (F.obj Y) (F.map f)

@[simp]

theorem CategoryTheory.Presieve.functorPullback_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) : CategoryTheory.Presieve.functorPullback (CategoryTheory.Functor.id C) R = R

class CategoryTheory.Presieve.hasPullbacks {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) : Prop

• has_pullbacks : ∀ {Y Z : C} {f : Y ⟶ X}, R f → ∀ {g : Z ⟶ X}, R g → CategoryTheory.Limits.HasPullback f g

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

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.

instance CategoryTheory.Presieve.instHasPullbacks {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X) [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Presieve.hasPullbacks R

def CategoryTheory.Presieve.functorPushforward {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Presieve X) : CategoryTheory.Presieve (F.obj X)

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.

structure CategoryTheory.Presieve.FunctorPushforwardStructure {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Presieve X) {Y : D} (f : Y ⟶ F.obj X) : Type (max (max u₁ v₁) v₂)

• preobj : C

  an object in the source category

• premap : s.preobj ⟶ X

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

• lift : Y ⟶ F.obj s.preobj

  the morphism which appear in the factorisation

• cover : S s.premap

  the condition that premap is in the presieve

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

  the factorisation of the morphism

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

noncomputable def CategoryTheory.Presieve.getFunctorPushforwardStructure {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X} (h : CategoryTheory.Presieve.functorPushforward F S f) : CategoryTheory.Presieve.FunctorPushforwardStructure F S f

The fixed choice of a preimage.

theorem CategoryTheory.Presieve.functorPushforward_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) (R : CategoryTheory.Presieve X) : CategoryTheory.Presieve.functorPushforward (CategoryTheory.Functor.comp F G) R = CategoryTheory.Presieve.functorPushforward G (CategoryTheory.Presieve.functorPushforward F R)

theorem CategoryTheory.Presieve.image_mem_functorPushforward {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (R : CategoryTheory.Presieve X) {f : Y ⟶ X} (h : R Y f) : CategoryTheory.Presieve.functorPushforward F R (F.map f)

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

• arrows : CategoryTheory.Presieve X

  the underlying presieve

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

  stability by precomposition

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

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

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

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

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

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

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

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

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

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

The union of two sieves is a sieve.

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

The intersection of two sieves is a sieve.

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

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

The maximal sieve always exists.

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Sieve.inter_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Sieve X} {S : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Sieve X} {S : CategoryTheory.Sieve X} {Y : C} (f : Y ⟶ X) : (R ⊔ S).arrows f ↔ R.arrows f ∨ S.arrows f

@[simp]

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

@[simp]

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

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

Generate the smallest sieve containing the given set of arrows.

@[simp]

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

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

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

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

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

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

@[simp]

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

theorem CategoryTheory.Sieve.id_mem_iff_eq_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : S.arrows (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {R : CategoryTheory.Presieve X} (f : Y ⟶ X) [CategoryTheory.IsSplitEpi f] (hf : R Y f) : CategoryTheory.Sieve.generate R = ⊤

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem CategoryTheory.Sieve.functorPullback_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve (F.obj X)) : (CategoryTheory.Sieve.functorPullback F R).arrows = CategoryTheory.Presieve.functorPullback F R.arrows

def CategoryTheory.Sieve.functorPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Sieve X

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

@[simp]

theorem CategoryTheory.Sieve.functorPullback_arrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve (F.obj X)) : (CategoryTheory.Sieve.functorPullback F R).arrows = CategoryTheory.Presieve.functorPullback F R.arrows

@[simp]

theorem CategoryTheory.Sieve.functorPullback_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPullback (CategoryTheory.Functor.id C) R = R

theorem CategoryTheory.Sieve.functorPullback_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) (R : CategoryTheory.Sieve ((CategoryTheory.Functor.comp F G).obj X)) : CategoryTheory.Sieve.functorPullback (CategoryTheory.Functor.comp F G) R = CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPullback G R)

theorem CategoryTheory.Sieve.functorPushforward_extend_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {R : CategoryTheory.Presieve X} : CategoryTheory.Presieve.functorPushforward F (CategoryTheory.Sieve.generate R).arrows = CategoryTheory.Presieve.functorPushforward F R

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve X) : (CategoryTheory.Sieve.functorPushforward F R).arrows = CategoryTheory.Presieve.functorPushforward F R.arrows

def CategoryTheory.Sieve.functorPushforward {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve (F.obj X)

The sieve generated by the image of R under F.

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPushforward (CategoryTheory.Functor.id C) R = R

theorem CategoryTheory.Sieve.functorPushforward_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor D E) (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPushforward (CategoryTheory.Functor.comp F G) R = CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPushforward F R)

theorem CategoryTheory.Sieve.functor_galoisConnection {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : GaloisConnection (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)

theorem CategoryTheory.Sieve.functorPullback_monotone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : Monotone (CategoryTheory.Sieve.functorPullback F)

theorem CategoryTheory.Sieve.functorPushforward_monotone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : Monotone (CategoryTheory.Sieve.functorPushforward F)

theorem CategoryTheory.Sieve.le_functorPushforward_pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve X) : R ≤ CategoryTheory.Sieve.functorPullback F (CategoryTheory.Sieve.functorPushforward F R)

theorem CategoryTheory.Sieve.functorPullback_pushforward_le {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.functorPullback F R) ≤ R

theorem CategoryTheory.Sieve.functorPushforward_union {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Sieve X) (R : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functorPushforward F (S ⊔ R) = CategoryTheory.Sieve.functorPushforward F S ⊔ CategoryTheory.Sieve.functorPushforward F R

theorem CategoryTheory.Sieve.functorPullback_union {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Sieve (F.obj X)) (R : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Sieve.functorPullback F (S ⊔ R) = CategoryTheory.Sieve.functorPullback F S ⊔ CategoryTheory.Sieve.functorPullback F R

theorem CategoryTheory.Sieve.functorPullback_inter {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Sieve (F.obj X)) (R : CategoryTheory.Sieve (F.obj X)) : CategoryTheory.Sieve.functorPullback F (S ⊓ R) = CategoryTheory.Sieve.functorPullback F S ⊓ CategoryTheory.Sieve.functorPullback F R

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_bot {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Sieve.functorPushforward F ⊥ = ⊥

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Sieve.functorPushforward F ⊤ = ⊤

@[simp]

theorem CategoryTheory.Sieve.functorPullback_bot {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Sieve.functorPullback F ⊥ = ⊥

@[simp]

theorem CategoryTheory.Sieve.functorPullback_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Sieve.functorPullback F ⊤ = ⊤

theorem CategoryTheory.Sieve.image_mem_functorPushforward {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve X) {V : C} {f : V ⟶ X} (h : R.arrows f) : (CategoryTheory.Sieve.functorPushforward F R).arrows (F.map f)

def CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.EssSurj F] [CategoryTheory.Full F] (X : C) : GaloisInsertion (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)

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

def CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] [CategoryTheory.Faithful F] (X : C) : GaloisCoinsertion (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)

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

@[simp]

theorem CategoryTheory.Sieve.functor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (Y : Cᵒᵖ) : (CategoryTheory.Sieve.functor S).obj Y = { g // S.arrows g }

@[simp]

theorem CategoryTheory.Sieve.functor_map_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (g : { g // S.arrows g }), ↑((CategoryTheory.Sieve.functor S).map f g) = CategoryTheory.CategoryStruct.comp f.unop ↑g

def CategoryTheory.Sieve.functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Functor Cᵒᵖ (Type v₁)

A sieve induces a presheaf.

@[simp]

theorem CategoryTheory.Sieve.natTransOfLe_app_coe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {T : CategoryTheory.Sieve X} (h : S ≤ T) (Y : Cᵒᵖ) (f : (CategoryTheory.Sieve.functor S).obj Y) : ↑((CategoryTheory.Sieve.natTransOfLe h).app Y f) = ↑f

def CategoryTheory.Sieve.natTransOfLe {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {T : CategoryTheory.Sieve X} (h : S ≤ T) : CategoryTheory.Sieve.functor S ⟶ CategoryTheory.Sieve.functor T

If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced presheaves.

@[simp]

theorem CategoryTheory.Sieve.functorInclusion_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (Y : Cᵒᵖ) (f : (CategoryTheory.Sieve.functor S).obj Y) : Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types (CategoryTheory.Sieve.functor S) (CategoryTheory.yoneda.obj X) (CategoryTheory.Sieve.functorInclusion S) Y f = ↑f

def CategoryTheory.Sieve.functorInclusion {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve.functor S ⟶ CategoryTheory.yoneda.obj X

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

theorem CategoryTheory.Sieve.natTransOfLe_comm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} {T : CategoryTheory.Sieve X} (h : S ≤ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.natTransOfLe h) (CategoryTheory.Sieve.functorInclusion T) = CategoryTheory.Sieve.functorInclusion S

instance CategoryTheory.Sieve.functorInclusion_is_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : CategoryTheory.Mono (CategoryTheory.Sieve.functorInclusion S)

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

@[simp]

theorem CategoryTheory.Sieve.sieveOfSubfunctor_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : R ⟶ CategoryTheory.yoneda.obj X) (Y : C) (g : Y ⟶ X) : (CategoryTheory.Sieve.sieveOfSubfunctor f).arrows g = ∃ t, Cᵒᵖ.app CategoryTheory.Category.opposite (Type v₁) CategoryTheory.types R (CategoryTheory.yoneda.obj X) f (Opposite.op Y) t = g

def CategoryTheory.Sieve.sieveOfSubfunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : R ⟶ CategoryTheory.yoneda.obj X) : CategoryTheory.Sieve X

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

theorem CategoryTheory.Sieve.sieveOfSubfunctor_functorInclusion {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X} : CategoryTheory.Sieve.sieveOfSubfunctor (CategoryTheory.Sieve.functorInclusion S) = S

instance CategoryTheory.Sieve.functorInclusion_top_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} : CategoryTheory.IsIso (CategoryTheory.Sieve.functorInclusion ⊤)