Presieves

A presieve on an object X of a category C is an arbitrary predicate on morphisms with codomain X. Unlike a sieve, a presieve is not required to be closed under precomposition. Presieves are useful for specifying generating families of arrows before passing to the sieve they generate.

This file develops the basic theory of presieves. It defines singleton presieves and presieves Presieve.ofArrows associated to indexed families of arrows, together with binding and pullback constructions. It also defines pullback and pushforward along a fixed morphism, the associated Galois connection, and the category, diagram, and cocone determined by a presieve. Finally, Presieve.uncurry realizes a presieve as a set in a sigma type.

Functorial operations induced by a functor between categories are developed in Mathlib.CategoryTheory.Sites.Sieves.Functoriality.

Tags

presieve, pullback

@[implicit_reducible]

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

A predicate on arrows with codomain X.

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• CategoryTheory.instInhabitedPresieve X = { default := CategoryTheory.instInhabitedPresieve._aux_1 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.

Equations

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

@[reducible, inline]

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

Construct an object of P.category.

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

• S.cocone = CategoryTheory.Limits.Cocone.whisker (CategoryTheory.ObjectProperty.ι fun (f : CategoryTheory.Over X) => S f.hom) (CategoryTheory.Over.forgetCocone X)

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

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

Equations

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

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

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

• Y : C

  the intermediate object

• g : Z ⟶ self.Y

  a morphism in the family of presieves R

• f : self.Y ⟶ X

  a morphism in the presieve S

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

@[simp]

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

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

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

Equations

• H.bindStruct = ⋯.some

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Presieve.singleton_le_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) {R : Presieve X} : singleton f ≤ R ↔ R 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) => 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).

Equations

• hf.idx = ⋯.choose

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.{w + 1}) => Y) fun (x : PUnit.{w + 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.pushforward {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (R : Presieve X) : Presieve Y

Compose a presieve on the right with a morphism.

Equations

• CategoryTheory.Presieve.pushforward f R fg = ∃ (g : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = fg ∧ R g

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

theorem CategoryTheory.Presieve.pushforward_ofArrows {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_1} {U : ι → C} {X Y : C} (g : (i : ι) → U i ⟶ X) (f : X ⟶ Y) : pushforward f (ofArrows U g) = ofArrows U fun (x : ι) => CategoryStruct.comp (g x) f

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

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

The pullback of a presieve R on Y along a morphism f : X ⟶ Y is the presieve on X given by all morphisms g : Z ⟶ X such that g ≫ f is in R.

Equations

• CategoryTheory.Presieve.pullback f R g = R (CategoryTheory.CategoryStruct.comp g f)

@[simp]

theorem CategoryTheory.Presieve.pullback_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} {R : Presieve X} {Z : C} {g : Z ⟶ Y} : pullback f R g ↔ R (CategoryStruct.comp g f)

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

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

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

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

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

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Presieve.pushforward_id {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (R : Presieve X) : pushforward (CategoryStruct.id X) R = R

theorem CategoryTheory.Presieve.pushforward_comp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : Y ⟶ X) (R : Presieve Y) (g : X ⟶ Z) : pushforward (CategoryStruct.comp f g) R = pushforward g (pushforward f 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.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.

Equations

• s.uncurry = {u : (Y : C) × (Y ⟶ X) | s u.snd}

@[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), (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 ⋯)