Theory of sieves

• For an object X of a category C, a Sieve X is a predicate on 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 predicate on arrows with codomain X.

@[implicit_reducible]

instance CategoryTheory.instCompleteLatticePresieve {C : Type u_1} [Category.{u_2, u_1} C] (X : C) : CompleteLattice (Presieve X)

@[implicit_reducible]

instance CategoryTheory.instInhabitedPresieve {C : Type u_1} [Category.{u_2, u_1} C] (X : C) : Inhabited (Presieve X)

@[simp]

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

@[simp]

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

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

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

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

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

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 presieve S on X, and presieve R on Y for each f : Y ⟶ X in S, produce a presieve on X: { g ≫ f | (f : Y ⟶ X) ∈ S, (g : Z ⟶ Y) ∈ R f }.

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.

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) : Presieve X

The singleton presieve.

• 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

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

A presieve R has pullbacks along f if for every h in R, the pullback with f exists.

• hasPullback {Z : C} {h : Z ⟶ X} : R h → Limits.HasPullback h f

theorem CategoryTheory.Presieve.hasPullback {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {X : C} {R : Presieve X} {Y : C} (f : Y ⟶ X) [self : R.HasPullbacks f] {Z : C} {h : Z ⟶ X} : R h → Limits.HasPullback h f

Alias of CategoryTheory.Presieve.HasPullbacks.hasPullback.

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

instance CategoryTheory.Presieve.instHasPullbacksSingletonOfHasPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) (g : Z ⟶ X) [Limits.HasPullback g f] : (singleton g).HasPullbacks f

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

Pullback a presieve along a fixed map, by taking the pullback in the category. This is not the same as the underlying presieve 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} {R : Presieve X} [R.HasPullbacks f] (Z : C) (h : Z ⟶ X) (hRh : 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) (g : Z ⟶ X) [Limits.HasPullback g f] : 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.mk' {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {Z : C} {g : Z ⟶ X} (i : ι) (h : Z = Y i) (hg : g = CategoryStruct.comp (eqToHom h) (f i)) : ofArrows Y f g

instance CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) {ι : Type u_1} (Z : ι → C) (g : (i : ι) → Z i ⟶ X) [∀ (i : ι), Limits.HasPullback (g i) f] : (ofArrows Z g).HasPullbacks f

theorem CategoryTheory.Presieve.ofArrows_pullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) {ι : Type u_1} (Z : ι → C) (g : (i : ι) → Z i ⟶ X) [∀ (i : ι), Limits.HasPullback (g i) f] : (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)

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

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

noncomputable def CategoryTheory.Presieve.ofArrows.idx {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {Y : C} {g : Y ⟶ S} (hf : ofArrows X f g) : ι

If g : Y ⟶ S is in the presieve given by the indexed family fᵢ, this is a choice of index such that g = fᵢ modulo eqToHom. Note: This should generally not be used! If possible, use the induction principle for the type Presieve.ofArrows instead (using e.g., rintro / obtain).

theorem CategoryTheory.Presieve.ofArrows.obj_idx {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {Y : C} {g : Y ⟶ S} (hf : ofArrows X f g) : X hf.idx = Y

theorem CategoryTheory.Presieve.ofArrows.eq_eqToHom_comp_hom_idx {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {Y : C} {g : Y ⟶ S} (hf : ofArrows X f g) : g = CategoryStruct.comp (eqToHom ⋯) (f hf.idx)

theorem CategoryTheory.Presieve.ofArrows.hom_idx {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {Y : C} {g : Y ⟶ S} (hf : ofArrows X f g) : f hf.idx = CategoryStruct.comp (eqToHom ⋯) g

theorem CategoryTheory.Presieve.ofArrows_comp_le {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {σ : Type u_2} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) (a : σ → ι) : (ofArrows (Y ∘ a) fun (i : σ) => f (a i)) ≤ ofArrows Y f

theorem CategoryTheory.Presieve.ofArrows_comp_eq_of_surjective {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {σ : Type u_2} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) {a : σ → ι} (ha : Function.Surjective a) : (ofArrows (Y ∘ a) fun (i : σ) => f (a i)) = ofArrows Y f

theorem CategoryTheory.Presieve.ofArrows_le_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {R : Presieve X} : ofArrows Y f ≤ R ↔ ∀ (i : ι), R (f i)

theorem CategoryTheory.Presieve.ofArrows_of_unique {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {ι : Type u_1} [Unique ι] {Y : ι → C} (f : (i : ι) → Y i ⟶ X) : ofArrows Y f = singleton (f default)

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_of_isEmpty {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {ι : Type u_1} [IsEmpty ι] {Y : ι → C} (f : (i : ι) → Y i ⟶ X) : ofArrows Y f = ⊥

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

A convenient constructor for a refinement of a presieve of the form Presieve.ofArrows. This contains a sieve obtained by Sieve.bind and Sieve.ofArrows, see Presieve.bind_ofArrows_le_bindOfArrows, but has better definitional properties.

• mk {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X} {R : (i : ι) → Presieve (Y i)} (i : ι) {Z : C} (g : Z ⟶ Y i) (hg : R i g) : bindOfArrows Y f R (CategoryStruct.comp g (f i))

theorem CategoryTheory.Presieve.bindOfArrows_ofArrows {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {σ : ι → Type u_2} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i) : (bindOfArrows X f fun (i : ι) => ofArrows (Y i) (g i)) = ofArrows (fun (p : (i : ι) × σ i) => Y p.fst p.snd) fun (p : (i : ι) × σ i) => CategoryStruct.comp (g p.fst p.snd) (f p.fst)

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.

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

Given a presieve R on X, the predicate R.HasPairwisePullbacks 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.instHasPairwisePullbacksOfHasPullbacks {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) [Limits.HasPullbacks C] : R.HasPairwisePullbacks

instance CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows {C : Type u₁} [Category.{v₁, u₁} C] {α : Type v₂} {X : α → C} {B : C} (π : (a : α) → X a ⟶ B) [(ofArrows X π).HasPairwisePullbacks] (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.

theorem CategoryTheory.Presieve.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)

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.

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)

inductive CategoryTheory.Presieve.map {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)

This presieve generates functorPushforward. See arrows_generate_map_eq_functorPushforward.

• of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} {s : Presieve X} {Y : C} {u : Y ⟶ X} (h : s u) : map F s (F.map u)

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

theorem CategoryTheory.Presieve.map_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} {R : Presieve X} {Y : D} {f : Y ⟶ F.obj X} : map F R f ↔ ∃ (Z : C) (h : F.obj Z = Y) (g : Z ⟶ X), R g ∧ F.map g = CategoryStruct.comp (eqToHom h) f

@[simp]

theorem CategoryTheory.Presieve.map_ofArrows {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X) : map F (ofArrows Y f) = ofArrows (fun (i : ι) => F.obj (Y i)) fun (i : ι) => F.map (f i)

@[simp]

theorem CategoryTheory.Presieve.map_singleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X Y : C} (f : X ⟶ Y) : map F (singleton f) = singleton (F.map f)

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

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

theorem CategoryTheory.Presieve.map_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)) : map F (functorPullback F R) ≤ R

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

@[simp]

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

@[simp]

theorem CategoryTheory.Presieve.functorPullback_map_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)) : functorPullback F (map F (functorPullback F R)) = functorPullback F R

@[simp]

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

theorem CategoryTheory.Presieve.map_monotone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} : Monotone (map F)

theorem CategoryTheory.Presieve.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)

def CategoryTheory.Presieve.uncurry {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (s : Presieve X) : Set ((Y : C) × (Y ⟶ X))

Uncurry a presieve to one set over the sigma type.

@[simp]

theorem CategoryTheory.Presieve.uncurry_singleton {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (u : Y ⟶ X) : (singleton u).uncurry = {⟨Y, u⟩}

@[simp]

theorem CategoryTheory.Presieve.uncurry_pullbackArrows {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (s : Presieve X) [Limits.HasPullbacks C] {B : C} (b : B ⟶ X) : (pullbackArrows b s).uncurry = (fun (f : (Y : C) × (Y ⟶ X)) => ⟨Limits.pullback f.snd b, Limits.pullback.snd f.snd b⟩) '' s.uncurry

@[simp]

theorem CategoryTheory.Presieve.uncurry_bind {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (s : Presieve X) (t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y) : (s.bind t).uncurry = ⋃ (i : (Y : C) × (Y ⟶ X)), ⋃ (h : i ∈ s.uncurry), (_root_.Sigma.map id fun (Z : C) (g : Z ⟶ i.fst) => CategoryStruct.comp g i.snd) '' (t i.snd h).uncurry

@[simp]

theorem CategoryTheory.Presieve.uncurry_ofArrows {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {ι : Type u_1} (Y : ι → C) (f : (i : ι) → Y i ⟶ X) : (ofArrows Y f).uncurry = Set.range fun (i : ι) => ⟨Y i, f i⟩

theorem CategoryTheory.Presieve.ofArrows_eq_ofArrows_uncurry {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) : ofArrows X f = ofArrows (fun (i : ↑(ofArrows X f).uncurry) => X (ofArrows.idx ⋯)) fun (i : ↑(ofArrows X f).uncurry) => f (ofArrows.idx ⋯)

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

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

• arrows : Presieve X

  the underlying presieve

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

  stability by precomposition

@[implicit_reducible]

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

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.

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.

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.

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.

@[implicit_reducible]

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

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

@[implicit_reducible]

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

The maximal sieve always exists.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

Generate the smallest sieve containing the given presieve.

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

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

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.

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

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

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

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

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

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

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.

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.

@[simp]

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

@[simp]

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

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

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

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

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

@[reducible, inline]

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

The sieve generated by two morphisms.

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.

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

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

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

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

def CategoryTheory.Sieve.pullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (h : Y ⟶ X) (S : Sieve X) : Sieve Y

Given a morphism h : Y ⟶ X, send a sieve S on X to a sieve on Y as the inverse image of S with _ ≫ h. That is, Sieve.pullback S h := (≫ h) '⁻¹ S.

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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.

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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.

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

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.

@[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.generate_functorPullback_le {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)) : generate (Presieve.functorPullback F R) ≤ functorPullback F (generate R)

theorem CategoryTheory.Sieve.functorPullback_pullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) (S : Sieve (F.obj Y)) : functorPullback F (pullback (F.map f) S) = pullback f (functorPullback F S)

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.

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

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

@[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.functorPushforward_le_iff_le_functorPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} (S : Sieve X) (R : Sieve (F.obj X)) : functorPushforward F S ≤ R ↔ S ≤ functorPullback F R

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)

theorem CategoryTheory.Sieve.functorPushforward_pullback_le {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : Y ⟶ X) (S : Sieve X) : functorPushforward F (pullback f S) ≤ pullback (F.map f) (functorPushforward F S)

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.

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.

theorem CategoryTheory.Sieve.functorPullback_functorPushforward_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X : C} {S : Sieve X} [F.Full] [F.Faithful] : functorPullback F (functorPushforward F S) = S

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

theorem CategoryTheory.Sieve.functorPushforward_ofObjects_le {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {I : Type u_1} (X : I → C) (Y : C) : functorPushforward F (ofObjects X Y) ≤ ofObjects (F.obj ∘ X) (F.obj Y)

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.

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

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

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

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

Any component f : Y ⟶ X of the sieve S induces a natural transformation from yoneda.obj Y to the presheaf induced by S.

@[simp]

theorem CategoryTheory.Sieve.toFunctor_app_coe {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) (Z : Cᵒᵖ) (g : (yoneda.obj Y).obj Z) : ↑((S.toFunctor f hf).app Z g) = CategoryStruct.comp g 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.

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

@[reducible, inline]

abbrev CategoryTheory.Sieve.uliftFunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : Functor Cᵒᵖ (Type (max w v₁))

A variant of Sieve.functor with universe lifting.

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

A variant of Sieve.natTransOfLe with universe lifting.

@[simp]

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

def CategoryTheory.Sieve.uliftFunctorInclusion {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : S.uliftFunctor ⟶ uliftYoneda.{w, v₁, u₁}.obj X

A variant of Sieve.functorInclusion with universe lifting.

@[simp]

theorem CategoryTheory.Sieve.uliftFunctorInclusion_app {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) (X✝ : Cᵒᵖ) (a✝ : CategoryTheory.uliftFunctor.{w, v₁}.obj (S.functor.obj X✝)) : S.uliftFunctorInclusion.app X✝ a✝ = { down := ↑a✝.down }

def CategoryTheory.Sieve.toUliftFunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : uliftYoneda.{w, v₁, u₁}.obj Y ⟶ S.uliftFunctor

A variant of Sieve.toFunctor with universe lifting.

@[simp]

theorem CategoryTheory.Sieve.toUliftFunctor_app_down_coe {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) (Z : Cᵒᵖ) (g : (uliftYoneda.{w, v₁, u₁}.obj Y).obj Z) : ↑((S.toUliftFunctor f hf).app Z g).down = CategoryStruct.comp g.down f

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

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

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

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

A variant of Sieve.sieveOfSubfunctor with universe lifting.

@[simp]

theorem CategoryTheory.Sieve.sieveOfUliftSubfunctor_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {R : Functor Cᵒᵖ (Type (max w v₁))} (f : R ⟶ uliftYoneda.{w, v₁, u₁}.obj X) (Y : C) (g : Y ⟶ X) : (sieveOfUliftSubfunctor f).arrows g = ∃ (t : R.obj (Opposite.op Y)), f.app (Opposite.op Y) t = { down := g }

theorem CategoryTheory.Sieve.sieveOfUliftSubfunctor_uliftFunctorInclusion {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} : sieveOfUliftSubfunctor S.uliftFunctorInclusion = S

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

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

def CategoryTheory.Sieve.shrinkFunctor {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] {X : C} (S : Sieve X) : Subfunctor (shrinkYoneda.{w, v₁, u₁}.obj X)

If C is w-locally small, any sieve induces a subfunctor of shrinkYoneda.{w}.obj X.

@[simp]

theorem CategoryTheory.Sieve.shrinkFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] {X : C} (S : Sieve X) (Y : Cᵒᵖ) : (shrinkFunctor.{w, v₁, u₁} S).obj Y = {f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y | S.arrows (shrinkYonedaObjObjEquiv f)}

noncomputable def CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{max w' w, v₁, u₁} C] : (shrinkFunctor.{w, v₁, u₁} S).toFunctor.comp CategoryTheory.uliftFunctor.{w', w} ≅ (shrinkFunctor.{max w' w, v₁, u₁} S).toFunctor

Sieve.shrinkFunctor is compatible with universe lifting.

theorem CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{max w' w, v₁, u₁} C] : CategoryStruct.comp S.shrinkFunctorUliftFunctorIso.inv (Functor.whiskerRight (shrinkFunctor.{w, v₁, u₁} S).ι CategoryTheory.uliftFunctor.{w', w}) = CategoryStruct.comp (shrinkFunctor.{max w' w, v₁, u₁} S).ι (shrinkYonedaUliftFunctorIso.inv.app X)

theorem CategoryTheory.Sieve.shrinkFunctorUliftFunctorIso_inv_ι_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {S : Sieve X} [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{max w' w, v₁, u₁} C] {Z : Functor Cᵒᵖ (Type (max w w'))} (h : (shrinkYoneda.{w, v₁, u₁}.obj X).comp CategoryTheory.uliftFunctor.{w', w} ⟶ Z) : CategoryStruct.comp S.shrinkFunctorUliftFunctorIso.inv (CategoryStruct.comp (Functor.whiskerRight (shrinkFunctor.{w, v₁, u₁} S).ι CategoryTheory.uliftFunctor.{w', w}) h) = CategoryStruct.comp (CategoryStruct.comp (shrinkFunctor.{max w' w, v₁, u₁} S).ι (shrinkYonedaUliftFunctorIso.inv.app X)) h

noncomputable def CategoryTheory.Sieve.shrinkFunctorIsoFunctor {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ≅ S.functor

Shrinking does nothing for the same universe level.

@[simp]

theorem CategoryTheory.Sieve.shrinkFunctorIsoFunctor_hom_app_coe {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) (X✝ : Cᵒᵖ) (a✝ : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj X✝) : ↑(S.shrinkFunctorIsoFunctor.hom.app X✝ a✝) = shrinkYonedaObjObjEquiv ↑a✝

@[simp]

theorem CategoryTheory.Sieve.shrinkFunctorIsoFunctor_inv_app_coe {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (S : Sieve X) (X✝ : Cᵒᵖ) (a✝ : S.functor.obj X✝) : ↑(S.shrinkFunctorIsoFunctor.inv.app X✝ a✝) = shrinkYonedaObjObjEquiv.symm ↑a✝

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

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

theorem CategoryTheory.Presieve.functorPushforward_overForget {C : Type u₁} [Category.{v₁, u₁} C] {S : C} {X : Over S} (R : Presieve X) : functorPushforward (Over.forget S) R = (Sieve.generate (map (Over.forget S) R)).arrows