# 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 : RL) (snd : RL) :

The type underlying the multiequalizer diagram.

• left: {L R : Type w} → {fst snd : RL} → L
• right: {L R : Type w} → {fst snd : RL} → R
Instances For
inductive CategoryTheory.Limits.WalkingMultispan {L : Type w} {R : Type w} (fst : LR) (snd : LR) :

The type underlying the multiecoqualizer diagram.

• left: {L R : Type w} → {fst snd : LR} → L
• right: {L R : Type w} → {fst snd : LR} → R
Instances For
instance CategoryTheory.Limits.WalkingMulticospan.instInhabited {L : Type w} {R : Type w} {fst : RL} {snd : RL} [] :
Equations
• CategoryTheory.Limits.WalkingMulticospan.instInhabited = { default := }
inductive CategoryTheory.Limits.WalkingMulticospan.Hom {L : Type w} {R : Type w} {fst : RL} {snd : RL} :

Morphisms for WalkingMulticospan.

• id: {L R : Type w} → {fst snd : RL} → (A : ) → A.Hom A
• fst: {L R : Type w} → {fst snd : RL} → (b : R) →
• snd: {L R : Type w} → {fst snd : RL} → (b : R) →
Instances For
instance CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom {L : Type w} {R : Type w} {fst : RL} {snd : RL} {a : } :
Inhabited (a.Hom a)
Equations
• CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom = { default := }
def CategoryTheory.Limits.WalkingMulticospan.Hom.comp {L : Type w} {R : Type w} {fst : RL} {snd : RL} {A : } {B : } {C : } :
A.Hom BB.Hom CA.Hom C

Composition of morphisms for WalkingMulticospan.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Limits.WalkingMulticospan.instSmallCategory {L : Type w} {R : Type w} {fst : RL} {snd : RL} :
Equations
• CategoryTheory.Limits.WalkingMulticospan.instSmallCategory =
@[simp]
theorem CategoryTheory.Limits.WalkingMulticospan.Hom.id_eq_id {L : Type w} {R : Type w} {fst : RL} {snd : RL} (X : ) :
@[simp]
theorem CategoryTheory.Limits.WalkingMulticospan.Hom.comp_eq_comp {L : Type w} {R : Type w} {fst : RL} {snd : RL} {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
instance CategoryTheory.Limits.WalkingMultispan.instInhabited {L : Type v} {R : Type v} {fst : LR} {snd : LR} [] :
Equations
• CategoryTheory.Limits.WalkingMultispan.instInhabited = { default := }
inductive CategoryTheory.Limits.WalkingMultispan.Hom {L : Type v} {R : Type v} {fst : LR} {snd : LR} :

Morphisms for WalkingMultispan.

• id: {L R : Type v} → {fst snd : LR} → (A : ) → A.Hom A
• fst: {L R : Type v} → {fst snd : LR} → (a : L) →
• snd: {L R : Type v} → {fst snd : LR} → (a : L) →
Instances For
instance CategoryTheory.Limits.WalkingMultispan.instInhabitedHom {L : Type v} {R : Type v} {fst : LR} {snd : LR} {a : } :
Inhabited (a.Hom a)
Equations
• CategoryTheory.Limits.WalkingMultispan.instInhabitedHom = { default := }
def CategoryTheory.Limits.WalkingMultispan.Hom.comp {L : Type v} {R : Type v} {fst : LR} {snd : LR} {A : } {B : } {C : } :
A.Hom BB.Hom CA.Hom C

Composition of morphisms for WalkingMultispan.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.Limits.WalkingMultispan.instSmallCategory {L : Type v} {R : Type v} {fst : LR} {snd : LR} :
Equations
• CategoryTheory.Limits.WalkingMultispan.instSmallCategory =
@[simp]
theorem CategoryTheory.Limits.WalkingMultispan.Hom.id_eq_id {L : Type v} {R : Type v} {fst : LR} {snd : LR} (X : ) :
@[simp]
theorem CategoryTheory.Limits.WalkingMultispan.Hom.comp_eq_comp {L : Type v} {R : Type v} {fst : LR} {snd : LR} {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
structure CategoryTheory.Limits.MulticospanIndex (C : Type u) :
Type (max (max u v) (w + 1))

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

• L : Type w
• R : Type w
• fstTo : self.Rself.L
• sndTo : self.Rself.L
• left : self.LC
• right : self.RC
• 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) :
Type (max (max u v) (w + 1))

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

• L : Type w
• R : Type w
• fstFrom : self.Lself.R
• sndFrom : self.Lself.R
• left : self.LC
• right : self.RC
• 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} (x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) :
I.multicospan.obj x = match x with | => I.left a | => I.right b
@[simp]
theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map {C : Type u} {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.CategoryStruct.id ((fun (x : CategoryTheory.Limits.WalkingMulticospan I.fstTo I.sndTo) => match x with | => I.left a | => I.right b) x) | .(), , => I.fst b | .(), , => I.snd b

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} [] [] :
∏ᶜ I.left ∏ᶜ I.right

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

Equations
Instances For
noncomputable def CategoryTheory.Limits.MulticospanIndex.sndPiMap {C : Type u} [] [] :
∏ᶜ I.left ∏ᶜ I.right

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

Equations
Instances For

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
Instances For

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} (a : I.L) :
I.multispan.obj = I.left a
@[simp]
theorem CategoryTheory.Limits.MultispanIndex.multispan_obj_right {C : Type u} (b : I.R) :
I.multispan.obj = I.right b
@[simp]
theorem CategoryTheory.Limits.MultispanIndex.multispan_map_fst {C : Type u} (a : I.L) :
I.multispan.map = I.fst a
@[simp]
theorem CategoryTheory.Limits.MultispanIndex.multispan_map_snd {C : Type u} (a : I.L) :
I.multispan.map = I.snd a
noncomputable def CategoryTheory.Limits.MultispanIndex.fstSigmaMap {C : Type u} [] [] :
I.left I.right

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

Equations
Instances For
noncomputable def CategoryTheory.Limits.MultispanIndex.sndSigmaMap {C : Type u} [] [] :
I.left I.right

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

Equations
Instances For
@[reducible, inline]

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
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.Multifork {C : Type u} :
Type (max (max w u) v)

A multifork is a cone over a multicospan.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.Multicofork {C : Type u} :
Type (max (max w u) v)

A multicofork is a cocone over a multispan.

Equations
Instances For
def CategoryTheory.Limits.Multifork.ι {C : Type u} (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 =
Instances For
@[simp]
theorem CategoryTheory.Limits.Multifork.app_left_eq_ι {C : Type u} (a : I.L) :
= K a
@[simp]
theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd_assoc {C : Type u} (b : I.R) {Z : C} (h : I.multicospan.obj Z) :
@[simp]
theorem CategoryTheory.Limits.Multifork.hom_comp_ι_assoc {C : Type u} (K₁ : ) (K₂ : ) (f : K₁ K₂) (j : I.L) {Z : C} (h : I.left j Z) :
@[simp]
theorem CategoryTheory.Limits.Multifork.hom_comp_ι {C : Type u} (K₁ : ) (K₂ : ) (f : K₁ K₂) (j : I.L) :
CategoryTheory.CategoryStruct.comp f.hom (K₂ j) = K₁ j
@[simp]
theorem CategoryTheory.Limits.Multifork.ofι_pt {C : Type u} (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)) :
().pt = P
@[simp]
theorem CategoryTheory.Limits.Multifork.ofι_π_app {C : Type u} (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) :
().app x = match x with | => ι a | => CategoryTheory.CategoryStruct.comp (ι (I.fstTo b)) (I.fst b)
def CategoryTheory.Limits.Multifork.ofι {C : Type u} (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)) :

Construct a multifork using a collection ι of morphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem CategoryTheory.Limits.Multifork.condition {C : Type u} (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} (lift : (E : ) → E.pt K.pt) (fac : ∀ (E : ) (i : I.L), CategoryTheory.CategoryStruct.comp (lift E) (K i) = E i) (uniq : ∀ (E : ) (m : E.pt K.pt), (∀ (i : I.L), = E i)m = lift E) :
(CategoryTheory.Limits.Multifork.IsLimit.mk K lift fac uniq).lift E = lift E
def CategoryTheory.Limits.Multifork.IsLimit.mk {C : Type u} (lift : (E : ) → E.pt K.pt) (fac : ∀ (E : ) (i : I.L), CategoryTheory.CategoryStruct.comp (lift E) (K i) = E i) (uniq : ∀ (E : ) (m : E.pt K.pt), (∀ (i : I.L), = E i)m = lift E) :

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

Equations
Instances For
theorem CategoryTheory.Limits.Multifork.IsLimit.hom_ext {C : Type u} (hK : ) {T : C} {f : T K.pt} {g : T K.pt} (h : ∀ (a : I.L), = ) :
f = g
def CategoryTheory.Limits.Multifork.IsLimit.lift {C : Type u} (hK : ) {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
• = hK.lift ()
Instances For
@[simp]
theorem CategoryTheory.Limits.Multifork.IsLimit.fac_assoc {C : Type u} (hK : ) {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) :
@[simp]
theorem CategoryTheory.Limits.Multifork.IsLimit.fac {C : Type u} (hK : ) {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) :
= k a
@[simp]
theorem CategoryTheory.Limits.Multifork.pi_condition_assoc {C : Type u} [] [] {Z : C} (h : ∏ᶜ I.right Z) :
=
@[simp]
theorem CategoryTheory.Limits.Multifork.toPiFork_pt {C : Type u} [] [] :
K.toPiFork.pt = K.pt
noncomputable def CategoryTheory.Limits.Multifork.toPiFork {C : Type u} [] [] :
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} [] [] :
K.toPiFork =
@[simp]
theorem CategoryTheory.Limits.Multifork.ofPiFork_pt {C : Type u} [] [] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) :
= c.pt
noncomputable def CategoryTheory.Limits.Multifork.ofPiFork {C : Type u} [] [] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) :

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} [] [] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) (a : I.L) :
=
@[simp]
theorem CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj {C : Type u} [] [] :
I.toPiForkFunctor.obj K = K.toPiFork
@[simp]
theorem CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom {C : Type u} [] [] {K₁ : } {K₂ : } (f : K₁ K₂) :
(I.toPiForkFunctor.map f).hom = f.hom

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} [] [] (c : CategoryTheory.Limits.Fork I.fstPiMap I.sndPiMap) :
I.ofPiForkFunctor.obj c =
@[simp]
theorem CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_map_hom {C : Type u} [] [] {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

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_inverse {C : Type u} [] [] :
I.multiforkEquivPiFork.inverse = I.ofPiForkFunctor
@[simp]
theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso {C : Type u} [] [] :
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_functor {C : Type u} [] [] :
I.multiforkEquivPiFork.functor = I.toPiForkFunctor
@[simp]
theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso {C : Type u} [] [] :
I.multiforkEquivPiFork.unitIso = CategoryTheory.NatIso.ofComponents (fun (K : ) => )

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} (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
Instances For
@[simp]
theorem CategoryTheory.Limits.Multicofork.π_eq_app_right {C : Type u} (b : I.R) :
K.app = K b
@[simp]
theorem CategoryTheory.Limits.Multicofork.fst_app_right {C : Type u} (a : I.L) :
K.app = CategoryTheory.CategoryStruct.comp (I.fst a) (K (I.fstFrom a))
theorem CategoryTheory.Limits.Multicofork.snd_app_right {C : Type u} (a : I.L) :
K.app = CategoryTheory.CategoryStruct.comp (I.snd a) (K (I.sndFrom a))
@[simp]
theorem CategoryTheory.Limits.Multicofork.π_comp_hom_assoc {C : Type u} (f : K₁ K₂) (b : I.R) {Z : C} (h : K₂.pt Z) :
@[simp]
theorem CategoryTheory.Limits.Multicofork.π_comp_hom {C : Type u} (f : K₁ K₂) (b : I.R) :
CategoryTheory.CategoryStruct.comp (K₁ b) f.hom = K₂ b
@[simp]
theorem CategoryTheory.Limits.Multicofork.ofπ_pt {C : Type u} (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))) :
().pt = P
@[simp]
theorem CategoryTheory.Limits.Multicofork.ofπ_ι_app {C : Type u} (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) :
().app x = match x with | => CategoryTheory.CategoryStruct.comp (I.fst a) (π (I.fstFrom a)) | => π b
def CategoryTheory.Limits.Multicofork.ofπ {C : Type u} (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))) :

Construct a multicofork using a collection π of morphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem CategoryTheory.Limits.Multicofork.condition {C : Type u} (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} (desc : (E : ) → K.pt E.pt) (fac : ∀ (E : ) (i : I.R), CategoryTheory.CategoryStruct.comp (K i) (desc E) = E i) (uniq : ∀ (E : ) (m : K.pt E.pt), (∀ (i : I.R), = E i)m = desc E) :
(CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq).desc E = desc E
def CategoryTheory.Limits.Multicofork.IsColimit.mk {C : Type u} (desc : (E : ) → K.pt E.pt) (fac : ∀ (E : ) (i : I.R), CategoryTheory.CategoryStruct.comp (K i) (desc E) = E i) (uniq : ∀ (E : ) (m : K.pt E.pt), (∀ (i : I.R), = E i)m = desc E) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.Multicofork.sigma_condition_assoc {C : Type u} [] [] {Z : C} (h : K.pt Z) :
=
@[simp]
theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_pt {C : Type u} [] [] :
K.toSigmaCofork.pt = K.pt
noncomputable def CategoryTheory.Limits.Multicofork.toSigmaCofork {C : Type u} [] [] :
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} [] [] :
K.toSigmaCofork =
@[simp]
theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_pt {C : Type u} [] [] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) :
= c.pt
noncomputable def CategoryTheory.Limits.Multicofork.ofSigmaCofork {C : Type u} [] [] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) :

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
theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right {C : Type u} [] [] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) (b : I.R) :
@[simp]
theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right' {C : Type u} [] [] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) (b : I.R) :
@[simp]
theorem CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_map_hom {C : Type u} [] [] (f : K₁ K₂) :
(I.toSigmaCoforkFunctor.map f).hom = f.hom
@[simp]
theorem CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_obj {C : Type u} [] [] :
I.toSigmaCoforkFunctor.obj K = K.toSigmaCofork

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} [] [] (c : CategoryTheory.Limits.Cofork I.fstSigmaMap I.sndSigmaMap) :
I.ofSigmaCoforkFunctor.obj c =
@[simp]
theorem CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_map_hom {C : Type u} [] [] {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

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_inverse {C : Type u} [] [] :
I.multicoforkEquivSigmaCofork.inverse = I.ofSigmaCoforkFunctor
@[simp]
theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso {C : Type u} [] [] :
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_functor {C : Type u} [] [] :
I.multicoforkEquivSigmaCofork.functor = I.toSigmaCoforkFunctor
@[simp]
theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso {C : Type u} [] [] :
I.multicoforkEquivSigmaCofork.unitIso = CategoryTheory.NatIso.ofComponents (fun (K : ) => )

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]

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

Equations
Instances For
@[reducible, inline]

The multiequalizer of I : MulticospanIndex C.

Equations
Instances For
@[reducible, inline]

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

Equations
Instances For
@[reducible, inline]

The multiecoqualizer of I : MultispanIndex C.

Equations
Instances For
@[reducible, inline]
abbrev CategoryTheory.Limits.Multiequalizer.ι {C : Type u} (a : I.L) :
I.left a

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

Equations
Instances For
@[reducible, inline]

The multifork associated to the multiequalizer.

Equations
Instances For
@[simp]
@[simp]
@[reducible, inline]
abbrev CategoryTheory.Limits.Multiequalizer.lift {C : Type u} (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)) :

Construct a morphism to the multiequalizer from its universal property.

Equations
Instances For
theorem CategoryTheory.Limits.Multiequalizer.lift_ι_assoc {C : Type u} (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) :
theorem CategoryTheory.Limits.Multiequalizer.lift_ι {C : Type u} (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) :
theorem CategoryTheory.Limits.Multiequalizer.hom_ext {C : Type u} {W : C} (i : ) (j : ) (h : ) :
i = j

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

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} [] [] (a : I.L) {Z : C} (h : I.left a Z) :
@[simp]
Equations
• =
@[reducible, inline]
abbrev CategoryTheory.Limits.Multicoequalizer.π {C : Type u} (b : I.R) :
I.right b

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

Equations
Instances For
@[reducible, inline]

The multicofork associated to the multicoequalizer.

Equations
Instances For
@[simp]
@[simp]
@[reducible, inline]
abbrev CategoryTheory.Limits.Multicoequalizer.desc {C : Type u} (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))) :

Construct a morphism from the multicoequalizer from its universal property.

Equations
Instances For
theorem CategoryTheory.Limits.Multicoequalizer.π_desc_assoc {C : Type u} (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) :
theorem CategoryTheory.Limits.Multicoequalizer.π_desc {C : Type u} (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) :
theorem CategoryTheory.Limits.Multicoequalizer.hom_ext {C : Type u} {W : C} (i : ) (j : ) (h : ) :
i = j

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

The canonical projection ∐ I.right ⟶ multicoequalizer I.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
Equations
• =