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 snd : R → L) : Type (max w w')

The type underlying the multiequalizer diagram.

• left {L : Type w} {R : Type w'} {fst snd : R → L} : L → WalkingMulticospan fst snd
• right {L : Type w} {R : Type w'} {fst snd : R → L} : R → WalkingMulticospan fst snd

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

The type underlying the multiecoqualizer diagram.

• left {L : Type w} {R : Type w'} {fst snd : L → R} : L → WalkingMultispan fst snd
• right {L : Type w} {R : Type w'} {fst snd : L → R} : R → WalkingMultispan fst snd

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

Equations

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

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

Morphisms for WalkingMulticospan.

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

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

Equations

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

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

Composition of morphisms for WalkingMulticospan.

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Morphisms for WalkingMultispan.

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

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

Equations

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

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

Composition of morphisms for WalkingMultispan.

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

The multicospan associated to I : MulticospanIndex.

Equations

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_obj {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) (x : WalkingMulticospan I.fstTo I.sndTo) : I.multicospan.obj x = match x with | WalkingMulticospan.left a => I.left a | WalkingMulticospan.right b => I.right b

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) {x y : WalkingMulticospan I.fstTo I.sndTo} (f : x ⟶ y) : I.multicospan.map f = match x, y, f with | x, .(x), WalkingMulticospan.Hom.id .(x) => CategoryStruct.id ((fun (x : WalkingMulticospan I.fstTo I.sndTo) => match x with | WalkingMulticospan.left a => I.left a | WalkingMulticospan.right b => I.right b) x) | .(WalkingMulticospan.left (I.fstTo b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b | .(WalkingMulticospan.left (I.sndTo b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b

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

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

Equations

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

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

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.fstPiMap_π {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) [HasProduct I.left] [HasProduct I.right] (b : I.R) : CategoryStruct.comp I.fstPiMap (Pi.π I.right b) = CategoryStruct.comp (Pi.π I.left (I.fstTo b)) (I.fst b)

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sndPiMap_π {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) [HasProduct I.left] [HasProduct I.right] (b : I.R) : CategoryStruct.comp I.sndPiMap (Pi.π I.right b) = CategoryStruct.comp (Pi.π I.left (I.sndTo b)) (I.snd b)

@[simp]

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

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

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_obj {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) [HasProduct I.left] [HasProduct I.right] (x : WalkingParallelPair) : I.parallelPairDiagram.obj x = match x with | WalkingParallelPair.zero => ∏ᶜ I.left | WalkingParallelPair.one => ∏ᶜ I.right

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram_map {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) [HasProduct I.left] [HasProduct I.right] {X✝ Y✝ : WalkingParallelPair} (h : X✝ ⟶ Y✝) : I.parallelPairDiagram.map h = match X✝, Y✝, h with | x, .(x), WalkingParallelPairHom.id .(x) => CategoryStruct.id (match x with | WalkingParallelPair.zero => ∏ᶜ I.left | WalkingParallelPair.one => ∏ᶜ I.right) | .(WalkingParallelPair.zero), .(WalkingParallelPair.one), WalkingParallelPairHom.left => I.fstPiMap | .(WalkingParallelPair.zero), .(WalkingParallelPair.one), WalkingParallelPairHom.right => I.sndPiMap

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

The multispan associated to I : MultispanIndex.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_map_fst {C : Type u} [Category.{v, u} C] (I : MultispanIndex C) (a : I.L) : I.multispan.map (WalkingMultispan.Hom.fst a) = I.fst a

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multispan_map_snd {C : Type u} [Category.{v, u} C] (I : MultispanIndex C) (a : I.L) : I.multispan.map (WalkingMultispan.Hom.snd a) = I.snd a

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

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

Equations

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

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

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap {C : Type u} [Category.{v, u} C] (I : MultispanIndex C) [HasCoproduct I.left] [HasCoproduct I.right] (b : I.L) : CategoryStruct.comp (Sigma.ι I.left b) I.fstSigmaMap = CategoryStruct.comp (I.fst b) (Sigma.ι I.right (I.fstFrom b))

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap {C : Type u} [Category.{v, u} C] (I : MultispanIndex C) [HasCoproduct I.left] [HasCoproduct I.right] (b : I.L) : CategoryStruct.comp (Sigma.ι I.left b) I.sndSigmaMap = CategoryStruct.comp (I.snd b) (Sigma.ι I.right (I.sndFrom b))

@[simp]

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

A multifork is a cone over a multicospan.

Equations

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

@[reducible, inline]

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

A multicofork is a cocone over a multispan.

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst {C : Type u} [Category.{v, u} C] {I : MulticospanIndex C} (K : Multifork I) (b : I.R) : K.π.app (WalkingMulticospan.right b) = CategoryStruct.comp (K.ι (I.fstTo b)) (I.fst b)

theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd {C : Type u} [Category.{v, u} C] {I : MulticospanIndex C} (K : Multifork I) (b : I.R) : K.π.app (WalkingMulticospan.right b) = CategoryStruct.comp (K.ι (I.sndTo b)) (I.snd b)

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

@[simp]

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

@[simp]

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

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

Construct a multifork using a collection ι of morphisms.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multifork.condition {C : Type u} [Category.{v, u} C] {I : MulticospanIndex C} (K : Multifork I) (b : I.R) : CategoryStruct.comp (K.ι (I.fstTo b)) (I.fst b) = CategoryStruct.comp (K.ι (I.sndTo b)) (I.snd b)

@[simp]

theorem CategoryTheory.Limits.Multifork.condition_assoc {C : Type u} [Category.{v, u} C] {I : MulticospanIndex C} (K : Multifork I) (b : I.R) {Z : C} (h : I.right b ⟶ Z) : CategoryStruct.comp (K.ι (I.fstTo b)) (CategoryStruct.comp (I.fst b) h) = CategoryStruct.comp (K.ι (I.sndTo b)) (CategoryStruct.comp (I.snd b) h)

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

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

Equations

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

@[simp]

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

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

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

Constructor for morphisms to the point of a limit multifork.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multifork.pi_condition {C : Type u} [Category.{v, u} C] {I : MulticospanIndex C} (K : Multifork I) [HasProduct I.left] [HasProduct I.right] : CategoryStruct.comp (Pi.lift K.ι) I.fstPiMap = CategoryStruct.comp (Pi.lift K.ι) I.sndPiMap

@[simp]

theorem CategoryTheory.Limits.Multifork.pi_condition_assoc {C : Type u} [Category.{v, u} C] {I : MulticospanIndex C} (K : Multifork I) [HasProduct I.left] [HasProduct I.right] {Z : C} (h : ∏ᶜ I.right ⟶ Z) : CategoryStruct.comp (Pi.lift K.ι) (CategoryStruct.comp I.fstPiMap h) = CategoryStruct.comp (Pi.lift K.ι) (CategoryStruct.comp I.sndPiMap h)

noncomputable def CategoryTheory.Limits.Multifork.toPiFork {C : Type u} [Category.{v, u} C] {I : MulticospanIndex C} [HasProduct I.left] [HasProduct I.right] (K : Multifork I) : 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.

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_one {C : Type u} [Category.{v, u} C] {I : MulticospanIndex C} (K : Multifork I) [HasProduct I.left] [HasProduct I.right] : K.toPiFork.π.app WalkingParallelPair.one = CategoryStruct.comp (Pi.lift K.ι) I.fstPiMap

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Multifork.toPiFork as a functor.

Equations

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

@[simp]

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

@[simp]

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

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

Multifork.ofPiFork as a functor.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) [HasProduct I.left] [HasProduct I.right] : I.multiforkEquivPiFork.unitIso = NatIso.ofComponents (fun (K : Multifork I) => Cones.ext (Iso.refl ((Functor.id (Multifork I)).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) [HasProduct I.left] [HasProduct I.right] : I.multiforkEquivPiFork.counitIso = NatIso.ofComponents (fun (K : Fork I.fstPiMap I.sndPiMap) => Fork.ext (Iso.refl ((I.ofPiForkFunctor.comp I.toPiForkFunctor).obj K).pt) ⋯) ⋯

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

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multicofork.fst_app_right {C : Type u} [Category.{v, u} C] {I : MultispanIndex C} (K : Multicofork I) (a : I.L) : K.ι.app (WalkingMultispan.left a) = CategoryStruct.comp (I.fst a) (K.π (I.fstFrom a))

theorem CategoryTheory.Limits.Multicofork.snd_app_right {C : Type u} [Category.{v, u} C] {I : MultispanIndex C} (K : Multicofork I) (a : I.L) : K.ι.app (WalkingMultispan.left a) = CategoryStruct.comp (I.snd a) (K.π (I.sndFrom a))

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

@[simp]

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

@[simp]

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

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

Construct a multicofork using a collection π of morphisms.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multicofork.condition {C : Type u} [Category.{v, u} C] {I : MultispanIndex C} (K : Multicofork I) (a : I.L) : CategoryStruct.comp (I.fst a) (K.π (I.fstFrom a)) = CategoryStruct.comp (I.snd a) (K.π (I.sndFrom a))

@[simp]

theorem CategoryTheory.Limits.Multicofork.condition_assoc {C : Type u} [Category.{v, u} C] {I : MultispanIndex C} (K : Multicofork I) (a : I.L) {Z : C} (h : K.pt ⟶ Z) : CategoryStruct.comp (I.fst a) (CategoryStruct.comp (K.π (I.fstFrom a)) h) = CategoryStruct.comp (I.snd a) (CategoryStruct.comp (K.π (I.sndFrom a)) h)

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

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multicofork.sigma_condition {C : Type u} [Category.{v, u} C] {I : MultispanIndex C} (K : Multicofork I) [HasCoproduct I.left] [HasCoproduct I.right] : CategoryStruct.comp I.fstSigmaMap (Sigma.desc K.π) = CategoryStruct.comp I.sndSigmaMap (Sigma.desc K.π)

@[simp]

theorem CategoryTheory.Limits.Multicofork.sigma_condition_assoc {C : Type u} [Category.{v, u} C] {I : MultispanIndex C} (K : Multicofork I) [HasCoproduct I.left] [HasCoproduct I.right] {Z : C} (h : K.pt ⟶ Z) : CategoryStruct.comp I.fstSigmaMap (CategoryStruct.comp (Sigma.desc K.π) h) = CategoryStruct.comp I.sndSigmaMap (CategoryStruct.comp (Sigma.desc K.π) h)

noncomputable def CategoryTheory.Limits.Multicofork.toSigmaCofork {C : Type u} [Category.{v, u} C] {I : MultispanIndex C} [HasCoproduct I.left] [HasCoproduct I.right] (K : Multicofork I) : 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.

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

Multicofork.toSigmaCofork as a functor.

Equations

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

@[simp]

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

@[simp]

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

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

Multicofork.ofSigmaCofork as a functor.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso {C : Type u} [Category.{v, u} C] (I : MultispanIndex C) [HasCoproduct I.left] [HasCoproduct I.right] : I.multicoforkEquivSigmaCofork.unitIso = NatIso.ofComponents (fun (K : Multicofork I) => Cocones.ext (Iso.refl ((Functor.id (Multicofork I)).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso {C : Type u} [Category.{v, u} C] (I : MultispanIndex C) [HasCoproduct I.left] [HasCoproduct I.right] : I.multicoforkEquivSigmaCofork.counitIso = NatIso.ofComponents (fun (K : Cofork I.fstSigmaMap I.sndSigmaMap) => Cofork.ext (Iso.refl ((I.ofSigmaCoforkFunctor.comp I.toSigmaCoforkFunctor).obj K).pt) ⋯) ⋯

@[simp]

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

@[simp]

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

The multiequalizer of I : MulticospanIndex C.

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

The multiecoqualizer of I : MultispanIndex C.

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

The multifork associated to the multiequalizer.

Equations

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Limits.Multiequalizer.condition {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) [HasMultiequalizer I] (b : I.R) : CategoryStruct.comp (ι I (I.fstTo b)) (I.fst b) = CategoryStruct.comp (ι I (I.sndTo b)) (I.snd b)

theorem CategoryTheory.Limits.Multiequalizer.condition_assoc {C : Type u} [Category.{v, u} C] (I : MulticospanIndex C) [HasMultiequalizer I] (b : I.R) {Z : C} (h : I.right b ⟶ Z) : CategoryStruct.comp (ι I (I.fstTo b)) (CategoryStruct.comp (I.fst b) h) = CategoryStruct.comp (ι I (I.sndTo b)) (CategoryStruct.comp (I.snd b) h)

@[reducible, inline]

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

Construct a morphism to the multiequalizer from its universal property.

Equations

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

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

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

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

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

The multicofork associated to the multicoequalizer.

Equations

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

@[simp]

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

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

@[simp]

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

theorem CategoryTheory.Limits.Multicoequalizer.condition {C : Type u} [Category.{v, u} C] (I : MultispanIndex C) [HasMulticoequalizer I] (a : I.L) : CategoryStruct.comp (I.fst a) (π I (I.fstFrom a)) = CategoryStruct.comp (I.snd a) (π I (I.sndFrom a))

theorem CategoryTheory.Limits.Multicoequalizer.condition_assoc {C : Type u} [Category.{v, u} C] (I : MultispanIndex C) [HasMulticoequalizer I] (a : I.L) {Z : C} (h : multicoequalizer I ⟶ Z) : CategoryStruct.comp (I.fst a) (CategoryStruct.comp (π I (I.fstFrom a)) h) = CategoryStruct.comp (I.snd a) (CategoryStruct.comp (π I (I.sndFrom a)) h)

@[reducible, inline]

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

Construct a morphism from the multicoequalizer from its universal property.

Equations

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

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

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

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

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

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

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

Equations

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

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

The canonical projection ∐ I.right ⟶ multicoequalizer I.

Equations

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

@[simp]

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

@[simp]

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

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