HepLean Documentation

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Multi-(co)equalizers #

A multiequalizer is an equalizer of two morphisms between two products. Since both products and equalizers are limits, such an object is again a limit. This file provides the diagram whose limit is indeed such an object. In fact, it is well-known that any limit can be obtained as a multiequalizer. The dual construction (multicoequalizers) is also provided.

Projects #

Prove that a multiequalizer can be identified with an equalizer between products (and analogously for multicoequalizers).

Prove that the limit of any diagram is a multiequalizer (and similarly for colimits).

inductive CategoryTheory.Limits.WalkingMulticospan {L : Type w} {R : Type w'} (fst : R → L) (snd : R → L) :

Type (max w w')

The type underlying the multiequalizer diagram.

left: {L : Type w} → {R : Type w'} → {fst snd : R → L} → L → CategoryTheory.Limits.WalkingMulticospan fst snd
right: {L : Type w} → {R : Type w'} → {fst snd : R → L} → R → CategoryTheory.Limits.WalkingMulticospan fst snd

Instances For

inductive CategoryTheory.Limits.WalkingMultispan {L : Type w} {R : Type w'} (fst : L → R) (snd : L → R) :

Type (max w w')

The type underlying the multiecoqualizer diagram.

left: {L : Type w} → {R : Type w'} → {fst snd : L → R} → L → CategoryTheory.Limits.WalkingMultispan fst snd
right: {L : Type w} → {R : Type w'} → {fst snd : L → R} → R → CategoryTheory.Limits.WalkingMultispan fst snd

Instances For

instance CategoryTheory.Limits.WalkingMulticospan.instInhabited {L : Type w} {R : Type w'} {fst : R → L} {snd : R → L} [Inhabited L] :

Inhabited (CategoryTheory.Limits.WalkingMulticospan fst snd)

Equations

CategoryTheory.Limits.WalkingMulticospan.instInhabited = { default := CategoryTheory.Limits.WalkingMulticospan.left default }

inductive CategoryTheory.Limits.WalkingMulticospan.Hom {L : Type w} {R : Type w'} {fst : R → L} {snd : R → L} :

CategoryTheory.Limits.WalkingMulticospan fst snd → CategoryTheory.Limits.WalkingMulticospan fst snd → Type (max w w')

Morphisms for WalkingMulticospan.

id: {L : Type w} → {R : Type w'} → {fst snd : R → L} → (A : CategoryTheory.Limits.WalkingMulticospan fst snd) → A.Hom A
fst: {L : Type w} → {R : Type w'} → {fst snd : R → L} → (b : R) → (CategoryTheory.Limits.WalkingMulticospan.left (fst b)).Hom (CategoryTheory.Limits.WalkingMulticospan.right b)
snd: {L : Type w} → {R : Type w'} → {fst snd : R → L} → (b : R) → (CategoryTheory.Limits.WalkingMulticospan.left (snd b)).Hom (CategoryTheory.Limits.WalkingMulticospan.right b)

Instances For

instance CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom {L : Type w} {R : Type w'} {fst : R → L} {snd : R → L} {a : CategoryTheory.Limits.WalkingMulticospan fst snd} :

Inhabited (a.Hom a)

Equations

CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom = { default := CategoryTheory.Limits.WalkingMulticospan.Hom.id a }

def CategoryTheory.Limits.WalkingMulticospan.Hom.comp {L : Type w} {R : Type w'} {fst : R → L} {snd : R → L} {A : CategoryTheory.Limits.WalkingMulticospan fst snd} {B : CategoryTheory.Limits.WalkingMulticospan fst snd} {C : CategoryTheory.Limits.WalkingMulticospan fst snd} :

A.Hom B → B.Hom C → A.Hom C

Composition of morphisms for WalkingMulticospan.

Equations

One or more equations did not get rendered due to their size.
(CategoryTheory.Limits.WalkingMulticospan.Hom.id x✝¹).comp x = x

Instances For

instance CategoryTheory.Limits.WalkingMulticospan.instSmallCategory {L : Type w} {R : Type w'} {fst : R → L} {snd : R → L} :

CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingMulticospan fst snd)

Equations

CategoryTheory.Limits.WalkingMulticospan.instSmallCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.WalkingMulticospan.Hom.id_eq_id {L : Type w} {R : Type w'} {fst : R → L} {snd : R → L} (X : CategoryTheory.Limits.WalkingMulticospan fst snd) :

CategoryTheory.Limits.WalkingMulticospan.Hom.id X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.WalkingMulticospan.Hom.comp_eq_comp {L : Type w} {R : Type w'} {fst : R → L} {snd : R → L} {X : CategoryTheory.Limits.WalkingMulticospan fst snd} {Y : CategoryTheory.Limits.WalkingMulticospan fst snd} {Z : CategoryTheory.Limits.WalkingMulticospan fst snd} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.Limits.WalkingMulticospan.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

instance CategoryTheory.Limits.WalkingMultispan.instInhabited {L : Type w} {R : Type w'} {fst : L → R} {snd : L → R} [Inhabited L] :

Inhabited (CategoryTheory.Limits.WalkingMultispan fst snd)

Equations

CategoryTheory.Limits.WalkingMultispan.instInhabited = { default := CategoryTheory.Limits.WalkingMultispan.left default }

inductive CategoryTheory.Limits.WalkingMultispan.Hom {L : Type w} {R : Type w'} {fst : L → R} {snd : L → R} :

CategoryTheory.Limits.WalkingMultispan fst snd → CategoryTheory.Limits.WalkingMultispan fst snd → Type (max w w')

Morphisms for WalkingMultispan.

id: {L : Type w} → {R : Type w'} → {fst snd : L → R} → (A : CategoryTheory.Limits.WalkingMultispan fst snd) → A.Hom A
fst: {L : Type w} → {R : Type w'} → {fst snd : L → R} → (a : L) → (CategoryTheory.Limits.WalkingMultispan.left a).Hom (CategoryTheory.Limits.WalkingMultispan.right (fst a))
snd: {L : Type w} → {R : Type w'} → {fst snd : L → R} → (a : L) → (CategoryTheory.Limits.WalkingMultispan.left a).Hom (CategoryTheory.Limits.WalkingMultispan.right (snd a))

Instances For

instance CategoryTheory.Limits.WalkingMultispan.instInhabitedHom {L : Type w} {R : Type w'} {fst : L → R} {snd : L → R} {a : CategoryTheory.Limits.WalkingMultispan fst snd} :

Inhabited (a.Hom a)

Equations

CategoryTheory.Limits.WalkingMultispan.instInhabitedHom = { default := CategoryTheory.Limits.WalkingMultispan.Hom.id a }

def CategoryTheory.Limits.WalkingMultispan.Hom.comp {L : Type w} {R : Type w'} {fst : L → R} {snd : L → R} {A : CategoryTheory.Limits.WalkingMultispan fst snd} {B : CategoryTheory.Limits.WalkingMultispan fst snd} {C : CategoryTheory.Limits.WalkingMultispan fst snd} :

A.Hom B → B.Hom C → A.Hom C

Composition of morphisms for WalkingMultispan.

Equations

One or more equations did not get rendered due to their size.
(CategoryTheory.Limits.WalkingMultispan.Hom.id x✝¹).comp x = x

Instances For

instance CategoryTheory.Limits.WalkingMultispan.instSmallCategory {L : Type w} {R : Type w'} {fst : L → R} {snd : L → R} :

CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingMultispan fst snd)

Equations

CategoryTheory.Limits.WalkingMultispan.instSmallCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.Hom.id_eq_id {L : Type w} {R : Type w'} {fst : L → R} {snd : L → R} (X : CategoryTheory.Limits.WalkingMultispan fst snd) :

CategoryTheory.Limits.WalkingMultispan.Hom.id X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.Hom.comp_eq_comp {L : Type w} {R : Type w'} {fst : L → R} {snd : L → R} {X : CategoryTheory.Limits.WalkingMultispan fst snd} {Y : CategoryTheory.Limits.WalkingMultispan fst snd} {Z : CategoryTheory.Limits.WalkingMultispan fst snd} (f : X ⟶ Y) (g : Y ⟶ Z) :

CategoryTheory.Limits.WalkingMultispan.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

structure CategoryTheory.Limits.MulticospanIndex (C : Type u) [CategoryTheory.Category.{v, u} C] :

Type (max (max (max u v) (w + 1)) (w' + 1))

This is a structure encapsulating the data necessary to define a Multicospan.

L : Type w
R : Type w'
fstTo : self.R → self.L
sndTo : self.R → self.L
left : self.L → C
right : self.R → C
fst : (b : self.R) → self.left (self.fstTo b) ⟶ self.right b
snd : (b : self.R) → self.left (self.sndTo b) ⟶ self.right b

Instances For

structure CategoryTheory.Limits.MultispanIndex (C : Type u) [CategoryTheory.Category.{v, u} C] :

Type (max (max (max u v) (w + 1)) (w' + 1))

This is a structure encapsulating the data necessary to define a Multispan.

L : Type w
R : Type w'
fstFrom : self.L → self.R
sndFrom : self.L → self.R
left : self.L → C
right : self.R → C
fst : (a : self.L) → self.left a ⟶ self.right (self.fstFrom a)
snd : (a : self.L) → self.left a ⟶ self.right (self.sndFrom a)

Instances For

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) :

I.multicospan.obj x = match x with | CategoryTheory.Limits.WalkingMulticospan.left a => I.left a | CategoryTheory.Limits.WalkingMulticospan.right b => I.right b

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) {x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo} {y : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo} (f : x ⟶ y) :

I.multicospan.map f = match x, y, f with | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => CategoryTheory.CategoryStruct.id ((fun (x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) => match x with | CategoryTheory.Limits.WalkingMulticospan.left a => I.left a | CategoryTheory.Limits.WalkingMulticospan.right b => I.right b) x) | .(CategoryTheory.Limits.WalkingMulticospan.left (I.fstTo b)), .(CategoryTheory.Limits.WalkingMulticospan.right b), CategoryTheory.Limits.WalkingMulticospan.Hom.fst b => I.fst b | .(CategoryTheory.Limits.WalkingMulticospan.left (I.sndTo b)), .(CategoryTheory.Limits.WalkingMulticospan.right b), CategoryTheory.Limits.WalkingMulticospan.Hom.snd b => I.snd b

def CategoryTheory.Limits.MulticospanIndex.multicospan {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) :

CategoryTheory.Functor (CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) C

The multicospan associated to I : MulticospanIndex.

Equations

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

Instances For

noncomputable def CategoryTheory.Limits.MulticospanIndex.fstPiMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

∏ᶜ I.left ⟶ ∏ᶜ I.right

The induced map ∏ᶜ I.left ⟶ ∏ᶜ I.right via I.fst.

Equations

I.fstPiMap = CategoryTheory.Limits.Pi.lift fun (b : I.R) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.fstTo b)) (I.fst b)

Instances For

noncomputable def CategoryTheory.Limits.MulticospanIndex.sndPiMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

∏ᶜ I.left ⟶ ∏ᶜ I.right

The induced map ∏ᶜ I.left ⟶ ∏ᶜ I.right via I.snd.

Equations

I.sndPiMap = CategoryTheory.Limits.Pi.lift fun (b : I.R) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.sndTo b)) (I.snd b)

Instances For

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.fstPiMap_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : I.R) {Z : C} (h : I.right b ⟶ Z) :

CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.fstTo b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.fstPiMap_π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : I.R) :

CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.fstTo b)) (I.fst b)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sndPiMap_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : I.R) {Z : C} (h : I.right b ⟶ Z) :

CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.sndTo b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sndPiMap_π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (b : I.R) :

CategoryTheory.CategoryStruct.comp I.sndPiMap (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (I.sndTo b)) (I.snd b)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (x : CategoryTheory.Limits.WalkingParallelPair) :

I.parallelPairDiagram.obj x = match x with | CategoryTheory.Limits.WalkingParallelPair.zero => ∏ᶜ I.left | CategoryTheory.Limits.WalkingParallelPair.one => ∏ᶜ I.right

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_map {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y), I.parallelPairDiagram.map h = match X, Y, h with | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => CategoryTheory.CategoryStruct.id (match x with | CategoryTheory.Limits.WalkingParallelPair.zero => ∏ᶜ I.left | CategoryTheory.Limits.WalkingParallelPair.one => ∏ᶜ I.right) | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.left => I.fstPiMap | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.right => I.sndPiMap

noncomputable def CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C

Taking the multiequalizer over the multicospan index is equivalent to taking the equalizer over the two morphisms ∏ᶜ I.left ⇉ ∏ᶜ I.right. This is the diagram of the latter.

Equations

I.parallelPairDiagram = CategoryTheory.Limits.parallelPair I.fstPiMap I.sndPiMap

Instances For

def CategoryTheory.Limits.MultispanIndex.multispan {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) :

CategoryTheory.Functor (CategoryTheory.Limits.WalkingMultispan I.fstFrom I.sndFrom) C

The multispan associated to I : MultispanIndex.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (a : I.L) :

I.multispan.obj (CategoryTheory.Limits.WalkingMultispan.left a) = I.left a

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (b : I.R) :

I.multispan.obj (CategoryTheory.Limits.WalkingMultispan.right b) = I.right b

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_map_fst {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (a : I.L) :

I.multispan.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst a) = I.fst a

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_map_snd {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (a : I.L) :

I.multispan.map (CategoryTheory.Limits.WalkingMultispan.Hom.snd a) = I.snd a

noncomputable def CategoryTheory.Limits.MultispanIndex.fstSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

∐ I.left ⟶ ∐ I.right

The induced map ∐ I.left ⟶ ∐ I.right via I.fst.

Equations

I.fstSigmaMap = CategoryTheory.Limits.Sigma.desc fun (b : I.L) => CategoryTheory.CategoryStruct.comp (I.fst b) (CategoryTheory.Limits.Sigma.ι I.right (I.fstFrom b))

Instances For

noncomputable def CategoryTheory.Limits.MultispanIndex.sndSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

∐ I.left ⟶ ∐ I.right

The induced map ∐ I.left ⟶ ∐ I.right via I.snd.

Equations

I.sndSigmaMap = CategoryTheory.Limits.Sigma.desc fun (b : I.L) => CategoryTheory.CategoryStruct.comp (I.snd b) (CategoryTheory.Limits.Sigma.ι I.right (I.sndFrom b))

Instances For

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.L) {Z : C} (h : ∐ I.right ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) (CategoryTheory.CategoryStruct.comp I.fstSigmaMap h) = CategoryTheory.CategoryStruct.comp (I.fst b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right (I.fstFrom b)) h)

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) I.fstSigmaMap = CategoryTheory.CategoryStruct.comp (I.fst b) (CategoryTheory.Limits.Sigma.ι I.right (I.fstFrom b))

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.L) {Z : C} (h : ∐ I.right ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) (CategoryTheory.CategoryStruct.comp I.sndSigmaMap h) = CategoryTheory.CategoryStruct.comp (I.snd b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right (I.sndFrom b)) h)

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) I.sndSigmaMap = CategoryTheory.CategoryStruct.comp (I.snd b) (CategoryTheory.Limits.Sigma.ι I.right (I.sndFrom b))

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.MultispanIndex.parallelPairDiagram {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C

Taking the multicoequalizer over the multispan index is equivalent to taking the coequalizer over the two morphsims ∐ I.left ⇉ ∐ I.right. This is the diagram of the latter.

Equations

I.parallelPairDiagram = CategoryTheory.Limits.parallelPair I.fstSigmaMap I.sndSigmaMap

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.Multifork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) :

Type (max (max (max w w') u) v)

A multifork is a cone over a multicospan.

Equations

CategoryTheory.Limits.Multifork I = CategoryTheory.Limits.Cone I.multicospan

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.Multicofork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) :

Type (max (max (max w w') u) v)

A multicofork is a cocone over a multispan.

Equations

CategoryTheory.Limits.Multicofork I = CategoryTheory.Limits.Cocone I.multispan

Instances For

def CategoryTheory.Limits.Multifork.ι {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (a : I.L) :

K.pt ⟶ I.left a

The maps from the cone point of a multifork to the objects on the left.

Equations

K.ι a = K.π.app (CategoryTheory.Limits.WalkingMulticospan.left a)

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.app_left_eq_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (a : I.L) :

K.π.app (CategoryTheory.Limits.WalkingMulticospan.left a) = K.ι a

@[simp]

theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) :

K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (K.ι (I.fstTo b)) (I.fst b)

theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) {Z : C} (h : I.multicospan.obj (CategoryTheory.Limits.WalkingMulticospan.right b) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b)) h = CategoryTheory.CategoryStruct.comp (K.ι (I.sndTo b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)

theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) :

K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.CategoryStruct.comp (K.ι (I.sndTo b)) (I.snd b)

@[simp]

theorem CategoryTheory.Limits.Multifork.hom_comp_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K₁ : CategoryTheory.Limits.Multifork I) (K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : I.L) {Z : C} (h : I.left j ⟶ Z) :

CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (K₂.ι j) h) = CategoryTheory.CategoryStruct.comp (K₁.ι j) h

@[simp]

theorem CategoryTheory.Limits.Multifork.hom_comp_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K₁ : CategoryTheory.Limits.Multifork I) (K₂ : CategoryTheory.Limits.Multifork I) (f : K₁ ⟶ K₂) (j : I.L) :

CategoryTheory.CategoryStruct.comp f.hom (K₂.ι j) = K₁.ι j

@[simp]

theorem CategoryTheory.Limits.Multifork.ofι_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (P : C) (ι : (a : I.L) → P ⟶ I.left a) (w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (I.sndTo b)) (I.snd b)) (x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) :

(CategoryTheory.Limits.Multifork.ofι I P ι w).π.app x = match x with | CategoryTheory.Limits.WalkingMulticospan.left a => ι a | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b)

@[simp]

theorem CategoryTheory.Limits.Multifork.ofι_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (P : C) (ι : (a : I.L) → P ⟶ I.left a) (w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (I.sndTo b)) (I.snd b)) :

(CategoryTheory.Limits.Multifork.ofι I P ι w).pt = P

def CategoryTheory.Limits.Multifork.ofι {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (P : C) (ι : (a : I.L) → P ⟶ I.left a) (w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (ι (I.sndTo b)) (I.snd b)) :

CategoryTheory.Limits.Multifork I

Construct a multifork using a collection ι of morphisms.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) {Z : C} (h : I.right b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (K.ι (I.fstTo b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h) = CategoryTheory.CategoryStruct.comp (K.ι (I.sndTo b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)

@[simp]

theorem CategoryTheory.Limits.Multifork.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (b : I.R) :

CategoryTheory.CategoryStruct.comp (K.ι (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (K.ι (I.sndTo b)) (I.snd b)

@[simp]

theorem CategoryTheory.Limits.Multifork.IsLimit.mk_lift {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : I.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E) (E : CategoryTheory.Limits.Multifork I) :

(CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E

def CategoryTheory.Limits.Multifork.IsLimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) (lift : (E : CategoryTheory.Limits.Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : CategoryTheory.Limits.Multifork I) (i : I.L), CategoryTheory.CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), CategoryTheory.CategoryStruct.comp m (K.ι i) = E.ι i) → m = lift E) :

CategoryTheory.Limits.IsLimit K

This definition provides a convenient way to show that a multifork is a limit.

Equations

CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq = { lift := lift, fac := ⋯, uniq := ⋯ }

Instances For

theorem CategoryTheory.Limits.Multifork.IsLimit.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} {f : T ⟶ K.pt} {g : T ⟶ K.pt} (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp f (K.ι a) = CategoryTheory.CategoryStruct.comp g (K.ι a)) :

f = g

def CategoryTheory.Limits.Multifork.IsLimit.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : I.L) → T ⟶ I.left a) (hk : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) :

T ⟶ K.pt

Constructor for morphisms to the point of a limit multifork.

Equations

CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk = hK.lift (CategoryTheory.Limits.Multifork.ofι I T k hk)

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.IsLimit.fac_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : I.L) → T ⟶ I.left a) (hk : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) (a : I.L) {Z : C} (h : I.left a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk) (CategoryTheory.CategoryStruct.comp (K.ι a) h) = CategoryTheory.CategoryStruct.comp (k a) h

@[simp]

theorem CategoryTheory.Limits.Multifork.IsLimit.fac {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} {K : CategoryTheory.Limits.Multifork I} (hK : CategoryTheory.Limits.IsLimit K) {T : C} (k : (a : I.L) → T ⟶ I.left a) (hk : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) (a : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.IsLimit.lift hK k hk) (K.ι a) = k a

@[simp]

theorem CategoryTheory.Limits.Multifork.pi_condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {Z : C} (h : ∏ᶜ I.right ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift K.ι) (CategoryTheory.CategoryStruct.comp I.fstPiMap h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift K.ι) (CategoryTheory.CategoryStruct.comp I.sndPiMap h)

@[simp]

theorem CategoryTheory.Limits.Multifork.pi_condition {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift K.ι) I.fstPiMap = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift K.ι) I.sndPiMap

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) :

K.toPiFork.pt = K.pt

noncomputable def CategoryTheory.Limits.Multifork.toPiFork {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) :

CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap

Given a multifork, we may obtain a fork over ∏ᶜ I.left ⇉ ∏ᶜ I.right.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

K.toPiFork.ι = CategoryTheory.Limits.Pi.lift K.ι

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_one {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} (K : CategoryTheory.Limits.Multifork I) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

K.toPiFork.π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift K.ι) I.fstPiMap

@[simp]

theorem CategoryTheory.Limits.Multifork.ofPiFork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) :

(CategoryTheory.Limits.Multifork.ofPiFork I c).pt = c.pt

noncomputable def CategoryTheory.Limits.Multifork.ofPiFork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) :

CategoryTheory.Limits.Multifork I

Given a fork over ∏ᶜ I.left ⇉ ∏ᶜ I.right, we may obtain a multifork.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) (a : I.L) :

(CategoryTheory.Limits.Multifork.ofPiFork I c).ι a = CategoryTheory.CategoryStruct.comp c.ι (CategoryTheory.Limits.Pi.π I.left a)

@[simp]

theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) (a : I.R) :

(CategoryTheory.Limits.Multifork.ofPiFork I c).π.app (CategoryTheory.Limits.WalkingMulticospan.right a) = CategoryTheory.CategoryStruct.comp c.ι (CategoryTheory.CategoryStruct.comp I.fstPiMap (CategoryTheory.Limits.Pi.π I.right a))

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ : CategoryTheory.Limits.Multifork I} {K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂) :

(I.toPiForkFunctor.map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (K : CategoryTheory.Limits.Multifork I) :

I.toPiForkFunctor.obj K = K.toPiFork

noncomputable def CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Functor (CategoryTheory.Limits.Multifork I) (CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap)

Multifork.toPiFork as a functor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) :

I.ofPiForkFunctor.obj c = CategoryTheory.Limits.Multifork.ofPiFork I c

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] {K₁ : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap} {K₂ : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap} (f : K₁ ⟶ K₂) :

(I.ofPiForkFunctor.map f).hom = f.hom

noncomputable def CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Functor (CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) (CategoryTheory.Limits.Multifork I)

Multifork.ofPiFork as a functor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

I.multiforkEquivPiFork.counitIso = CategoryTheory.NatIso.ofComponents (fun (K : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) => CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl ((I.ofPiForkFunctor.comp I.toPiForkFunctor).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

I.multiforkEquivPiFork.inverse = I.ofPiForkFunctor

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

I.multiforkEquivPiFork.functor = I.toPiForkFunctor

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

I.multiforkEquivPiFork.unitIso = CategoryTheory.NatIso.ofComponents (fun (K : CategoryTheory.Limits.Multifork I) => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt) ⋯) ⋯

noncomputable def CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.Multifork I ≌ CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap

The category of multiforks is equivalent to the category of forks over ∏ᶜ I.left ⇉ ∏ᶜ I.right. It then follows from CategoryTheory.IsLimit.ofPreservesConeTerminal (or reflects) that it preserves and reflects limit cones.

Equations

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

Instances For

def CategoryTheory.Limits.Multicofork.π {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (b : I.R) :

I.right b ⟶ K.pt

The maps to the cocone point of a multicofork from the objects on the right.

Equations

K.π b = K.ι.app (CategoryTheory.Limits.WalkingMultispan.right b)

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.π_eq_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (b : I.R) :

K.ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = K.π b

@[simp]

theorem CategoryTheory.Limits.Multicofork.fst_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) :

K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (I.fst a) (K.π (I.fstFrom a))

theorem CategoryTheory.Limits.Multicofork.snd_app_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) {Z : C} (h : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingMultispan I.fstFrom I.sndFrom)).obj K.pt).obj (CategoryTheory.Limits.WalkingMultispan.left a) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a)) h = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.CategoryStruct.comp (K.π (I.sndFrom a)) h)

theorem CategoryTheory.Limits.Multicofork.snd_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) :

K.ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (I.snd a) (K.π (I.sndFrom a))

@[simp]

theorem CategoryTheory.Limits.Multicofork.π_comp_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K₁ : CategoryTheory.Limits.Multicofork I) (K₂ : CategoryTheory.Limits.Multicofork I) (f : K₁ ⟶ K₂) (b : I.R) {Z : C} (h : K₂.pt ⟶ Z) :

CategoryTheory.CategoryStruct.comp (K₁.π b) (CategoryTheory.CategoryStruct.comp f.hom h) = CategoryTheory.CategoryStruct.comp (K₂.π b) h

@[simp]

theorem CategoryTheory.Limits.Multicofork.π_comp_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K₁ : CategoryTheory.Limits.Multicofork I) (K₂ : CategoryTheory.Limits.Multicofork I) (f : K₁ ⟶ K₂) (b : I.R) :

CategoryTheory.CategoryStruct.comp (K₁.π b) f.hom = K₂.π b

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofπ_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (P : C) (π : (b : I.R) → I.right b ⟶ P) (w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (π (I.sndFrom a))) (x : CategoryTheory.Limits.WalkingMultispan I.fstFrom I.sndFrom) :

(CategoryTheory.Limits.Multicofork.ofπ I P π w).ι.app x = match x with | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) | CategoryTheory.Limits.WalkingMultispan.right a => π a

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofπ_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (P : C) (π : (b : I.R) → I.right b ⟶ P) (w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (π (I.sndFrom a))) :

(CategoryTheory.Limits.Multicofork.ofπ I P π w).pt = P

def CategoryTheory.Limits.Multicofork.ofπ {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (P : C) (π : (b : I.R) → I.right b ⟶ P) (w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (π (I.sndFrom a))) :

CategoryTheory.Limits.Multicofork I

Construct a multicofork using a collection π of morphisms.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) {Z : C} (h : K.pt ⟶ Z) :

CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.CategoryStruct.comp (K.π (I.fstFrom a)) h) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.CategoryStruct.comp (K.π (I.sndFrom a)) h)

@[simp]

theorem CategoryTheory.Limits.Multicofork.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (a : I.L) :

CategoryTheory.CategoryStruct.comp (I.fst a) (K.π (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (K.π (I.sndFrom a))

@[simp]

theorem CategoryTheory.Limits.Multicofork.IsColimit.mk_desc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (desc : (E : CategoryTheory.Limits.Multicofork I) → K.pt ⟶ E.pt) (fac : ∀ (E : CategoryTheory.Limits.Multicofork I) (i : I.R), CategoryTheory.CategoryStruct.comp (K.π i) (desc E) = E.π i) (uniq : ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), CategoryTheory.CategoryStruct.comp (K.π i) m = E.π i) → m = desc E) (E : CategoryTheory.Limits.Multicofork I) :

(CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq).desc E = desc E

def CategoryTheory.Limits.Multicofork.IsColimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) (desc : (E : CategoryTheory.Limits.Multicofork I) → K.pt ⟶ E.pt) (fac : ∀ (E : CategoryTheory.Limits.Multicofork I) (i : I.R), CategoryTheory.CategoryStruct.comp (K.π i) (desc E) = E.π i) (uniq : ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), CategoryTheory.CategoryStruct.comp (K.π i) m = E.π i) → m = desc E) :

CategoryTheory.Limits.IsColimit K

This definition provides a convenient way to show that a multicofork is a colimit.

Equations

CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq = { desc := desc, fac := ⋯, uniq := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.sigma_condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] {Z : C} (h : K.pt ⟶ Z) :

CategoryTheory.CategoryStruct.comp I.fstSigmaMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc K.π) h) = CategoryTheory.CategoryStruct.comp I.sndSigmaMap (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc K.π) h)

@[simp]

theorem CategoryTheory.Limits.Multicofork.sigma_condition {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.CategoryStruct.comp I.fstSigmaMap (CategoryTheory.Limits.Sigma.desc K.π) = CategoryTheory.CategoryStruct.comp I.sndSigmaMap (CategoryTheory.Limits.Sigma.desc K.π)

@[simp]

theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I) :

K.toSigmaCofork.pt = K.pt

noncomputable def CategoryTheory.Limits.Multicofork.toSigmaCofork {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I) :

CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap

Given a multicofork, we may obtain a cofork over ∐ I.left ⇉ ∐ I.right.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_π {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} (K : CategoryTheory.Limits.Multicofork I) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

K.toSigmaCofork.π = CategoryTheory.Limits.Sigma.desc K.π

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) :

(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).pt = c.pt

noncomputable def CategoryTheory.Limits.Multicofork.ofSigmaCofork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) :

CategoryTheory.Limits.Multicofork I

Given a cofork over ∐ I.left ⇉ ∐ I.right, we may obtain a multicofork.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) (a : I.L) :

(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).ι.app (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left a) (CategoryTheory.CategoryStruct.comp I.fstSigmaMap c.π)

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) (b : I.R) :

(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) c.π

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right' {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) (b : I.R) :

(CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).π b = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) c.π

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] {K₁ : CategoryTheory.Limits.Multicofork I} {K₂ : CategoryTheory.Limits.Multicofork I} (f : K₁ ⟶ K₂) :

(I.toSigmaCoforkFunctor.map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (K : CategoryTheory.Limits.Multicofork I) :

I.toSigmaCoforkFunctor.obj K = K.toSigmaCofork

noncomputable def CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Functor (CategoryTheory.Limits.Multicofork I) (CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap)

Multicofork.toSigmaCofork as a functor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) :

I.ofSigmaCoforkFunctor.obj c = CategoryTheory.Limits.Multicofork.ofSigmaCofork I c

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] {K₁ : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap} {K₂ : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap} (f : K₁ ⟶ K₂) :

(I.ofSigmaCoforkFunctor.map f).hom = f.hom

noncomputable def CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Functor (CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) (CategoryTheory.Limits.Multicofork I)

Multicofork.ofSigmaCofork as a functor.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

I.multicoforkEquivSigmaCofork.functor = I.toSigmaCoforkFunctor

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

I.multicoforkEquivSigmaCofork.unitIso = CategoryTheory.NatIso.ofComponents (fun (K : CategoryTheory.Limits.Multicofork I) => CategoryTheory.Limits.Cocones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multicofork I)).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

I.multicoforkEquivSigmaCofork.counitIso = CategoryTheory.NatIso.ofComponents (fun (K : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) => CategoryTheory.Limits.Cofork.ext (CategoryTheory.Iso.refl ((I.ofSigmaCoforkFunctor.comp I.toSigmaCoforkFunctor).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

I.multicoforkEquivSigmaCofork.inverse = I.ofSigmaCoforkFunctor

noncomputable def CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Limits.Multicofork I ≌ CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap

The category of multicoforks is equivalent to the category of coforks over ∐ I.left ⇉ ∐ I.right. It then follows from CategoryTheory.IsColimit.ofPreservesCoconeInitial (or reflects) that it preserves and reflects colimit cocones.

Equations

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

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.HasMultiequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) :

For I : MulticospanIndex C, we say that it has a multiequalizer if the associated multicospan has a limit.

Equations

CategoryTheory.Limits.HasMultiequalizer I = CategoryTheory.Limits.HasLimit I.multicospan

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.multiequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] :

C

The multiequalizer of I : MulticospanIndex C.

Equations

CategoryTheory.Limits.multiequalizer I = CategoryTheory.Limits.limit I.multicospan

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.HasMulticoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) :

For I : MultispanIndex C, we say that it has a multicoequalizer if the associated multicospan has a limit.

Equations

CategoryTheory.Limits.HasMulticoequalizer I = CategoryTheory.Limits.HasColimit I.multispan

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.multicoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] :

C

The multiecoqualizer of I : MultispanIndex C.

Equations

CategoryTheory.Limits.multicoequalizer I = CategoryTheory.Limits.colimit I.multispan

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.Multiequalizer.ι {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (a : I.L) :

CategoryTheory.Limits.multiequalizer I ⟶ I.left a

The canonical map from the multiequalizer to the objects on the left.

Equations

CategoryTheory.Limits.Multiequalizer.ι I a = CategoryTheory.Limits.limit.π I.multicospan (CategoryTheory.Limits.WalkingMulticospan.left a)

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.Multiequalizer.multifork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] :

CategoryTheory.Limits.Multifork I

The multifork associated to the multiequalizer.

Equations

CategoryTheory.Limits.Multiequalizer.multifork I = CategoryTheory.Limits.limit.cone I.multicospan

Instances For

@[simp]

theorem CategoryTheory.Limits.Multiequalizer.multifork_ι {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (a : I.L) :

(CategoryTheory.Limits.Multiequalizer.multifork I).ι a = CategoryTheory.Limits.Multiequalizer.ι I a

@[simp]

theorem CategoryTheory.Limits.Multiequalizer.multifork_π_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (a : I.L) :

(CategoryTheory.Limits.Multiequalizer.multifork I).π.app (CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.Limits.Multiequalizer.ι I a

theorem CategoryTheory.Limits.Multiequalizer.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (b : I.R) {Z : C} (h : I.right b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.fstTo b)) (CategoryTheory.CategoryStruct.comp (I.fst b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.sndTo b)) (CategoryTheory.CategoryStruct.comp (I.snd b) h)

theorem CategoryTheory.Limits.Multiequalizer.condition {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (I.sndTo b)) (I.snd b)

@[reducible, inline]

abbrev CategoryTheory.Limits.Multiequalizer.lift {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : I.L) → W ⟶ I.left a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) :

W ⟶ CategoryTheory.Limits.multiequalizer I

Construct a morphism to the multiequalizer from its universal property.

Equations

CategoryTheory.Limits.Multiequalizer.lift I W k h = CategoryTheory.Limits.limit.lift I.multicospan (CategoryTheory.Limits.Multifork.ofι I W k h)

Instances For

theorem CategoryTheory.Limits.Multiequalizer.lift_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : I.L) → W ⟶ I.left a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) (a : I.L) {Z : C} (h : I.left a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h) = CategoryTheory.CategoryStruct.comp (k a) h

theorem CategoryTheory.Limits.Multiequalizer.lift_ι {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] (W : C) (k : (a : I.L) → W ⟶ I.left a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (I.fstTo b)) (I.fst b) = CategoryTheory.CategoryStruct.comp (k (I.sndTo b)) (I.snd b)) (a : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h) (CategoryTheory.Limits.Multiequalizer.ι I a) = k a

theorem CategoryTheory.Limits.Multiequalizer.hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MulticospanIndex C} [CategoryTheory.Limits.HasMultiequalizer I] {W : C} {i : W ⟶ CategoryTheory.Limits.multiequalizer I} {j : W ⟶ CategoryTheory.Limits.multiequalizer I} :

i = j ↔ ∀ (a : I.L), CategoryTheory.CategoryStruct.comp i (CategoryTheory.Limits.Multiequalizer.ι I a) = CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.Multiequalizer.ι I a)

theorem CategoryTheory.Limits.Multiequalizer.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] {W : C} (i : W ⟶ CategoryTheory.Limits.multiequalizer I) (j : W ⟶ CategoryTheory.Limits.multiequalizer I) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp i (CategoryTheory.Limits.Multiequalizer.ι I a) = CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.Multiequalizer.ι I a)) :

i = j

instance CategoryTheory.Limits.Multiequalizer.instHasEqualizerFstPiMapSndPiMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.HasEqualizer I.fstPiMap I.sndPiMap

Equations

⋯ = ⋯

def CategoryTheory.Limits.Multiequalizer.isoEqualizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.multiequalizer I ≅ CategoryTheory.Limits.equalizer I.fstPiMap I.sndPiMap

The multiequalizer is isomorphic to the equalizer of ∏ᶜ I.left ⇉ ∏ᶜ I.right.

Equations

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

Instances For

def CategoryTheory.Limits.Multiequalizer.ιPi {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Limits.multiequalizer I ⟶ ∏ᶜ I.left

The canonical injection multiequalizer I ⟶ ∏ᶜ I.left.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multiequalizer.ιPi_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : I.L) {Z : C} (h : I.left a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left a) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h

@[simp]

theorem CategoryTheory.Limits.Multiequalizer.ιPi_π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] (a : I.L) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ιPi I) (CategoryTheory.Limits.Pi.π I.left a) = CategoryTheory.Limits.Multiequalizer.ι I a

instance CategoryTheory.Limits.Multiequalizer.instMonoιPi {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) [CategoryTheory.Limits.HasMultiequalizer I] [CategoryTheory.Limits.HasProduct I.left] [CategoryTheory.Limits.HasProduct I.right] :

CategoryTheory.Mono (CategoryTheory.Limits.Multiequalizer.ιPi I)

Equations

⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.Limits.Multicoequalizer.π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : I.R) :

I.right b ⟶ CategoryTheory.Limits.multicoequalizer I

The canonical map from the multiequalizer to the objects on the left.

Equations

CategoryTheory.Limits.Multicoequalizer.π I b = CategoryTheory.Limits.colimit.ι I.multispan (CategoryTheory.Limits.WalkingMultispan.right b)

Instances For

@[reducible, inline]

abbrev CategoryTheory.Limits.Multicoequalizer.multicofork {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] :

CategoryTheory.Limits.Multicofork I

The multicofork associated to the multicoequalizer.

Equations

CategoryTheory.Limits.Multicoequalizer.multicofork I = CategoryTheory.Limits.colimit.cocone I.multispan

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicoequalizer.multicofork_π {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : I.R) :

(CategoryTheory.Limits.Multicoequalizer.multicofork I).π b = CategoryTheory.Limits.Multicoequalizer.π I b

theorem CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : I.R) :

(CategoryTheory.Limits.Multicoequalizer.multicofork I).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicoequalizer.π I b

@[simp]

theorem CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right' {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (b : I.R) :

CategoryTheory.Limits.colimit.ι I.multispan (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.Multicoequalizer.π I b

theorem CategoryTheory.Limits.Multicoequalizer.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (a : I.L) {Z : C} (h : CategoryTheory.Limits.multicoequalizer I ⟶ Z) :

CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (I.fstFrom a)) h) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (I.sndFrom a)) h)

theorem CategoryTheory.Limits.Multicoequalizer.condition {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (a : I.L) :

CategoryTheory.CategoryStruct.comp (I.fst a) (CategoryTheory.Limits.Multicoequalizer.π I (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (CategoryTheory.Limits.Multicoequalizer.π I (I.sndFrom a))

@[reducible, inline]

abbrev CategoryTheory.Limits.Multicoequalizer.desc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : I.R) → I.right b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (I.sndFrom a))) :

CategoryTheory.Limits.multicoequalizer I ⟶ W

Construct a morphism from the multicoequalizer from its universal property.

Equations

CategoryTheory.Limits.Multicoequalizer.desc I W k h = CategoryTheory.Limits.colimit.desc I.multispan (CategoryTheory.Limits.Multicofork.ofπ I W k h)

Instances For

theorem CategoryTheory.Limits.Multicoequalizer.π_desc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : I.R) → I.right b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (I.sndFrom a))) (b : I.R) {Z : C} (h : W ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.desc I W k h✝) h) = CategoryTheory.CategoryStruct.comp (k b) h

theorem CategoryTheory.Limits.Multicoequalizer.π_desc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] (W : C) (k : (b : I.R) → I.right b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (I.fst a) (k (I.fstFrom a)) = CategoryTheory.CategoryStruct.comp (I.snd a) (k (I.sndFrom a))) (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) (CategoryTheory.Limits.Multicoequalizer.desc I W k h) = k b

theorem CategoryTheory.Limits.Multicoequalizer.hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {I : CategoryTheory.Limits.MultispanIndex C} [CategoryTheory.Limits.HasMulticoequalizer I] {W : C} {i : CategoryTheory.Limits.multicoequalizer I ⟶ W} {j : CategoryTheory.Limits.multicoequalizer I ⟶ W} :

i = j ↔ ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) j

theorem CategoryTheory.Limits.Multicoequalizer.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] {W : C} (i : CategoryTheory.Limits.multicoequalizer I ⟶ W) (j : CategoryTheory.Limits.multicoequalizer I ⟶ W) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) j) :

i = j

instance CategoryTheory.Limits.Multicoequalizer.instHasCoequalizerFstSigmaMapSndSigmaMap {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Limits.HasCoequalizer I.fstSigmaMap I.sndSigmaMap

Equations

⋯ = ⋯

def CategoryTheory.Limits.Multicoequalizer.isoCoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Limits.multicoequalizer I ≅ CategoryTheory.Limits.coequalizer I.fstSigmaMap I.sndSigmaMap

The multicoequalizer is isomorphic to the coequalizer of ∐ I.left ⇉ ∐ I.right.

Equations

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

Instances For

def CategoryTheory.Limits.Multicoequalizer.sigmaπ {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

∐ I.right ⟶ CategoryTheory.Limits.multicoequalizer I

The canonical projection ∐ I.right ⟶ multicoequalizer I.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.R) {Z : C} (h : CategoryTheory.Limits.multicoequalizer I ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b) h

@[simp]

theorem CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] (b : I.R) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) = CategoryTheory.Limits.Multicoequalizer.π I b

instance CategoryTheory.Limits.Multicoequalizer.instEpiSigmaπ {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) [CategoryTheory.Limits.HasMulticoequalizer I] [CategoryTheory.Limits.HasCoproduct I.left] [CategoryTheory.Limits.HasCoproduct I.right] :

CategoryTheory.Epi (CategoryTheory.Limits.Multicoequalizer.sigmaπ I)

Equations

⋯ = ⋯