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).

structure CategoryTheory.Limits.MulticospanShape : Type (max (w + 1) (w' + 1))

The shape of a multiequalizer diagram. It involves two types L and R, and two maps R → L.

• L : Type w

  the left type

• R : Type w'

  the right type

• fst : self.R → self.L

  the first map R → L

• snd : self.R → self.L

  the second map R → L

def CategoryTheory.Limits.MulticospanShape.prod (ι : Type w) : MulticospanShape

Given a type ι, this is the shape of multiequalizer diagrams corresponding to situations where we want to equalize two families of maps U i ⟶ V ⟨i, j⟩ and U j ⟶ V ⟨i, j⟩ with i : ι and j : ι.

Equations

• CategoryTheory.Limits.MulticospanShape.prod ι = { L := ι, R := ι × ι, fst := Prod.fst, snd := Prod.snd }

@[simp]

theorem CategoryTheory.Limits.MulticospanShape.prod_R (ι : Type w) : (prod ι).R = (ι × ι)

@[simp]

theorem CategoryTheory.Limits.MulticospanShape.prod_fst (ι : Type w) (self : ι × ι) : (prod ι).fst self = self.1

@[simp]

theorem CategoryTheory.Limits.MulticospanShape.prod_snd (ι : Type w) (self : ι × ι) : (prod ι).snd self = self.2

@[simp]

theorem CategoryTheory.Limits.MulticospanShape.prod_L (ι : Type w) : (prod ι).L = ι

structure CategoryTheory.Limits.MultispanShape : Type (max (w + 1) (w' + 1))

The shape of a multicoequalizer diagram. It involves two types L and R, and two maps L → R.

• L : Type w

  the left type

• R : Type w'

  the right type

• fst : self.L → self.R

  the first map L → R

• snd : self.L → self.R

  the second map L → R

def CategoryTheory.Limits.MultispanShape.prod (ι : Type w) : MultispanShape

Given a type ι, this is the shape of multicoequalizer diagrams corresponding to situations where we want to coequalize two families of maps V ⟨i, j⟩ ⟶ U i and V ⟨i, j⟩ ⟶ U j with i : ι and j : ι.

Equations

• CategoryTheory.Limits.MultispanShape.prod ι = { L := ι × ι, R := ι, fst := Prod.fst, snd := Prod.snd }

@[simp]

theorem CategoryTheory.Limits.MultispanShape.prod_snd (ι : Type w) (self : ι × ι) : (prod ι).snd self = self.2

@[simp]

theorem CategoryTheory.Limits.MultispanShape.prod_L (ι : Type w) : (prod ι).L = (ι × ι)

@[simp]

theorem CategoryTheory.Limits.MultispanShape.prod_R (ι : Type w) : (prod ι).R = ι

@[simp]

theorem CategoryTheory.Limits.MultispanShape.prod_fst (ι : Type w) (self : ι × ι) : (prod ι).fst self = self.1

def CategoryTheory.Limits.MultispanShape.ofLinearOrder (ι : Type w) [LinearOrder ι] : MultispanShape

Given a linearly ordered type ι, this is the shape of multicoequalizer diagrams corresponding to situations where we want to coequalize two families of maps V ⟨i, j⟩ ⟶ U i and V ⟨i, j⟩ ⟶ U j with i < j.

Equations

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

@[simp]

theorem CategoryTheory.Limits.MultispanShape.ofLinearOrder_L (ι : Type w) [LinearOrder ι] : (ofLinearOrder ι).L = ↑{x : ι × ι | x.1 < x.2}

@[simp]

theorem CategoryTheory.Limits.MultispanShape.ofLinearOrder_fst (ι : Type w) [LinearOrder ι] (x : ↑{x : ι × ι | x.1 < x.2}) : (ofLinearOrder ι).fst x = (↑x).1

@[simp]

theorem CategoryTheory.Limits.MultispanShape.ofLinearOrder_R (ι : Type w) [LinearOrder ι] : (ofLinearOrder ι).R = ι

@[simp]

theorem CategoryTheory.Limits.MultispanShape.ofLinearOrder_snd (ι : Type w) [LinearOrder ι] (x : ↑{x : ι × ι | x.1 < x.2}) : (ofLinearOrder ι).snd x = (↑x).2

instance CategoryTheory.Limits.instUniqueLOfLinearOrderBool : Unique (MultispanShape.ofLinearOrder Bool).L

Equations

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

inductive CategoryTheory.Limits.WalkingMulticospan (J : MulticospanShape) : Type (max w w')

The type underlying the multiequalizer diagram.

• left {J : MulticospanShape} : J.L → WalkingMulticospan J
• right {J : MulticospanShape} : J.R → WalkingMulticospan J

inductive CategoryTheory.Limits.WalkingMultispan (J : MultispanShape) : Type (max w w')

The type underlying the multicoequalizer diagram.

• left {J : MultispanShape} : J.L → WalkingMultispan J
• right {J : MultispanShape} : J.R → WalkingMultispan J

instance CategoryTheory.Limits.WalkingMulticospan.instInhabitedOfL {J : MulticospanShape} [Inhabited J.L] : Inhabited (WalkingMulticospan J)

Equations

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

inductive CategoryTheory.Limits.WalkingMulticospan.Hom {J : MulticospanShape} : WalkingMulticospan J → WalkingMulticospan J → Type (max w w')

Morphisms for WalkingMulticospan.

• id {J : MulticospanShape} (A : WalkingMulticospan J) : A.Hom A
• fst {J : MulticospanShape} (b : J.R) : (left (J.fst b)).Hom (right b)
• snd {J : MulticospanShape} (b : J.R) : (left (J.snd b)).Hom (right b)

instance CategoryTheory.Limits.WalkingMulticospan.instInhabitedHom {J : MulticospanShape} {a : WalkingMulticospan J} : Inhabited (a.Hom a)

Equations

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

def CategoryTheory.Limits.WalkingMulticospan.Hom.comp {J : MulticospanShape} {A B C : WalkingMulticospan J} : 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 {J : MulticospanShape} : SmallCategory (WalkingMulticospan J)

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingMulticospan.Hom.id_eq_id {J : MulticospanShape} (X : WalkingMulticospan J) : id X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.WalkingMulticospan.Hom.comp_eq_comp {J : MulticospanShape} {X Y Z : WalkingMulticospan J} (f : X ⟶ Y) (g : Y ⟶ Z) : comp f g = CategoryStruct.comp f g

def CategoryTheory.Limits.WalkingMulticospan.functorExt {J : MulticospanShape} {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor (WalkingMulticospan J) C} (left : (i : J.L) → F.obj (left i) ≅ G.obj (left i)) (right : (i : J.R) → F.obj (right i) ≅ G.obj (right i)) (wl : ∀ (i : J.R), CategoryStruct.comp (F.map (Hom.fst i)) (right i).hom = CategoryStruct.comp (left (J.fst i)).hom (G.map (Hom.fst i)) := by cat_disch) (wr : ∀ (i : J.R), CategoryStruct.comp (F.map (Hom.snd i)) (right i).hom = CategoryStruct.comp (left (J.snd i)).hom (G.map (Hom.snd i)) := by cat_disch) : F ≅ G

Construct a natural isomorphism between functors out of a walking multicospan from its components.

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingMulticospan.functorExt_inv_app {J : MulticospanShape} {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor (WalkingMulticospan J) C} (left : (i : J.L) → F.obj (left i) ≅ G.obj (left i)) (right : (i : J.R) → F.obj (right i) ≅ G.obj (right i)) (wl : ∀ (i : J.R), CategoryStruct.comp (F.map (Hom.fst i)) (right i).hom = CategoryStruct.comp (left (J.fst i)).hom (G.map (Hom.fst i)) := by cat_disch) (wr : ∀ (i : J.R), CategoryStruct.comp (F.map (Hom.snd i)) (right i).hom = CategoryStruct.comp (left (J.snd i)).hom (G.map (Hom.snd i)) := by cat_disch) (X : WalkingMulticospan J) : (functorExt left right wl wr).inv.app X = (match X with | WalkingMulticospan.left i => left i | WalkingMulticospan.right i => right i).inv

@[simp]

theorem CategoryTheory.Limits.WalkingMulticospan.functorExt_hom_app {J : MulticospanShape} {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor (WalkingMulticospan J) C} (left : (i : J.L) → F.obj (left i) ≅ G.obj (left i)) (right : (i : J.R) → F.obj (right i) ≅ G.obj (right i)) (wl : ∀ (i : J.R), CategoryStruct.comp (F.map (Hom.fst i)) (right i).hom = CategoryStruct.comp (left (J.fst i)).hom (G.map (Hom.fst i)) := by cat_disch) (wr : ∀ (i : J.R), CategoryStruct.comp (F.map (Hom.snd i)) (right i).hom = CategoryStruct.comp (left (J.snd i)).hom (G.map (Hom.snd i)) := by cat_disch) (X : WalkingMulticospan J) : (functorExt left right wl wr).hom.app X = (match X with | WalkingMulticospan.left i => left i | WalkingMulticospan.right i => right i).hom

instance CategoryTheory.Limits.WalkingMultispan.instInhabitedOfL {J : MultispanShape} [Inhabited J.L] : Inhabited (WalkingMultispan J)

Equations

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

instance CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR {J : MultispanShape} [Small.{t, w} J.L] [Small.{t, w'} J.R] : Small.{t, max w' w} (WalkingMultispan J)

inductive CategoryTheory.Limits.WalkingMultispan.Hom {J : MultispanShape} : WalkingMultispan J → WalkingMultispan J → Type (max w w')

Morphisms for WalkingMultispan.

• id {J : MultispanShape} (A : WalkingMultispan J) : A.Hom A
• fst {J : MultispanShape} (a : J.L) : (left a).Hom (right (J.fst a))
• snd {J : MultispanShape} (a : J.L) : (left a).Hom (right (J.snd a))

instance CategoryTheory.Limits.WalkingMultispan.instInhabitedHom {J : MultispanShape} {a : WalkingMultispan J} : Inhabited (a.Hom a)

Equations

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

def CategoryTheory.Limits.WalkingMultispan.Hom.comp {J : MultispanShape} {A B C : WalkingMultispan J} : 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 {J : MultispanShape} : SmallCategory (WalkingMultispan J)

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.Hom.id_eq_id {J : MultispanShape} (X : WalkingMultispan J) : id X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.Hom.comp_eq_comp {J : MultispanShape} {X Y Z : WalkingMultispan J} (f : X ⟶ Y) (g : Y ⟶ Z) : comp f g = CategoryStruct.comp f g

def CategoryTheory.Limits.WalkingMultispan.functorExt {J : MultispanShape} {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor (WalkingMultispan J) C} (left : (i : J.L) → F.obj (left i) ≅ G.obj (left i)) (right : (i : J.R) → F.obj (right i) ≅ G.obj (right i)) (wl : ∀ (i : J.L), CategoryStruct.comp (F.map (Hom.fst i)) (right (J.fst i)).hom = CategoryStruct.comp (left i).hom (G.map (Hom.fst i)) := by cat_disch) (wr : ∀ (i : J.L), CategoryStruct.comp (F.map (Hom.snd i)) (right (J.snd i)).hom = CategoryStruct.comp (left i).hom (G.map (Hom.snd i)) := by cat_disch) : F ≅ G

Construct a natural isomorphism between functors out of a walking multispan from its components.

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.functorExt_hom_app {J : MultispanShape} {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor (WalkingMultispan J) C} (left : (i : J.L) → F.obj (left i) ≅ G.obj (left i)) (right : (i : J.R) → F.obj (right i) ≅ G.obj (right i)) (wl : ∀ (i : J.L), CategoryStruct.comp (F.map (Hom.fst i)) (right (J.fst i)).hom = CategoryStruct.comp (left i).hom (G.map (Hom.fst i)) := by cat_disch) (wr : ∀ (i : J.L), CategoryStruct.comp (F.map (Hom.snd i)) (right (J.snd i)).hom = CategoryStruct.comp (left i).hom (G.map (Hom.snd i)) := by cat_disch) (X : WalkingMultispan J) : (functorExt left right wl wr).hom.app X = (match X with | WalkingMultispan.left i => left i | WalkingMultispan.right i => right i).hom

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.functorExt_inv_app {J : MultispanShape} {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor (WalkingMultispan J) C} (left : (i : J.L) → F.obj (left i) ≅ G.obj (left i)) (right : (i : J.R) → F.obj (right i) ≅ G.obj (right i)) (wl : ∀ (i : J.L), CategoryStruct.comp (F.map (Hom.fst i)) (right (J.fst i)).hom = CategoryStruct.comp (left i).hom (G.map (Hom.fst i)) := by cat_disch) (wr : ∀ (i : J.L), CategoryStruct.comp (F.map (Hom.snd i)) (right (J.snd i)).hom = CategoryStruct.comp (left i).hom (G.map (Hom.snd i)) := by cat_disch) (X : WalkingMultispan J) : (functorExt left right wl wr).inv.app X = (match X with | WalkingMultispan.left i => left i | WalkingMultispan.right i => right i).inv

instance CategoryTheory.Limits.WalkingMultispan.instUniqueHom {J : MultispanShape} (a : WalkingMultispan J) : Unique (a ⟶ a)

Equations

• a.instUniqueHom = { default := CategoryTheory.CategoryStruct.id a, uniq := ⋯ }

instance CategoryTheory.Limits.WalkingMultispan.instSubsingletonHomLeft {J : MultispanShape} (a b : J.L) : Subsingleton (left a ⟶ left b)

instance CategoryTheory.Limits.WalkingMultispan.instSubsingletonHomRight {J : MultispanShape} (a b : J.R) : Subsingleton (right a ⟶ right b)

instance CategoryTheory.Limits.WalkingMultispan.instIsEmptyHomRightLeft {J : MultispanShape} (a : J.R) (b : J.L) : IsEmpty (right a ⟶ left b)

instance CategoryTheory.Limits.WalkingMultispan.instLocallySmall {J : MultispanShape} : LocallySmall.{t, max w w', max w' w} (WalkingMultispan J)

def CategoryTheory.Limits.WalkingMultispan.equiv (J : MultispanShape) : WalkingMultispan J ≃ J.L ⊕ J.R

The bijection WalkingMultispan J ≃ J.L ⊕ J.R.

Equations

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

def CategoryTheory.Limits.WalkingMultispan.arrowEquiv (J : MultispanShape) : Arrow (WalkingMultispan J) ≃ WalkingMultispan J ⊕ J.L ⊕ J.L

The bijection Arrow (WalkingMultispan J) ≃ WalkingMultispan J ⊕ J.R ⊕ J.R.

Equations

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

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

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

• left : J.L → C

  Left map, from J.L to C

• right : J.R → C

  Right map, from J.R to C

• fst (b : J.R) : self.left (J.fst b) ⟶ self.right b

  A family of maps from left (J.fst b) to right b

• snd (b : J.R) : self.left (J.snd b) ⟶ self.right b

  A family of maps from left (J.snd b) to right b

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

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

• left : J.L → C

  Left map, from J.L to C

• right : J.R → C

  Right map, from J.R to C

• fst (a : J.L) : self.left a ⟶ self.right (J.fst a)

  A family of maps from left a to right (J.fst a)

• snd (a : J.L) : self.left a ⟶ self.right (J.snd a)

  A family of maps from left a to right (J.snd a)

def CategoryTheory.Limits.MulticospanIndex.multicospan {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) : Functor (WalkingMulticospan J) 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_map {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {x y : WalkingMulticospan J} (f : x ⟶ y) : I.multicospan.map f = match x, y, f with | x, .(x), WalkingMulticospan.Hom.id .(x) => CategoryStruct.id (match x with | WalkingMulticospan.left a => I.left a | WalkingMulticospan.right b => I.right b) | .(WalkingMulticospan.left (J.fst b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.fst b => I.fst b | .(WalkingMulticospan.left (J.snd b)), .(WalkingMulticospan.right b), WalkingMulticospan.Hom.snd b => I.snd b

@[simp]

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

def CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) : c.pt ⟶ d.pt

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

Equations

• I.fstPiMapOfIsLimit c hd = CategoryTheory.Limits.Fan.IsLimit.desc hd fun (i : J.R) => CategoryTheory.CategoryStruct.comp (c.proj (J.fst i)) (I.fst i)

def CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) : c.pt ⟶ d.pt

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

Equations

• I.sndPiMapOfIsLimit c hd = CategoryTheory.Limits.Fan.IsLimit.desc hd fun (i : J.R) => CategoryTheory.CategoryStruct.comp (c.proj (J.snd i)) (I.snd i)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) (i : J.R) : CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i) = CategoryStruct.comp (c.proj (J.fst i)) (I.fst i)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj_assoc {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z) : CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (CategoryStruct.comp (d.proj i) h) = CategoryStruct.comp (c.proj (J.fst i)) (CategoryStruct.comp (I.fst i) h)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) (i : J.R) : CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (d.proj i) = CategoryStruct.comp (c.proj (J.snd i)) (I.snd i)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj_assoc {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) (i : J.R) {Z : C} (h : I.right i ⟶ Z) : CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) (CategoryStruct.comp (d.proj i) h) = CategoryStruct.comp (c.proj (J.snd i)) (CategoryStruct.comp (I.snd i) h)

noncomputable def CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) : 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 for limiting fans.

Equations

• I.parallelPairDiagramOfIsLimit c hd = CategoryTheory.Limits.parallelPair (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_obj {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) (x : WalkingParallelPair) : (I.parallelPairDiagramOfIsLimit c hd).obj x = match x with | WalkingParallelPair.zero => c.pt | WalkingParallelPair.one => d.pt

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.parallelPairDiagramOfIsLimit_map {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (c : Fan I.left) {d : Fan I.right} (hd : IsLimit d) {X✝ Y✝ : WalkingParallelPair} (h : X✝ ⟶ Y✝) : (I.parallelPairDiagramOfIsLimit c hd).map h = match X✝, Y✝, h with | x, .(x), WalkingParallelPairHom.id .(x) => CategoryStruct.id (match x with | WalkingParallelPair.zero => c.pt | WalkingParallelPair.one => d.pt) | .(WalkingParallelPair.zero), .(WalkingParallelPair.one), WalkingParallelPairHom.left => I.fstPiMapOfIsLimit c hd | .(WalkingParallelPair.zero), .(WalkingParallelPair.one), WalkingParallelPairHom.right => I.sndPiMapOfIsLimit c hd

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

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

Equations

• I.fstPiMap = I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))

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

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

Equations

• I.sndPiMap = I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left)) (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Limits.MulticospanIndex.parallelPairDiagram {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MultispanShape} (I : MultispanIndex J C) : Functor (WalkingMultispan J) 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] {J : MultispanShape} (I : MultispanIndex J C) (a : J.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] {J : MultispanShape} (I : MultispanIndex J C) (b : J.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] {J : MultispanShape} (I : MultispanIndex J C) (a : J.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] {J : MultispanShape} (I : MultispanIndex J C) (a : J.L) : I.multispan.map (WalkingMultispan.Hom.snd a) = I.snd a

def CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimit {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) : c.pt ⟶ d.pt

The induced map ∐ I.left ⟶ ∐ I.right via I.fst for colimiting cofans.

Equations

• I.fstSigmaMapOfIsColimit d hc = CategoryTheory.Limits.Cofan.IsColimit.desc hc fun (i : J.L) => CategoryTheory.CategoryStruct.comp (I.fst i) (d.inj (J.fst i))

def CategoryTheory.Limits.MultispanIndex.sndSigmaMapOfIsColimit {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) : c.pt ⟶ d.pt

The induced map ∐ I.left ⟶ ∐ I.right via I.snd for colimiting cofans.

Equations

• I.sndSigmaMapOfIsColimit d hc = CategoryTheory.Limits.Cofan.IsColimit.desc hc fun (i : J.L) => CategoryTheory.CategoryStruct.comp (I.snd i) (d.inj (J.snd i))

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) (i : J.L) : CategoryStruct.comp (c.inj i) (I.fstSigmaMapOfIsColimit d hc) = CategoryStruct.comp (I.fst i) (d.inj (J.fst i))

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) (i : J.L) {Z : C} (h : d.pt ⟶ Z) : CategoryStruct.comp (c.inj i) (CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) h) = CategoryStruct.comp (I.fst i) (CategoryStruct.comp (d.inj (J.fst i)) h)

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) (i : J.L) : CategoryStruct.comp (c.inj i) (I.sndSigmaMapOfIsColimit d hc) = CategoryStruct.comp (I.snd i) (d.inj (J.snd i))

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) (i : J.L) {Z : C} (h : d.pt ⟶ Z) : CategoryStruct.comp (c.inj i) (CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc) h) = CategoryStruct.comp (I.snd i) (CategoryStruct.comp (d.inj (J.snd i)) h)

noncomputable def CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) : Functor WalkingParallelPair C

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

Equations

• I.parallelPairDiagramOfIsColimit d hc = CategoryTheory.Limits.parallelPair (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit_obj {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) (x : WalkingParallelPair) : (I.parallelPairDiagramOfIsColimit d hc).obj x = match x with | WalkingParallelPair.zero => c.pt | WalkingParallelPair.one => d.pt

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.parallelPairDiagramOfIsColimit_map {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (d : Cofan I.right) (hc : IsColimit c) {X✝ Y✝ : WalkingParallelPair} (h : X✝ ⟶ Y✝) : (I.parallelPairDiagramOfIsColimit d hc).map h = match X✝, Y✝, h with | x, .(x), WalkingParallelPairHom.id .(x) => CategoryStruct.id (match x with | WalkingParallelPair.zero => c.pt | WalkingParallelPair.one => d.pt) | .(WalkingParallelPair.zero), .(WalkingParallelPair.one), WalkingParallelPairHom.left => I.fstSigmaMapOfIsColimit d hc | .(WalkingParallelPair.zero), .(WalkingParallelPair.one), WalkingParallelPairHom.right => I.sndSigmaMapOfIsColimit d hc

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (b : J.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 (J.fst b)) h)

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (b : J.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 (J.snd b)) h)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.MultispanIndex.parallelPairDiagram {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J 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 morphisms ∐ 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] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MultispanShape} (I : MultispanIndex J 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] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) (a : J.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] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) (a : J.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] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) (b : J.R) : K.π.app (WalkingMulticospan.right b) = CategoryStruct.comp (K.ι (J.fst b)) (I.fst b)

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multifork.hom_comp_ι_assoc {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K₁ K₂ : Multifork I) (f : K₁ ⟶ K₂) (j : J.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] {J : MulticospanShape} (I : MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a) (w : ∀ (b : J.R), CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryStruct.comp (ι (J.snd 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] {J : MulticospanShape} (I : MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a) (w : ∀ (b : J.R), CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryStruct.comp (ι (J.snd b)) (I.snd b)) : (ofι I P ι w).pt = P

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Multifork.ext {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {t s : Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : t ≅ s

Constructor for isomorphisms between multiforks.

Equations

• CategoryTheory.Limits.Multifork.ext e h = CategoryTheory.Limits.Cones.ext e ⋯

@[simp]

theorem CategoryTheory.Limits.Multifork.ext_inv_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {t s : Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : (ext e h).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Limits.Multifork.ext_hom_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {t s : Multifork I} (e : t.pt ≅ s.pt) (h : ∀ (i : J.L), CategoryStruct.comp e.hom (s.ι i) = t.ι i := by cat_disch) : (ext e h).hom.hom = e.hom

def CategoryTheory.Limits.Multifork.isoOfι {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (t : Multifork I) : t ≅ ofι I t.pt t.ι ⋯

Every multifork is isomorphic to one of the form Multifork.ofι.

Equations

• t.isoOfι = CategoryTheory.Limits.Multifork.ext (CategoryTheory.Iso.refl t.pt) ⋯

@[simp]

theorem CategoryTheory.Limits.Multifork.isoOfι_hom_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (t : Multifork I) : t.isoOfι.hom.hom = CategoryStruct.id t.pt

@[simp]

theorem CategoryTheory.Limits.Multifork.isoOfι_inv_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (t : Multifork I) : t.isoOfι.inv.hom = CategoryStruct.id t.pt

def CategoryTheory.Limits.Multifork.IsLimit.mk {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) (lift : (E : Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : Multifork I) (i : J.L), CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.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] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) (lift : (E : Multifork I) → E.pt ⟶ K.pt) (fac : ∀ (E : Multifork I) (i : J.L), CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.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] {J : MulticospanShape} {I : MulticospanIndex J C} {K : Multifork I} (hK : IsLimit K) {T : C} {f g : T ⟶ K.pt} (h : ∀ (a : J.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] {J : MulticospanShape} {I : MulticospanIndex J C} {K : Multifork I} (hK : IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd 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] {J : MulticospanShape} {I : MulticospanIndex J C} {K : Multifork I} (hK : IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.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] {J : MulticospanShape} {I : MulticospanIndex J C} {K : Multifork I} (hK : IsLimit K) {T : C} (k : (a : J.L) → T ⟶ I.left a) (hk : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) {Z : C} (h : I.left a ⟶ Z) : CategoryStruct.comp (lift hK k hk) (CategoryStruct.comp (K.ι a) h) = CategoryStruct.comp (k a) h

def CategoryTheory.Limits.Multifork.isLimitEquivOfIsos {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I I' : MulticospanIndex J C} (c : Multifork I) (c' : Multifork I') (e : c.pt ≅ c'.pt) (el : (i : J.L) → I.left i ≅ I'.left i) (er : (i : J.R) → I.right i ≅ I'.right i) (hl : ∀ (i : J.R), CategoryStruct.comp (I.fst i) (er i).hom = CategoryStruct.comp (el (J.fst i)).hom (I'.fst i) := by cat_disch) (hr : ∀ (i : J.R), CategoryStruct.comp (I.snd i) (er i).hom = CategoryStruct.comp (el (J.snd i)).hom (I'.snd i) := by cat_disch) (he : ∀ (i : J.L), CategoryStruct.comp e.hom (c'.ι i) = CategoryStruct.comp (c.ι i) (el i).hom := by cat_disch) : IsLimit c ≃ IsLimit c'

Given two multiforks with isomorphic components in such a way that the natural diagrams commute, then one is a limit if and only if the other one is.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Multifork.pi_condition {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : CategoryStruct.comp (Fan.IsLimit.desc hc K.ι) (I.fstPiMapOfIsLimit c hd) = CategoryStruct.comp (Fan.IsLimit.desc hc K.ι) (I.sndPiMapOfIsLimit c hd)

@[simp]

theorem CategoryTheory.Limits.Multifork.pi_condition_assoc {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) {Z : C} (h : d.pt ⟶ Z) : CategoryStruct.comp (Fan.IsLimit.desc hc K.ι) (CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) h) = CategoryStruct.comp (Fan.IsLimit.desc hc K.ι) (CategoryStruct.comp (I.sndPiMapOfIsLimit c hd) h)

def CategoryTheory.Limits.Multifork.toPiFork {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) (K : Multifork I) : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)

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

Equations

• CategoryTheory.Limits.Multifork.toPiFork hc hd K = CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.Fan.IsLimit.desc hc K.ι) ⋯

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_pt {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) (K : Multifork I) : (toPiFork hc hd K).pt = K.pt

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_zero {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : (toPiFork hc hd K).ι = Fan.IsLimit.desc hc K.ι

@[simp]

theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_one {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : (toPiFork hc hd K).π.app WalkingParallelPair.one = CategoryStruct.comp (Fan.IsLimit.desc hc K.ι) (I.fstPiMapOfIsLimit c hd)

def CategoryTheory.Limits.Multifork.ofPiFork {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {c : Fan I.left} {d : Fan I.right} {hd : IsLimit d} (a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : 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] {J : MulticospanShape} {I : MulticospanIndex J C} {c : Fan I.left} {d : Fan I.right} {hd : IsLimit d} (a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (ofPiFork a).pt = a.pt

@[simp]

theorem CategoryTheory.Limits.Multifork.ofPiFork_ι {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {c : Fan I.left} {d : Fan I.right} (hd : IsLimit d) (a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.L) : (ofPiFork a).ι i = CategoryStruct.comp a.ι (c.proj i)

@[deprecated CategoryTheory.Limits.Multifork.ofPiFork_ι (since := "2025-12-08")]

theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_left {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {c : Fan I.left} {d : Fan I.right} (hd : IsLimit d) (a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.L) : (ofPiFork a).ι i = CategoryStruct.comp a.ι (c.proj i)

Alias of CategoryTheory.Limits.Multifork.ofPiFork_ι.

@[simp]

theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_right {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {c : Fan I.left} {d : Fan I.right} (hd : IsLimit d) (a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i : J.R) : (ofPiFork a).π.app (WalkingMulticospan.right i) = CategoryStruct.comp a.ι (CategoryStruct.comp (I.fstPiMapOfIsLimit c hd) (d.proj i))

def CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : Functor (Multifork I) (Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))

Multifork.toPiFork as a functor.

Equations

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_map_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) {K₁ K₂ : Multifork I} (f : K₁ ⟶ K₂) : ((I.toPiForkFunctor hc hd).map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) (K : Multifork I) : (I.toPiForkFunctor hc hd).obj K = Multifork.toPiFork hc hd K

def CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} {d : Fan I.right} (hd : IsLimit d) : Functor (Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (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] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} {d : Fan I.right} (hd : IsLimit d) {K₁ K₂ : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)} (f : K₁ ⟶ K₂) : ((I.ofPiForkFunctor hd).map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor_obj {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} {d : Fan I.right} (hd : IsLimit d) (a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) : (I.ofPiForkFunctor hd).obj a = Multifork.ofPiFork a

def CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : Multifork I ≌ Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)

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.multiforkEquivPiForkOfIsLimit_counitIso {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).counitIso = NatIso.ofComponents (fun (K : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) => Fork.ext (Iso.refl (((I.ofPiForkFunctor hd).comp (I.toPiForkFunctor hc hd)).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_functor {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).functor = I.toPiForkFunctor hc hd

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_inverse {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).inverse = I.ofPiForkFunctor hd

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_unitIso {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) {c : Fan I.left} (hc : IsLimit c) {d : Fan I.right} (hd : IsLimit d) : (I.multiforkEquivPiForkOfIsLimit hc hd).unitIso = NatIso.ofComponents (fun (K : Multifork I) => Cones.ext (Iso.refl ((Functor.id (Multifork I)).obj K).pt) ⋯) ⋯

noncomputable def CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J 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_obj_pt {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] (a : Fork (I.fstPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right))) (I.sndPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right)))) : (I.multiforkEquivPiFork.inverse.obj a).pt = a.pt

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_inv_app_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] (X : Fork (I.fstPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right))) (I.sndPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.inv.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_map_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] {K₁ K₂ : Fork (I.fstPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right))) (I.sndPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right)))} (f : K₁ ⟶ K₂) : (I.multiforkEquivPiFork.inverse.map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_inverse_obj_π_app {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] (a : Fork (I.fstPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right))) (I.sndPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right)))) (x✝ : WalkingMulticospan J) : (I.multiforkEquivPiFork.inverse.obj a).π.app x✝ = match x✝ with | WalkingMulticospan.left a_1 => CategoryStruct.comp a.ι (Fan.proj (limit.cone (Discrete.functor I.left)) a_1) | WalkingMulticospan.right a_1 => CategoryStruct.comp a.ι (CategoryStruct.comp (Fan.proj (limit.cone (Discrete.functor I.left)) (J.fst a_1)) (I.fst a_1))

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_pt {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] (K : Multifork I) : (I.multiforkEquivPiFork.functor.obj K).pt = K.pt

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_obj_π_app {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] (K : Multifork I) (X : WalkingParallelPair) : (I.multiforkEquivPiFork.functor.obj K).π.app X = WalkingParallelPair.rec (motive := fun (t : WalkingParallelPair) => X = t → (K.pt ⟶ (parallelPair (I.fstPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right))) (I.sndPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right)))).obj X)) (fun (h : X = WalkingParallelPair.zero) => ⋯ ▸ Fan.IsLimit.desc (limit.isLimit (Discrete.functor I.left)) K.ι) (fun (h : X = WalkingParallelPair.one) => ⋯ ▸ CategoryStruct.comp (Fan.IsLimit.desc (limit.isLimit (Discrete.functor I.left)) K.ι) (I.sndPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right)))) X ⋯

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] (X : Fork (I.fstPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right))) (I.sndPiMapOfIsLimit (limit.cone (Discrete.functor I.left)) (limit.isLimit (Discrete.functor I.right)))) : (I.multiforkEquivPiFork.counitIso.hom.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_inv_app_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] (X : Multifork I) : (I.multiforkEquivPiFork.unitIso.inv.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_unitIso_hom_app_hom {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasProduct I.left] [HasProduct I.right] (X : Multifork I) : (I.multiforkEquivPiFork.unitIso.hom.app X).hom = CategoryStruct.id X.pt

def CategoryTheory.Limits.MulticospanIndex.ofParallelHoms {C : Type u} [Category.{v, u} C] (J : MulticospanShape) {X Y : C} (f g : X ⟶ Y) : MulticospanIndex J C

The constant MulticospanShape for a pair of parallel morphisms.

Equations

• CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g = { left := fun (x : J.L) => X, right := fun (x : J.R) => Y, fst := fun (x : J.R) => f, snd := fun (x : J.R) => g }

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_right {C : Type u} [Category.{v, u} C] (J : MulticospanShape) {X Y : C} (f g : X ⟶ Y) (x✝ : J.R) : (ofParallelHoms J f g).right x✝ = Y

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_snd {C : Type u} [Category.{v, u} C] (J : MulticospanShape) {X Y : C} (f g : X ⟶ Y) (x✝ : J.R) : (ofParallelHoms J f g).snd x✝ = g

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_fst {C : Type u} [Category.{v, u} C] (J : MulticospanShape) {X Y : C} (f g : X ⟶ Y) (x✝ : J.R) : (ofParallelHoms J f g).fst x✝ = f

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_left {C : Type u} [Category.{v, u} C] (J : MulticospanShape) {X Y : C} (f g : X ⟶ Y) (x✝ : J.L) : (ofParallelHoms J f g).left x✝ = X

def CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork {C : Type u} [Category.{v, u} C] (J : MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) : Multifork (ofParallelHoms J f g) ≌ Fork f g

A fork on a pair of morphisms f and g is the same as a multifork on the single point index defined by f and g.

Equations

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

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι {C : Type u} [Category.{v, u} C] (J : MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) (c : Multifork (ofParallelHoms J f g)) : ((multiforkOfParallelHomsEquivFork J f g).functor.obj c).ι = c.ι default

@[simp]

theorem CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι {C : Type u} [Category.{v, u} C] (J : MulticospanShape) [Unique J.L] [Unique J.R] {X Y : C} (f g : X ⟶ Y) (c : Fork f g) (a : J.L) : ((multiforkOfParallelHomsEquivFork J f g).inverse.obj c).ι a = c.ι

def CategoryTheory.Limits.Multicofork.π {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) (b : J.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] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) (b : J.R) : K.ι.app (WalkingMultispan.right b) = K.π b

@[simp]

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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Multicofork.π_comp_hom_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K₁ K₂ : Multicofork I) (f : K₁ ⟶ K₂) (b : J.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] {J : MultispanShape} (I : MultispanIndex J C) (P : C) (π : (b : J.R) → I.right b ⟶ P) (w : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (π (J.fst a)) = CategoryStruct.comp (I.snd a) (π (J.snd 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π_ι_app {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) (P : C) (π : (b : J.R) → I.right b ⟶ P) (w : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (π (J.fst a)) = CategoryStruct.comp (I.snd a) (π (J.snd a))) (x : WalkingMultispan J) : (ofπ I P π w).ι.app x = match x with | WalkingMultispan.left a => CategoryStruct.comp (I.fst a) (π (J.fst a)) | WalkingMultispan.right a => π a

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Multicofork.IsColimit.mk {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) (desc : (E : Multicofork I) → K.pt ⟶ E.pt) (fac : ∀ (E : Multicofork I) (i : J.R), CategoryStruct.comp (K.π i) (desc E) = E.π i) (uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.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] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) (desc : (E : Multicofork I) → K.pt ⟶ E.pt) (fac : ∀ (E : Multicofork I) (i : J.R), CategoryStruct.comp (K.π i) (desc E) = E.π i) (uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), CategoryStruct.comp (K.π i) m = E.π i) → m = desc E) (E : Multicofork I) : (mk K desc fac uniq).desc E = desc E

theorem CategoryTheory.Limits.Multicofork.IsColimit.hom_ext {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K : Multicofork I} (hK : IsColimit K) {T : C} {f g : K.pt ⟶ T} (h : ∀ (a : J.R), CategoryStruct.comp (K.π a) f = CategoryStruct.comp (K.π a) g) : f = g

def CategoryTheory.Limits.Multicofork.IsColimit.desc {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K : Multicofork I} (hK : IsColimit K) {T : C} (k : (a : J.R) → I.right a ⟶ T) (hk : ∀ (b : J.L), CategoryStruct.comp (I.fst b) (k (J.fst b)) = CategoryStruct.comp (I.snd b) (k (J.snd b))) : K.pt ⟶ T

Constructor for morphisms from the point of a colimit multicofork.

Equations

• CategoryTheory.Limits.Multicofork.IsColimit.desc hK k hk = hK.desc (CategoryTheory.Limits.Multicofork.ofπ I T k hk)

@[simp]

theorem CategoryTheory.Limits.Multicofork.IsColimit.fac {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K : Multicofork I} (hK : IsColimit K) {T : C} (k : (a : J.R) → I.right a ⟶ T) (hk : ∀ (b : J.L), CategoryStruct.comp (I.fst b) (k (J.fst b)) = CategoryStruct.comp (I.snd b) (k (J.snd b))) (a : J.R) : CategoryStruct.comp (K.π a) (desc hK k hk) = k a

@[simp]

theorem CategoryTheory.Limits.Multicofork.IsColimit.fac_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K : Multicofork I} (hK : IsColimit K) {T : C} (k : (a : J.R) → I.right a ⟶ T) (hk : ∀ (b : J.L), CategoryStruct.comp (I.fst b) (k (J.fst b)) = CategoryStruct.comp (I.snd b) (k (J.snd b))) (a : J.R) {Z : C} (h : T ⟶ Z) : CategoryStruct.comp (K.π a) (CategoryStruct.comp (desc hK k hk) h) = CategoryStruct.comp (k a) h

@[simp]

theorem CategoryTheory.Limits.Multicofork.sigma_condition {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) : CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) (Cofan.IsColimit.desc hd K.π) = CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc) (Cofan.IsColimit.desc hd K.π)

@[simp]

theorem CategoryTheory.Limits.Multicofork.sigma_condition_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) {Z : C} (h : K.pt ⟶ Z) : CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) (CategoryStruct.comp (Cofan.IsColimit.desc hd K.π) h) = CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc) (CategoryStruct.comp (Cofan.IsColimit.desc hd K.π) h)

noncomputable def CategoryTheory.Limits.Multicofork.toSigmaCofork {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) (K : Multicofork I) : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)

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

Equations

• CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K = CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π) ⋯

@[simp]

theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_pt {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) (K : Multicofork I) : (toSigmaCofork hc hd K).pt = K.pt

@[simp]

theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_π {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) : (toSigmaCofork hc hd K).π = Cofan.IsColimit.desc hd K.π

noncomputable def CategoryTheory.Limits.Multicofork.ofSigmaCofork {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {c : Cofan I.left} {hc : IsColimit c} {d : Cofan I.right} (a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) : 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] {J : MultispanShape} {I : MultispanIndex J C} {c : Cofan I.left} {hc : IsColimit c} {d : Cofan I.right} (a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) : (ofSigmaCofork a).pt = a.pt

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_left {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (i : J.L) : (ofSigmaCofork a).ι.app (WalkingMultispan.left i) = CategoryStruct.comp (c.inj i) (CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc) a.π)

@[simp]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_π {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (i : J.R) : (ofSigmaCofork a).π i = CategoryStruct.comp (d.inj i) a.π

@[deprecated CategoryTheory.Limits.Multicofork.ofSigmaCofork_π (since := "2025-12-08")]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (i : J.R) : (ofSigmaCofork a).π i = CategoryStruct.comp (d.inj i) a.π

Alias of CategoryTheory.Limits.Multicofork.ofSigmaCofork_π.

@[deprecated CategoryTheory.Limits.Multicofork.ofSigmaCofork_π (since := "2025-12-08")]

theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right' {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (i : J.R) : (ofSigmaCofork a).π i = CategoryStruct.comp (d.inj i) a.π

Alias of CategoryTheory.Limits.Multicofork.ofSigmaCofork_π.

def CategoryTheory.Limits.Multicofork.ext {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K K' : Multicofork I} (e : K.pt ≅ K'.pt) (h : ∀ (i : J.R), CategoryStruct.comp (K.π i) e.hom = K'.π i := by cat_disch) : K ≅ K'

Constructor for isomorphisms between multicoforks.

Equations

• CategoryTheory.Limits.Multicofork.ext e h = CategoryTheory.Limits.Cocones.ext e ⋯

@[simp]

theorem CategoryTheory.Limits.Multicofork.ext_inv_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K K' : Multicofork I} (e : K.pt ≅ K'.pt) (h : ∀ (i : J.R), CategoryStruct.comp (K.π i) e.hom = K'.π i := by cat_disch) : (ext e h).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Limits.Multicofork.ext_hom_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K K' : Multicofork I} (e : K.pt ≅ K'.pt) (h : ∀ (i : J.R), CategoryStruct.comp (K.π i) e.hom = K'.π i := by cat_disch) : (ext e h).hom.hom = e.hom

def CategoryTheory.Limits.Multicofork.isoOfπ {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (t : Multicofork I) : t ≅ ofπ I t.pt t.π ⋯

Every multicofork is isomorphic to one of the form Multicofork.ofπ.

Equations

• t.isoOfπ = CategoryTheory.Limits.Multicofork.ext (CategoryTheory.Iso.refl t.pt) ⋯

@[simp]

theorem CategoryTheory.Limits.Multicofork.isoOfπ_hom_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (t : Multicofork I) : t.isoOfπ.hom.hom = CategoryStruct.id t.pt

@[simp]

theorem CategoryTheory.Limits.Multicofork.isoOfπ_inv_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (t : Multicofork I) : t.isoOfπ.inv.hom = CategoryStruct.id t.pt

noncomputable def CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) : Functor (Multicofork I) (Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))

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] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) {K₁ K₂ : Multicofork I} (f : K₁ ⟶ K₂) : ((I.toSigmaCoforkFunctor hc hd).map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor_obj {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) (K : Multicofork I) : (I.toSigmaCoforkFunctor hc hd).obj K = Multicofork.toSigmaCofork hc hd K

noncomputable def CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} : Functor (Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) (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] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (a : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) : (I.ofSigmaCoforkFunctor hc).obj a = Multicofork.ofSigmaCofork a

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_map_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} {K₁ K₂ : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)} (f : K₁ ⟶ K₂) : ((I.ofSigmaCoforkFunctor hc).map f).hom = f.hom

noncomputable def CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) : Multicofork I ≌ Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)

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.multicoforkEquivSigmaCoforkOfIsColimit_functor {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) : (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).functor = I.toSigmaCoforkFunctor hc hd

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_inverse {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) : (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).inverse = I.ofSigmaCoforkFunctor hc

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_unitIso {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) : (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).unitIso = NatIso.ofComponents (fun (K : Multicofork I) => Cocones.ext (Iso.refl ((Functor.id (Multicofork I)).obj K).pt) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCoforkOfIsColimit_counitIso {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) {c : Cofan I.left} (hc : IsColimit c) {d : Cofan I.right} (hd : IsColimit d) : (I.multicoforkEquivSigmaCoforkOfIsColimit hc hd).counitIso = NatIso.ofComponents (fun (K : Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)) => Cofork.ext (Iso.refl (((I.ofSigmaCoforkFunctor hc).comp (I.toSigmaCoforkFunctor hc hd)).obj K).pt) ⋯) ⋯

noncomputable def CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J 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_hom_app_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (X : Multicofork I) : (I.multicoforkEquivSigmaCofork.unitIso.hom.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (a : Cofork (I.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left)))) : (I.multicoforkEquivSigmaCofork.inverse.obj a).pt = a.pt

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_map_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] {K₁ K₂ : Cofork (I.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left)))} (f : K₁ ⟶ K₂) : (I.multicoforkEquivSigmaCofork.inverse.map f).hom = f.hom

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (a : Cofork (I.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left)))) (x : WalkingMultispan J) : (I.multicoforkEquivSigmaCofork.inverse.obj a).ι.app x = match x with | WalkingMultispan.left a_1 => CategoryStruct.comp (I.fst a_1) (CategoryStruct.comp (Cofan.inj (colimit.cocone (Discrete.functor I.right)) (J.fst a_1)) a.π) | WalkingMultispan.right a_1 => CategoryStruct.comp (Cofan.inj (colimit.cocone (Discrete.functor I.right)) a_1) a.π

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_hom_app_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (X : Cofork (I.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left)))) : (I.multicoforkEquivSigmaCofork.counitIso.hom.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_counitIso_inv_app_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (X : Cofork (I.fstSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left))) (I.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left)))) : (I.multicoforkEquivSigmaCofork.counitIso.inv.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_unitIso_inv_app_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (X : Multicofork I) : (I.multicoforkEquivSigmaCofork.unitIso.inv.app X).hom = CategoryStruct.id X.pt

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_pt {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (K : Multicofork I) : (I.multicoforkEquivSigmaCofork.functor.obj K).pt = K.pt

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_functor_obj_ι_app {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasCoproduct I.left] [HasCoproduct I.right] (K : Multicofork I) (X : WalkingParallelPair) : (I.multicoforkEquivSigmaCofork.functor.obj K).ι.app X = WalkingParallelPair.rec (CategoryStruct.comp (I.sndSigmaMapOfIsColimit (colimit.cocone (Discrete.functor I.right)) (colimit.isColimit (Discrete.functor I.left))) (Cofan.IsColimit.desc (colimit.isColimit (Discrete.functor I.right)) K.π)) (Cofan.IsColimit.desc (colimit.isColimit (Discrete.functor I.right)) K.π) X

@[reducible, inline]

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

For I : MulticospanIndex J 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] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] : C

The multiequalizer of I : MulticospanIndex J C.

Equations

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

@[reducible, inline]

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

For I : MultispanIndex J 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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] : C

The multicoequalizer of I : MultispanIndex J C.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.Multiequalizer.ι {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] (a : J.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] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] (a : J.L) : (multifork I).ι a = ι I a

@[simp]

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

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

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

@[reducible, inline]

abbrev CategoryTheory.Limits.Multiequalizer.lift {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] (W : C) (k : (a : J.L) → W ⟶ I.left a) (h : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd 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] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] (W : C) (k : (a : J.L) → W ⟶ I.left a) (h : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.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] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] (W : C) (k : (a : J.L) → W ⟶ I.left a) (h : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.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] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] {W : C} (i j : W ⟶ multiequalizer I) (h : ∀ (a : J.L), CategoryStruct.comp i (ι I a) = CategoryStruct.comp j (ι I a)) : i = j

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

instance CategoryTheory.Limits.Multiequalizer.instHasEqualizerFstPiMapSndPiMap {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] [HasProduct I.left] [HasProduct I.right] (a : J.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] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] [HasProduct I.left] [HasProduct I.right] (a : J.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] {J : MulticospanShape} (I : MulticospanIndex J 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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] (b : J.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] {J : MultispanShape} (I : MultispanIndex J 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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] (b : J.R) : (multicofork I).π b = π I b

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

@[simp]

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

@[simp]-normal form of multicofork_ι_app_right.

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

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

@[reducible, inline]

abbrev CategoryTheory.Limits.Multicoequalizer.desc {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b ⟶ W) (h : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryStruct.comp (I.snd a) (k (J.snd 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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b ⟶ W) (h : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryStruct.comp (I.snd a) (k (J.snd a))) (b : J.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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b ⟶ W) (h : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryStruct.comp (I.snd a) (k (J.snd a))) (b : J.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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] {W : C} (i j : multicoequalizer I ⟶ W) (h : ∀ (b : J.R), CategoryStruct.comp (π I b) i = CategoryStruct.comp (π I b) j) : i = j

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

instance CategoryTheory.Limits.Multicoequalizer.instHasCoequalizerFstSigmaMapSndSigmaMap {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J 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] {J : MultispanShape} (I : MultispanIndex J 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] {J : MultispanShape} (I : MultispanIndex J 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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] [HasCoproduct I.left] [HasCoproduct I.right] (b : J.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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] [HasCoproduct I.left] [HasCoproduct I.right] (b : J.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] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] [HasCoproduct I.left] [HasCoproduct I.right] : Epi (sigmaπ I)

def CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder (ι : Type w) [LinearOrder ι] : Functor (WalkingMultispan (MultispanShape.ofLinearOrder ι)) (WalkingMultispan (MultispanShape.prod ι))

The inclusion functor WalkingMultispan (.ofLinearOrder ι) ⥤ WalkingMultispan (.prod ι).

Equations

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

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder_obj (ι : Type w) [LinearOrder ι] (x : WalkingMultispan (MultispanShape.ofLinearOrder ι)) : (inclusionOfLinearOrder ι).obj x = match x with | left a => left ↑a | right b => right b

@[simp]

theorem CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder_map (ι : Type w) [LinearOrder ι] {x y : WalkingMultispan (MultispanShape.ofLinearOrder ι)} (f : x ⟶ y) : (inclusionOfLinearOrder ι).map f = match x, y, f with | x, .(x), Hom.id .(x) => CategoryStruct.id (match x with | left a => left ↑a | right b => right b) | .(left b), .(right ((MultispanShape.ofLinearOrder ι).fst b)), Hom.fst b => Hom.fst ↑b | .(left b), .(right ((MultispanShape.ofLinearOrder ι).snd b)), Hom.snd b => Hom.snd ↑b

structure CategoryTheory.Limits.MultispanIndex.SymmStruct {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) : Type (max v w)

Structure expressing a symmetry of I : MultispanIndex (.prod ι) C which allows to compare the corresponding multicoequalizer to the multicoequalizer of I.toLinearOrder.

• iso (i j : ι) : I.left (i, j) ≅ I.left (j, i)

  the symmetry isomorphism

• iso_hom_fst (i j : ι) : CategoryStruct.comp (self.iso i j).hom (I.fst (j, i)) = I.snd (i, j)
• iso_hom_snd (i j : ι) : CategoryStruct.comp (self.iso i j).hom (I.snd (j, i)) = I.fst (i, j)
• fst_eq_snd (i : ι) : I.fst (i, i) = I.snd (i, i)

theorem CategoryTheory.Limits.MultispanIndex.SymmStruct.iso_hom_fst_assoc {C : Type u} [Category.{v, u} C] {ι : Type w} {I : MultispanIndex (MultispanShape.prod ι) C} (self : I.SymmStruct) (i j : ι) {Z : C} (h : I.right ((MultispanShape.prod ι).fst (j, i)) ⟶ Z) : CategoryStruct.comp (self.iso i j).hom (CategoryStruct.comp (I.fst (j, i)) h) = CategoryStruct.comp (I.snd (i, j)) h

theorem CategoryTheory.Limits.MultispanIndex.SymmStruct.iso_hom_snd_assoc {C : Type u} [Category.{v, u} C] {ι : Type w} {I : MultispanIndex (MultispanShape.prod ι) C} (self : I.SymmStruct) (i j : ι) {Z : C} (h : I.right ((MultispanShape.prod ι).snd (j, i)) ⟶ Z) : CategoryStruct.comp (self.iso i j).hom (CategoryStruct.comp (I.snd (j, i)) h) = CategoryStruct.comp (I.fst (i, j)) h

def CategoryTheory.Limits.MultispanIndex.toLinearOrder {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) [LinearOrder ι] : MultispanIndex (MultispanShape.ofLinearOrder ι) C

The multispan index for MultispanShape.ofLinearOrder ι deduced from a multispan index for MultispanShape.prod ι when ι is linearly ordered.

Equations

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toLinearOrder_fst {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) [LinearOrder ι] (j : (MultispanShape.ofLinearOrder ι).L) : I.toLinearOrder.fst j = I.fst ↑j

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toLinearOrder_snd {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) [LinearOrder ι] (j : (MultispanShape.ofLinearOrder ι).L) : I.toLinearOrder.snd j = I.snd ↑j

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toLinearOrder_left {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) [LinearOrder ι] (j : (MultispanShape.ofLinearOrder ι).L) : I.toLinearOrder.left j = I.left ↑j

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toLinearOrder_right {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) [LinearOrder ι] (i : (MultispanShape.ofLinearOrder ι).R) : I.toLinearOrder.right i = I.right i

def CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) [LinearOrder ι] : (WalkingMultispan.inclusionOfLinearOrder ι).comp I.multispan ≅ I.toLinearOrder.multispan

Given a linearly ordered type ι and I : MultispanIndex (.prod ι) C, this is the isomorphism of functors between WalkingMultispan.inclusionOfLinearOrder ι ⋙ I.multispan and I.toLinearOrder.multispan.

Equations

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

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso_hom_app {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) [LinearOrder ι] (X : WalkingMultispan (MultispanShape.ofLinearOrder ι)) : I.toLinearOrderMultispanIso.hom.app X = (match X with | WalkingMultispan.left a => Iso.refl (I.left ↑a) | WalkingMultispan.right a => Iso.refl (I.right a)).hom

@[simp]

theorem CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso_inv_app {C : Type u} [Category.{v, u} C] {ι : Type w} (I : MultispanIndex (MultispanShape.prod ι) C) [LinearOrder ι] (X : WalkingMultispan (MultispanShape.ofLinearOrder ι)) : I.toLinearOrderMultispanIso.inv.app X = (match X with | WalkingMultispan.left a => Iso.refl (I.left ↑a) | WalkingMultispan.right a => Iso.refl (I.right a)).inv

def CategoryTheory.Limits.Multicofork.toLinearOrder {C : Type u} [Category.{v, u} C] {ι : Type w} [LinearOrder ι] {I : MultispanIndex (MultispanShape.prod ι) C} (c : Multicofork I) : Multicofork I.toLinearOrder

The multicofork for I.toLinearOrder deduced from a multicofork for I : MultispanIndex (.prod ι) C when ι is linearly ordered.

Equations

• c.toLinearOrder = CategoryTheory.Limits.Multicofork.ofπ I.toLinearOrder c.pt c.π ⋯

def CategoryTheory.Limits.Multicofork.ofLinearOrder {C : Type u} [Category.{v, u} C] {ι : Type w} [LinearOrder ι] {I : MultispanIndex (MultispanShape.prod ι) C} (c : Multicofork I.toLinearOrder) (h : I.SymmStruct) : Multicofork I

The multicofork for I : MultispanIndex (.prod ι) C deduced from a multicofork for I.toLinearOrder when ι is linearly ordered and I is symmetric.

Equations

• c.ofLinearOrder h = CategoryTheory.Limits.Multicofork.ofπ I c.pt c.π ⋯

def CategoryTheory.Limits.Multicofork.isColimitToLinearOrder {C : Type u} [Category.{v, u} C] {ι : Type w} [LinearOrder ι] {I : MultispanIndex (MultispanShape.prod ι) C} (c : Multicofork I) (hc : IsColimit c) (h : I.SymmStruct) : IsColimit c.toLinearOrder

If ι is a linearly ordered type, I : MultispanIndex (.prod ι) C, and c a colimit multicofork for I, then c.toLinearOrder is a colimit multicofork for I.toLinearOrder.

Equations

• c.isColimitToLinearOrder hc h = CategoryTheory.Limits.Multicofork.IsColimit.mk c.toLinearOrder (fun (s : CategoryTheory.Limits.Multicofork I.toLinearOrder) => hc.desc (s.ofLinearOrder h)) ⋯ ⋯