English
If f,g: X→Y admit a coequalizer and X⊔X has a binary coproduct, then the square with coprod.desc f g and coprod.desc (id_X)(id_X) is a pushout of coequalizer π f g and f ≫ π f g.
Русский
Если морфизмы f,g: X→Y существуют с кофакториализацией, и X⨿X имеет двоичный копрод, то квадрат с coprod.desc f g и coprod.desc (id_X)(id_X) является пушпойнтом для π f g и f ≫ π f g.
LaTeX
$$$\mathrm{IsPushout} (\mathrm{coprod.desc} f g) (\mathrm{coprod.desc}(\mathrm{id}_X)(\mathrm{id}_X)) (\mathrm{coequalizer.π} f g) (f \;≫\; \mathrm{coequalizer.π} f g).$$$
Lean4
/-- The coequalizer of `f g : X ⟶ Y` is the pushout of the diagonal map `X ⨿ X ⟶ X`
along the map `(f, g) : X ⨿ X ⟶ Y`. -/
theorem isPushout_coequalizer_coprod [HasCoequalizer f g] [HasBinaryCoproduct X X] :
IsPushout (coprod.desc f g) (coprod.desc (𝟙 _) (𝟙 _)) (coequalizer.π f g) (f ≫ coequalizer.π f g) :=
by
refine ⟨⟨by ext <;> simp [coequalizer.condition f g]⟩, ⟨PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
· refine fun s ↦ coequalizer.desc s.inl ?_
have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)
have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)
exact H₁.trans H₂.symm
· exact fun s ↦ by simp
· exact fun s ↦ by simpa using congr(coprod.inl ≫ $s.condition)
· exact fun s m hm _ ↦ by ext; simp [*]
