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.

Equations

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

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

Equations

• CategoryTheory.instCompleteLatticePresieve = id inferInstance

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

Equations

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

@[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 : CategoryTheory.Over X) => S 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.

Equations

• CategoryTheory.Presieve.diagram S = CategoryTheory.Functor.comp (CategoryTheory.fullSubcategoryInclusion fun (f : CategoryTheory.Over X) => S f.hom) (CategoryTheory.Over.forget X)

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

Equations

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

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

Equations

• CategoryTheory.Presieve.bind S R h = ∃ (Y : C) (g : Z ⟶ Y) (f : Y ⟶ X) (H : S f), R H g ∧ CategoryTheory.CategoryStruct.comp g f = h

@[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 f → CategoryTheory.Presieve Y} {g : Z ⟶ Y} (h₁ : S f) (h₂ : R h₁ 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

The singleton presieve.

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

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.

Equations

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

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

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₁} [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

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

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

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

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 : PUnit.{u_1 + 1} ) => Y) fun (x : PUnit.{u_1 + 1} ) => 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 f H → C) (k : ⦃Y : C⦄ → (f : Y ⟶ X) → (H : CategoryTheory.Presieve.ofArrows Z g f) → (i : j f H) → W f H i ⟶ Y) : (CategoryTheory.Presieve.bind (CategoryTheory.Presieve.ofArrows Z g) fun (Y : C) (f : Y ⟶ X) (H : CategoryTheory.Presieve.ofArrows Z g f) => 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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) {Z : C} (g : Z ⟶ X) (hg : CategoryTheory.Presieve.ofArrows Y f g) : ∃ (i : ι) (h : Y i = Z), g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (f i)

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.

Equations

• CategoryTheory.Presieve.functorPullback F R f = R (F.map 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.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

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 → CategoryTheory.Limits.HasPullback f g

  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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

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₁} [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₂)

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

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.

Equations

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

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

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 : CategoryTheory.Presieve X

  the underlying presieve

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

  stability by precomposition

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• CategoryTheory.Sieve.instCompleteLatticeSieve = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

The maximal sieve always exists.

Equations

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

@[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 ∈ 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 : CategoryTheory.Sieve X) (_ : S ∈ Ss), 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 : C) (h : Z ⟶ Y) (g : Y ⟶ X), R 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.

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

Equations

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

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

Equations

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

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

@[inline, reducible]

abbrev CategoryTheory.Sieve.ofArrows {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} (Y : I → C) (f : (i : I) → Y i ⟶ X) (i : I) : (CategoryTheory.Sieve.ofArrows Y f).arrows (f i)

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

def CategoryTheory.Sieve.ofObjects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) (X : C) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (Y : I → C) {Z : C} {X : C} (g : Z ⟶ X) : (CategoryTheory.Sieve.ofObjects Y X).arrows g ↔ ∃ (i : I), Nonempty (Z ⟶ Y i)

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

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

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

Equations

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

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

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

@[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 : Z ⟶ Y), 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.

Equations

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

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 f → CategoryTheory.Sieve Y) (f : Y ⟶ X) (h : S f) : CategoryTheory.Sieve.pushforward f (R 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 f → CategoryTheory.Sieve Y) (f : Y ⟶ X) (h : S f) : R 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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

@[simp]

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

@[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 : Y.unop ⟶ X // S.arrows 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.

Equations

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

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

Equations

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

@[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) : (CategoryTheory.Sieve.functorInclusion S).app 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.

Equations

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

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.

Equations

• ⋯ = ⋯

@[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 : R.obj (Opposite.op Y)), f.app (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.

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

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

Equations

• ⋯ = ⋯