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

A set of arrows all with codomain X.

Equations

• CategoryTheory.Presieve X = (⦃Y : C⦄ → Set (Y ⟶ X))

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

Equations

• CategoryTheory.instCompleteLatticePresieve = id inferInstance

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

Equations

• CategoryTheory.Presieve.instInhabited = { default := ⊤ }

@[reducible, inline]

abbrev CategoryTheory.Presieve.category {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (P : Presieve X) : Type (max u₁ v₁)

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

Equations

• P.category = CategoryTheory.ObjectProperty.FullSubcategory fun (f : CategoryTheory.Over X) => P f.hom

@[reducible, inline]

abbrev CategoryTheory.Presieve.categoryMk {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (P : Presieve X) {Y : C} (f : Y ⟶ X) (hf : P f) : P.category

Construct an object of P.category.

Equations

• P.categoryMk f hf = { obj := CategoryTheory.Over.mk f, property := hf }

@[reducible, inline]

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

Equations

• S.diagram = (CategoryTheory.ObjectProperty.ι fun (f : CategoryTheory.Over X) => S f.hom).comp (CategoryTheory.Over.forget X)

@[reducible, inline]

abbrev CategoryTheory.Presieve.cocone {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Presieve X) : Limits.Cocone S.diagram

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 = CategoryTheory.Limits.Cocone.whisker (CategoryTheory.ObjectProperty.ι fun (f : CategoryTheory.Over X) => S f.hom) (CategoryTheory.Over.forgetCocone X)

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

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

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

• Y : C

  the intermediate object

• g : Z ⟶ self.Y

  a morphism in the family of presieves R

• f : self.Y ⟶ X

  a morphism in the presieve S

• hf : S self.f
• hg : R ⋯ self.g
• fac : CategoryStruct.comp self.g self.f = h

@[simp]

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

noncomputable def CategoryTheory.Presieve.bind.bindStruct {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Presieve X} {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Presieve Y} {Z : C} {h : Z ⟶ X} (H : S.bind R h) : S.BindStruct R h

If a morphism h satisfies Presieve.bind S R h, this is a choice of a structure in BindStruct S R h.

Equations

• H.bindStruct = ⋯.some

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

@[simp]

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

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

The singleton presieve.

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

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

The singleton presieve.

Equations

• CategoryTheory.Presieve.singleton f = CategoryTheory.Presieve.singleton' f

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

@[simp]

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

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

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

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.

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

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

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

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

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

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

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

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

theorem CategoryTheory.Presieve.ofArrows_surj {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) {Z : C} (g : Z ⟶ X) (hg : ofArrows Y f g) : ∃ (i : ι) (h : Y i = Z), g = CategoryStruct.comp (eqToHom ⋯) (f i)

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

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

Equations

• CategoryTheory.Presieve.functorPullback F R f = R (F.map f)

@[simp]

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

@[simp]

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

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

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}, R g → Limits.HasPullback f g

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

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

instance CategoryTheory.Presieve.instHasPullbackOfHasPullbacksOfArrows {C : Type u₁} [Category.{v₁, u₁} C] {α : Type v₂} {X : α → C} {B : C} (π : (a : α) → X a ⟶ B) [(ofArrows X π).hasPullbacks] (a b : α) : Limits.HasPullback (π a) (π b)

def CategoryTheory.Presieve.functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S : Presieve X) : 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.

Equations

• CategoryTheory.Presieve.functorPushforward F S f = ∃ (Z : C) (g : Z ⟶ X) (h : Y ⟶ F.obj Z), S g ∧ f = CategoryTheory.CategoryStruct.comp h (F.map g)

structure CategoryTheory.Presieve.FunctorPushforwardStructure {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S : Presieve X) {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 = CategoryStruct.comp self.lift (F.map self.premap)

  the factorisation of the morphism

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

The fixed choice of a preimage.

Equations

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

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

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

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

@[simp]

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

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 set of arrows.

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, set_over).

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.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 an arrow set 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.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 (CategoryTheory.Sieve.ofArrows.h hg) (CategoryStruct.comp (f (i hg)) h) = CategoryStruct.comp g h

@[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 to X which factor through at least one of the Y i.

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

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.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 = ⊤

@[deprecated CategoryTheory.Sieve.mem_iff_pullback_eq_top (since := "2025-02-28")]

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

Alias of CategoryTheory.Sieve.mem_iff_pullback_eq_top.

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

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

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] [Limits.HasPullbacks C] {X Y : C} (f : Y ⟶ X) (R : Presieve X) : generate (Presieve.pullbackArrows f R) = pullback f (generate R)

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

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

Equations

• CategoryTheory.Sieve.functorPullback F R = { arrows := CategoryTheory.Presieve.functorPullback F R.arrows, downward_closed := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

The sieve generated by the image of R under F.

Equations

• CategoryTheory.Sieve.functorPushforward F R = { arrows := CategoryTheory.Presieve.functorPushforward F R.arrows, downward_closed := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion F X = ⋯.toGaloisInsertion ⋯

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

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

Equations

• CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion F X = ⋯.toGaloisCoinsertion ⋯

theorem CategoryTheory.Sieve.functorPushforward_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} (S : Sieve X) (e : C ≌ D) : functorPushforward e.functor S = functorPullback e.inverse (pullback (e.unitInv.app X) S)

@[simp]

theorem CategoryTheory.Sieve.mem_functorPushforward_functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : C} {Y : D} {S : Sieve X} {e : C ≌ D} {f : Y ⟶ e.functor.obj X} : (functorPushforward e.functor S).arrows f ↔ S.arrows (CategoryStruct.comp (e.inverse.map f) (e.unitInv.app X))

theorem CategoryTheory.Sieve.functorPushforward_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X : D} (S : Sieve X) (e : C ≌ D) : functorPushforward e.inverse S = functorPullback e.functor (pullback (e.counit.app X) S)

@[simp]

theorem CategoryTheory.Sieve.mem_functorPushforward_inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {Y : C} {X : D} {S : Sieve X} {e : C ≌ D} {f : Y ⟶ e.inverse.obj X} : (functorPushforward e.inverse S).arrows f ↔ S.arrows (CategoryStruct.comp (e.functor.map f) (e.counit.app X))

theorem CategoryTheory.Sieve.functorPushforward_equivalence_eq_pullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {U : C} (S : Sieve U) : functorPushforward e.inverse (functorPushforward e.functor S) = pullback (e.unitInv.app U) S

theorem CategoryTheory.Sieve.pullback_functorPushforward_equivalence_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (e : C ≌ D) {X : C} (S : Sieve X) : pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S)) = S

theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] {X Y : C} (R : Sieve X) (f : F.obj Y ⟶ F.obj X) : Presieve.functorPushforward F R.arrows f ↔ ∃ (g : Y ⟶ X), F.map g = f ∧ R.arrows g

theorem CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] [F.Faithful] {X Y : C} (R : Sieve X) (f : Y ⟶ X) : Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f

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

A sieve induces a presheaf.

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.Sieve.natTransOfLe {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S T : 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

• CategoryTheory.Sieve.natTransOfLe h = { app := fun (x : Cᵒᵖ) (f : S.functor.obj x) => ⟨↑f, ⋯⟩, naturality := ⋯ }

@[simp]

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

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

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

Equations

• S.functorInclusion = { app := fun (x : Cᵒᵖ) (f : S.functor.obj x) => ↑f, naturality := ⋯ }

@[simp]

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

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

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

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

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

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

Equations

• CategoryTheory.Sieve.sieveOfSubfunctor f = { arrows := fun (Y : C) (g : Y ⟶ X) => ∃ (t : R.obj (Opposite.op Y)), f.app (Opposite.op Y) t = g, downward_closed := ⋯ }

@[simp]

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

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

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