English
The same pushout statement as in 72434, asserting the pushout property for the specified square in the IsColimit IsPushout construction.
Русский
Та же конструкция pushout, что и в 72434, утвержающая свойство pushout для указанного квадрата в построении IsColimit.IsPushout.
LaTeX
$$$\text{IsPushout}(I.fst default)(I.snd default)(c.\pi (J.fst default))(c.\pi (J.snd default))$$$
Lean4
/-- A multicoequalizer for `I : MultispanIndex J C` is also
a pushout when `J` is essentially `.ofLinearOrder ι` where
`ι` contains exactly two elements. -/
theorem isPushout (hc : IsColimit c) :
IsPushout (I.fst default) (I.snd default) (c.π (J.fst default)) (c.π (J.snd default))
where
w := c.condition _
isColimit' :=
⟨PushoutCocone.IsColimit.mk _ (fun s ↦ hc.desc (isPushout.multicofork h h' s))
(fun s ↦ by simpa using hc.fac (isPushout.multicofork h h' s) (.right (J.fst default)))
(fun s ↦ by simpa using hc.fac (isPushout.multicofork h h' s) (.right (J.snd default)))
(fun s m h₁ h₂ ↦ by
apply Multicofork.IsColimit.hom_ext hc
intro k
have := h.symm.le (Set.mem_univ k)
simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at this
obtain rfl | rfl := this
· simpa [h₁] using (hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))).symm
· simpa [h₂] using (hc.fac (isPushout.multicofork h h' s) (.right (J.snd default))).symm)⟩
