English
If the coproduct Y ⨿ Z exists and the coequalizer of f ≫ ι1 and g ≫ ι2 exists, then the pushout of f and g exists. It can be realized by composing the inclusions with the coequalizer.
Русский
Если существует копродукт Y ⨿ Z и существуют коэкваленторы f ≫ ι1 и g ≫ ι2, то пушаут для f и g существует; он задаётся композициями включений с коэквалентором.
LaTeX
$$$$\exists \text{Pushout}(f,g)\,.$$$$
Lean4
/-- If the coproduct `Y ⨿ Z` and the coequalizer of `f ≫ ι₁` and `g ≫ ι₂` exist, then the
pushout of `f` and `g` exists: It is given by composing the inclusions with the coequalizer. -/
theorem hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair {C : Type u} [𝒞 : Category.{v} C] {X Y Z : C}
(f : X ⟶ Y) (g : X ⟶ Z) [HasColimit (pair Y Z)] [HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))] :
HasColimit (span f g) :=
let ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
let ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
let c := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
HasColimit.mk
{ cocone := PushoutCocone.mk (ι₁ ≫ c) (ι₂ ≫ c) <| by rw [← Category.assoc, ← Category.assoc, coequalizer.condition]
isColimit :=
PushoutCocone.IsColimit.mk _
(fun s =>
coequalizer.desc (coprod.desc (s.ι.app WalkingSpan.left) (s.ι.app WalkingSpan.right)) <|
by
rw [Category.assoc, colimit.ι_desc, Category.assoc, colimit.ι_desc]
exact PushoutCocone.condition _)
(by simp [ι₁, c]) (by simp [ι₂, c]) fun s m h₁ h₂ =>
by
ext
· simpa using h₁
· simpa using h₂ }
