English
A square is a pushout if and only if the associated binary cofan is a colimit; this characterizes pushouts in terms of a binary coproduct-like universal property.
Русский
Квадрат является pushout тогда и только тогда, когда связанный бинарный кофан является колимитом; это характеристика pushout через универсальное свойство, подобное двоичному копроизводному.
LaTeX
$$Nontrivial colimit equivalence: pushout ⇔ BinaryCofan.mk isColimit$$
Lean4
theorem is_coprod_iff_isPushout {X E Y YE : C} (c : BinaryCofan X E) (hc : IsColimit c) {f : X ⟶ Y} {iY : Y ⟶ YE}
{fE : c.pt ⟶ YE} (H : CommSq f c.inl iY fE) :
Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) ↔ IsPushout f c.inl iY fE :=
by
constructor
· rintro ⟨h⟩
refine ⟨H, ⟨Limits.PushoutCocone.isColimitAux' _ ?_⟩⟩
intro s
dsimp
refine ⟨h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl), h.fac _ ⟨WalkingPair.right⟩, ?_, ?_⟩
· apply BinaryCofan.IsColimit.hom_ext hc
· rw [← H.w_assoc]; erw [h.fac _ ⟨WalkingPair.right⟩]; exact s.condition
· rw [← Category.assoc]; exact h.fac _ ⟨WalkingPair.left⟩
· intro m e₁ e₂
apply BinaryCofan.IsColimit.hom_ext h
· dsimp
rw [Category.assoc, e₂, eq_comm]; exact h.fac _ ⟨WalkingPair.left⟩
· refine e₁.trans (Eq.symm ?_); exact h.fac _ _
· refine fun H => ⟨?_⟩
fapply Limits.BinaryCofan.isColimitMk
·
exact fun s =>
H.isColimit.desc
(PushoutCocone.mk s.inr _ <| (hc.fac (BinaryCofan.mk (f ≫ s.inr) s.inl) ⟨WalkingPair.left⟩).symm)
· intro s
rw [Category.assoc]
erw [H.isColimit.fac _ WalkingSpan.right]
erw [hc.fac]
rfl
· intro s; exact H.isColimit.fac _ WalkingSpan.left
· intro s m e₁ e₂
apply PushoutCocone.IsColimit.hom_ext H.isColimit
· symm; exact (H.isColimit.fac _ WalkingSpan.left).trans e₂.symm
· rw [H.isColimit.fac _ WalkingSpan.right]
apply BinaryCofan.IsColimit.hom_ext hc
· erw [hc.fac]
erw [← H.w_assoc]
rw [e₂]
rfl
· refine ((Category.assoc _ _ _).symm.trans e₁).trans ?_; symm; exact hc.fac _ _
