Documentation

Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

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.

source
noncomputable def CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork {C : Type u_1} [Category.{v_1, 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.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork_π_eq_inl {C : Type u_1} [Category.{v_1, 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
    source
    @[simp]
    theorem CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork_π_eq_inr {C : Type u_1} [Category.{v_1, 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
    source
    theorem CategoryTheory.Limits.Multicofork.IsColimit.isPushout {C : Type u_1} [Category.{v_1, 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.