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 w

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

The type underlying the multiequalizer diagram.

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

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

The type underlying the multiecoqualizer diagram.

instance CategoryTheory.Limits.WalkingMulticospan.instInhabitedWalkingMulticospan {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} [Inhabited L] : Inhabited (CategoryTheory.Limits.WalkingMulticospan fst snd)

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 w

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

Morphisms for WalkingMulticospan.

instance CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} {a : CategoryTheory.Limits.WalkingMulticospan fst snd} : Inhabited (CategoryTheory.Limits.WalkingMulticospan.Hom a 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} : CategoryTheory.Limits.WalkingMulticospan.Hom A B → CategoryTheory.Limits.WalkingMulticospan.Hom B C → CategoryTheory.Limits.WalkingMulticospan.Hom A C

Composition of morphisms for WalkingMulticospan.

instance CategoryTheory.Limits.WalkingMulticospan.instSmallCategoryWalkingMulticospan {L : Type w} {R : Type w} {fst : R → L} {snd : R → L} : CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingMulticospan fst snd)

@[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.instInhabitedWalkingMultispan {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} [Inhabited L] : Inhabited (CategoryTheory.Limits.WalkingMultispan fst snd)

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

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

Morphisms for WalkingMultispan.

instance CategoryTheory.Limits.WalkingMultispan.instInhabitedHom {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} {a : CategoryTheory.Limits.WalkingMultispan fst snd} : Inhabited (CategoryTheory.Limits.WalkingMultispan.Hom a a)

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

Composition of morphisms for WalkingMultispan.

instance CategoryTheory.Limits.WalkingMultispan.instSmallCategoryWalkingMultispan {L : Type v} {R : Type v} {fst : L → R} {snd : L → R} : CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingMultispan fst snd)

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.Hom.id_eq_id {L : Type v} {R : Type v} {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 v} {R : Type v} {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 u v) (w + 1))

• L : Type w
• R : Type w
• fstTo : s.R → s.L
• sndTo : s.R → s.L
• left : s.L → C
• right : s.R → C
• fst : (b : s.R) → CategoryTheory.Limits.MulticospanIndex.left s (CategoryTheory.Limits.MulticospanIndex.fstTo s b) ⟶ CategoryTheory.Limits.MulticospanIndex.right s b
• snd : (b : s.R) → CategoryTheory.Limits.MulticospanIndex.left s (CategoryTheory.Limits.MulticospanIndex.sndTo s b) ⟶ CategoryTheory.Limits.MulticospanIndex.right s b

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

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

• L : Type w
• R : Type w
• fstFrom : s.L → s.R
• sndFrom : s.L → s.R
• left : s.L → C
• right : s.R → C
• fst : (a : s.L) → CategoryTheory.Limits.MultispanIndex.left s a ⟶ CategoryTheory.Limits.MultispanIndex.right s (CategoryTheory.Limits.MultispanIndex.fstFrom s a)
• snd : (a : s.L) → CategoryTheory.Limits.MultispanIndex.left s a ⟶ CategoryTheory.Limits.MultispanIndex.right s (CategoryTheory.Limits.MultispanIndex.sndFrom s a)

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

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.

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (a : I.L) : (CategoryTheory.Limits.MulticospanIndex.multicospan I).obj (CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.Limits.MulticospanIndex.left I a

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (b : I.R) : (CategoryTheory.Limits.MulticospanIndex.multicospan I).obj (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.Limits.MulticospanIndex.right I b

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map_fst {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (b : I.R) : (CategoryTheory.Limits.MulticospanIndex.multicospan I).map (CategoryTheory.Limits.WalkingMulticospan.Hom.fst b) = CategoryTheory.Limits.MulticospanIndex.fst I b

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map_snd {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MulticospanIndex C) (b : I.R) : (CategoryTheory.Limits.MulticospanIndex.multicospan I).map (CategoryTheory.Limits.WalkingMulticospan.Hom.snd b) = CategoryTheory.Limits.MulticospanIndex.snd I b

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.

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.

@[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 : CategoryTheory.Limits.MulticospanIndex.right I b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fst I 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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I 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 : CategoryTheory.Limits.MulticospanIndex.right I b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.sndPiMap I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.right b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.snd I 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 (CategoryTheory.Limits.MulticospanIndex.sndPiMap I) (CategoryTheory.Limits.Pi.π I.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π I.left (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I b)

@[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), (CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram I).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 => CategoryTheory.Limits.MulticospanIndex.fstPiMap I | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.right => CategoryTheory.Limits.MulticospanIndex.sndPiMap I

@[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) : (CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram I).obj x = match x with | CategoryTheory.Limits.WalkingParallelPair.zero => ∏ I.left | CategoryTheory.Limits.WalkingParallelPair.one => ∏ I.right

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 morphsims ∏ I.left ⇉ ∏ I.right. This is the diagram of the latter.

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.

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (I : CategoryTheory.Limits.MultispanIndex C) (a : I.L) : (CategoryTheory.Limits.MultispanIndex.multispan I).obj (CategoryTheory.Limits.WalkingMultispan.left a) = CategoryTheory.Limits.MultispanIndex.left I 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) : (CategoryTheory.Limits.MultispanIndex.multispan I).obj (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.Limits.MultispanIndex.right I 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) : (CategoryTheory.Limits.MultispanIndex.multispan I).map (CategoryTheory.Limits.WalkingMultispan.Hom.fst a) = CategoryTheory.Limits.MultispanIndex.fst I 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) : (CategoryTheory.Limits.MultispanIndex.multispan I).map (CategoryTheory.Limits.WalkingMultispan.Hom.snd a) = CategoryTheory.Limits.MultispanIndex.snd I 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.

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.

@[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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fst I b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right (CategoryTheory.Limits.MultispanIndex.fstFrom I 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) (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fst I b) (CategoryTheory.Limits.Sigma.ι I.right (CategoryTheory.Limits.MultispanIndex.fstFrom I 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 (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right (CategoryTheory.Limits.MultispanIndex.sndFrom I 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) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I b) (CategoryTheory.Limits.Sigma.ι I.right (CategoryTheory.Limits.MultispanIndex.sndFrom I b))

@[inline, reducible]

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.

@[inline, reducible]

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

A multifork is a cone over a multicospan.

@[inline, reducible]

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

A multicofork is a cocone over a multispan.

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 ⟶ CategoryTheory.Limits.MulticospanIndex.left I a

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

@[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) = CategoryTheory.Limits.Multifork.ι 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 (CategoryTheory.Limits.Multifork.ι K (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I 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 : (CategoryTheory.Limits.MulticospanIndex.multicospan I).obj (CategoryTheory.Limits.WalkingMulticospan.right b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.snd I 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 (CategoryTheory.Limits.Multifork.ι K (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I 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 : CategoryTheory.Limits.MulticospanIndex.left I j ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K₂ j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι 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 (CategoryTheory.Limits.Multifork.ι K₂ j) = CategoryTheory.Limits.Multifork.ι K₁ j

@[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 ⟶ CategoryTheory.Limits.MulticospanIndex.left I a) (w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I b) = CategoryTheory.CategoryStruct.comp (ι (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I b)) : (CategoryTheory.Limits.Multifork.ofι I P ι w).pt = P

@[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 ⟶ CategoryTheory.Limits.MulticospanIndex.left I a) (w : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (ι (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I b) = CategoryTheory.CategoryStruct.comp (ι (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I 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 (ι (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I b)

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

Construct a multifork using a collection ι of morphisms.

@[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 : CategoryTheory.Limits.MulticospanIndex.right I b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fst I b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.snd I 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 (CategoryTheory.Limits.Multifork.ι K (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι K (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I 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) (CategoryTheory.Limits.Multifork.ι K i) = CategoryTheory.Limits.Multifork.ι E i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Multifork.ι K i) = CategoryTheory.Limits.Multifork.ι E i) → m = lift E) (E : CategoryTheory.Limits.Multifork I) : CategoryTheory.Limits.IsLimit.lift (CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq) 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) (CategoryTheory.Limits.Multifork.ι K i) = CategoryTheory.Limits.Multifork.ι E i) (uniq : ∀ (E : CategoryTheory.Limits.Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : I.L), CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Multifork.ι K i) = CategoryTheory.Limits.Multifork.ι E i) → m = lift E) : CategoryTheory.Limits.IsLimit K

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

@[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 (CategoryTheory.Limits.Multifork.ι K)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.Multifork.ι K)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.sndPiMap I) 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 (CategoryTheory.Limits.Multifork.ι K)) (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.Multifork.ι K)) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

@[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) : (CategoryTheory.Limits.Multifork.toPiFork K).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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

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

@[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] : CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.Multifork.toPiFork K) = CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.Multifork.ι 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] : (CategoryTheory.Limits.Multifork.toPiFork K).π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.lift (CategoryTheory.Limits.Multifork.ι K)) (CategoryTheory.Limits.MulticospanIndex.fstPiMap I)

@[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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) : (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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) : CategoryTheory.Limits.Multifork I

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

@[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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) (a : I.L) : CategoryTheory.Limits.Multifork.ι (CategoryTheory.Limits.Multifork.ofPiFork I c) a = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι 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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) (a : I.R) : (CategoryTheory.Limits.Multifork.ofPiFork I c).π.app (CategoryTheory.Limits.WalkingMulticospan.right a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.Pi.π I.right a))

@[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) : (CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor I).obj K = CategoryTheory.Limits.Multifork.toPiFork K

@[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₂) : ((CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor I).map f).hom = f.hom

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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I))

Multifork.toPiFork as a functor.

@[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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) : (CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor I).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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)} {K₂ : CategoryTheory.Limits.Fork (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)} (f : K₁ ⟶ K₂) : ((CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor I).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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)) (CategoryTheory.Limits.Multifork I)

Multifork.ofPiFork as a functor.

@[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] : (CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork I).counitIso = CategoryTheory.NatIso.ofComponents fun K => CategoryTheory.Limits.Fork.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor I) (CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor I)).obj K).pt)

@[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] : (CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork I).unitIso = CategoryTheory.NatIso.ofComponents fun K => CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Multifork I)).obj K).pt)

@[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] : (CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork I).functor = CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor I

@[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] : (CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork I).inverse = CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor I

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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

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.

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) : CategoryTheory.Limits.MultispanIndex.right I b ⟶ K.pt

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

@[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) = CategoryTheory.Limits.Multicofork.π 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 (CategoryTheory.Limits.MultispanIndex.fst I a) (CategoryTheory.Limits.Multicofork.π K (CategoryTheory.Limits.MultispanIndex.fstFrom I 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 (CategoryTheory.Limits.MultispanIndex.snd I a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K (CategoryTheory.Limits.MultispanIndex.sndFrom I 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 (CategoryTheory.Limits.MultispanIndex.snd I a) (CategoryTheory.Limits.Multicofork.π K (CategoryTheory.Limits.MultispanIndex.sndFrom I 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 (CategoryTheory.Limits.Multicofork.π K₁ b) (CategoryTheory.CategoryStruct.comp f.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π 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 (CategoryTheory.Limits.Multicofork.π K₁ b) f.hom = CategoryTheory.Limits.Multicofork.π K₂ b

@[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) → CategoryTheory.Limits.MultispanIndex.right I b ⟶ P) (w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fst I a) (π (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (π (CategoryTheory.Limits.MultispanIndex.sndFrom I a))) : (CategoryTheory.Limits.Multicofork.ofπ I P π w).pt = P

@[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) → CategoryTheory.Limits.MultispanIndex.right I b ⟶ P) (w : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fst I a) (π (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (π (CategoryTheory.Limits.MultispanIndex.sndFrom I 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 (CategoryTheory.Limits.MultispanIndex.fst I a) (π (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) | CategoryTheory.Limits.WalkingMultispan.right b => π b

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

Construct a multicofork using a collection π of morphisms.

@[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 (CategoryTheory.Limits.MultispanIndex.fst I a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K (CategoryTheory.Limits.MultispanIndex.sndFrom I 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 (CategoryTheory.Limits.MultispanIndex.fst I a) (CategoryTheory.Limits.Multicofork.π K (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (CategoryTheory.Limits.Multicofork.π K (CategoryTheory.Limits.MultispanIndex.sndFrom I 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 (CategoryTheory.Limits.Multicofork.π K i) (desc E) = CategoryTheory.Limits.Multicofork.π E i) (uniq : ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K i) m = CategoryTheory.Limits.Multicofork.π E i) → m = desc E) (E : CategoryTheory.Limits.Multicofork I) : CategoryTheory.Limits.IsColimit.desc (CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq) 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 (CategoryTheory.Limits.Multicofork.π K i) (desc E) = CategoryTheory.Limits.Multicofork.π E i) (uniq : ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : I.R), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π K i) m = CategoryTheory.Limits.Multicofork.π E i) → m = desc E) : CategoryTheory.Limits.IsColimit K

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

@[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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.Multicofork.π K)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.Multicofork.π 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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.Multicofork.π K)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I) (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.Multicofork.π 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) : (CategoryTheory.Limits.Multicofork.toSigmaCofork K).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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)

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

@[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] : CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.Multicofork.toSigmaCofork K) = CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.Multicofork.π 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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) : (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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) : CategoryTheory.Limits.Multicofork I

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

@[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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) (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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.Cofork.π 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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) (b : I.R) : (CategoryTheory.Limits.Multicofork.ofSigmaCofork I c).ι.app (CategoryTheory.Limits.WalkingMultispan.right b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.Limits.Cofork.π 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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) (b : I.R) : CategoryTheory.Limits.Multicofork.π (CategoryTheory.Limits.Multicofork.ofSigmaCofork I c) b = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b) (CategoryTheory.Limits.Cofork.π 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₂) : ((CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor I).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) : (CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor I).obj K = CategoryTheory.Limits.Multicofork.toSigmaCofork K

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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I))

Multicofork.toSigmaCofork as a functor.

@[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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)} {K₂ : CategoryTheory.Limits.Cofork (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)} (f : K₁ ⟶ K₂) : ((CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor I).map f).hom = f.hom

@[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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) : (CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor I).obj c = CategoryTheory.Limits.Multicofork.ofSigmaCofork I c

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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)) (CategoryTheory.Limits.Multicofork I)

Multicofork.ofSigmaCofork as a functor.

@[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] : (CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork I).functor = CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor I

@[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] : (CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork I).inverse = CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor I

@[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] : (CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork I).unitIso = CategoryTheory.NatIso.ofComponents fun K => 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] : (CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork I).counitIso = CategoryTheory.NatIso.ofComponents fun K => CategoryTheory.Limits.Cofork.ext (CategoryTheory.Iso.refl ((CategoryTheory.Functor.comp (CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor I) (CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor I)).obj K).pt)

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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)

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.

@[inline, reducible]

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

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

@[inline, reducible]

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.

@[inline, reducible]

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

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

@[inline, reducible]

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.

@[inline, reducible]

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 ⟶ CategoryTheory.Limits.MulticospanIndex.left I a

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

@[inline, reducible]

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.

@[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.Multifork.ι (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 : CategoryTheory.Limits.MulticospanIndex.right I b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.fst I b) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MulticospanIndex.snd I 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 (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I b)

@[inline, reducible]

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 ⟶ CategoryTheory.Limits.MulticospanIndex.left I a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I b) = CategoryTheory.CategoryStruct.comp (k (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I b)) : W ⟶ CategoryTheory.Limits.multiequalizer I

Construct a morphism to the multiequalizer from its universal property.

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 ⟶ CategoryTheory.Limits.MulticospanIndex.left I a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I b) = CategoryTheory.CategoryStruct.comp (k (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I b)) (a : I.L) {Z : C} (h : CategoryTheory.Limits.MulticospanIndex.left I 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 ⟶ CategoryTheory.Limits.MulticospanIndex.left I a) (h : ∀ (b : I.R), CategoryTheory.CategoryStruct.comp (k (CategoryTheory.Limits.MulticospanIndex.fstTo I b)) (CategoryTheory.Limits.MulticospanIndex.fst I b) = CategoryTheory.CategoryStruct.comp (k (CategoryTheory.Limits.MulticospanIndex.sndTo I b)) (CategoryTheory.Limits.MulticospanIndex.snd I 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 {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.instHasEqualizerPiObjLLeftRRightFstPiMapSndPiMap {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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

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 (CategoryTheory.Limits.MulticospanIndex.fstPiMap I) (CategoryTheory.Limits.MulticospanIndex.sndPiMap I)

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

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.

@[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 : CategoryTheory.Limits.MulticospanIndex.left I 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.instMonoMultiequalizerPiObjLLeftι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)

@[inline, reducible]

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

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

@[inline, reducible]

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.

@[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.Multicofork.π (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.ι (CategoryTheory.Limits.MultispanIndex.multispan I) (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 (CategoryTheory.Limits.MultispanIndex.fst I a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I (CategoryTheory.Limits.MultispanIndex.sndFrom I 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 (CategoryTheory.Limits.MultispanIndex.fst I a) (CategoryTheory.Limits.Multicoequalizer.π I (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (CategoryTheory.Limits.Multicoequalizer.π I (CategoryTheory.Limits.MultispanIndex.sndFrom I a))

@[inline, reducible]

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) → CategoryTheory.Limits.MultispanIndex.right I b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fst I a) (k (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (k (CategoryTheory.Limits.MultispanIndex.sndFrom I a))) : CategoryTheory.Limits.multicoequalizer I ⟶ W

Construct a morphism from the multicoequalizer from its universal property.

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) → CategoryTheory.Limits.MultispanIndex.right I b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fst I a) (k (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (k (CategoryTheory.Limits.MultispanIndex.sndFrom I 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) → CategoryTheory.Limits.MultispanIndex.right I b ⟶ W) (h : ∀ (a : I.L), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fst I a) (k (CategoryTheory.Limits.MultispanIndex.fstFrom I a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd I a) (k (CategoryTheory.Limits.MultispanIndex.sndFrom I 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 {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.instHasCoequalizerSigmaObjLLeftRRightFstSigmaMapSndSigmaMap {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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)

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 (CategoryTheory.Limits.MultispanIndex.fstSigmaMap I) (CategoryTheory.Limits.MultispanIndex.sndSigmaMap I)

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

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.

@[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.instEpiSigmaObjRRightMulticoequalizerSigmaπ {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)