Multicoequalizers that are pushouts

In this file, we show that a multicoequalizer for I : MultispanIndex (.ofLinearOrder ι) C is also a pushout when ι has exactly two elements.

noncomputable def CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork {C : Type u_1} [Category.{u_2, u_1} C] {J : MultispanShape} [Unique J.L] {I : MultispanIndex J C} (h : {J.fst default, J.snd default} = Set.univ) (h' : J.fst default ≠ J.snd default) (s : PushoutCocone (I.fst default) (I.snd default)) : Multicofork I

Given a multispan shape J which is essentially .ofLinearOrder ι (where ι has exactly two elements), this is the multicofork deduced from a pushout cocone.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork_π_eq_inl {C : Type u_1} [Category.{u_2, u_1} C] {J : MultispanShape} [Unique J.L] {I : MultispanIndex J C} (h : {J.fst default, J.snd default} = Set.univ) (h' : J.fst default ≠ J.snd default) (s : PushoutCocone (I.fst default) (I.snd default)) : (multicofork h h' s).π (J.fst default) = s.inl

@[simp]

theorem CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork_π_eq_inr {C : Type u_1} [Category.{u_2, u_1} C] {J : MultispanShape} [Unique J.L] {I : MultispanIndex J C} (h : {J.fst default, J.snd default} = Set.univ) (h' : J.fst default ≠ J.snd default) (s : PushoutCocone (I.fst default) (I.snd default)) : (multicofork h h' s).π (J.snd default) = s.inr

theorem CategoryTheory.Limits.Multicofork.IsColimit.isPushout {C : Type u_1} [Category.{u_4, u_1} C] {J : MultispanShape} [Unique J.L] {I : MultispanIndex J C} (c : Multicofork I) (h : {J.fst default, J.snd default} = Set.univ) (h' : J.fst default ≠ J.snd default) (hc : IsColimit c) : IsPushout (I.fst default) (I.snd default) (c.π (J.fst default)) (c.π (J.snd default))

A multicoequalizer for I : MultispanIndex J C is also a pushout when J is essentially .ofLinearOrder ι where ι contains exactly two elements.