English
If a cospan is the pushout cospan under the initial object, it is a binary coproduct.
Русский
Если коспон образует пушоут-κоспон над начальным объектом, то он является бинарным копроодом.
LaTeX
$$$\\forall F:\\mathrm{DiscreteWalkingPair}\\to C,\\ c:\\mathrm{Cocone}\;F,\\ X:\\,C,\\ hX:\\mathrm{IsInitial} X,\\ f,g:\\,X\\to F(\\mathrm{left/right})\\Rightarrow\\mathrm{IsColimit}\;c$$$
Lean4
/-- If a cospan is the pushout cospan under the initial object, then it is a binary coproduct. -/
def isBinaryCoproductOfIsInitialIsPushout (F : Discrete WalkingPair ⥤ C) (c : Cocone F) {X : C} (hX : IsInitial X)
(f : X ⟶ F.obj ⟨WalkingPair.left⟩) (g : X ⟶ F.obj ⟨WalkingPair.right⟩)
(hc :
IsColimit
(PushoutCocone.mk (c.ι.app ⟨WalkingPair.left⟩) (c.ι.app ⟨WalkingPair.right⟩ :) <| hX.hom_ext (f ≫ _) (g ≫ _))) :
IsColimit c
where
desc s := hc.desc (PushoutCocone.mk (s.ι.app ⟨WalkingPair.left⟩) (s.ι.app ⟨WalkingPair.right⟩) (hX.hom_ext _ _))
fac _ j := Discrete.casesOn j fun j => WalkingPair.casesOn j (hc.fac _ WalkingSpan.left) (hc.fac _ WalkingSpan.right)
uniq s m
J :=
by
let c' :=
PushoutCocone.mk (c.ι.app ⟨WalkingPair.left⟩ ≫ m) (c.ι.app ⟨WalkingPair.right⟩ ≫ m) (hX.hom_ext (f ≫ _) (g ≫ _))
dsimp; rw [← J, ← J]
apply hc.hom_ext
rintro (_ | (_ | _)) <;> simp only [PushoutCocone.mk_ι_app, Category.assoc]
on_goal 1 => congr 1
exacts [(hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.right).symm]
