English
The pushout of two epimorphisms exists.
Русский
Существует пушпоу двух эпиморфизмов.
LaTeX
$$$\forall a,b: X\to Y, X\to Z, [Epi a][Epi b] : HasColimit(span a b)$$$
Lean4
/-- The pushout of two epimorphisms exists. -/
theorem pushout_of_epi {X Y Z : C} (a : X ⟶ Y) (b : X ⟶ Z) [Epi a] [Epi b] : HasColimit (span a b) :=
let ⟨P, f, hfa, i⟩ := normalEpiOfEpi a
let ⟨Q, g, hgb, i'⟩ := normalEpiOfEpi b
let ⟨a', ha'⟩ :=
CokernelCofork.IsColimit.desc' i (cokernel.π (coprod.desc f g)) <|
calc
f ≫ cokernel.π (coprod.desc f g) = coprod.inl ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) := by
rw [coprod.inl_desc_assoc]
_ = coprod.inl ≫ (0 : P ⨿ Q ⟶ cokernel (coprod.desc f g)) := by rw [cokernel.condition]
_ = 0 := HasZeroMorphisms.comp_zero _ _
let ⟨b', hb'⟩ :=
CokernelCofork.IsColimit.desc' i' (cokernel.π (coprod.desc f g)) <|
calc
g ≫ cokernel.π (coprod.desc f g) = coprod.inr ≫ coprod.desc f g ≫ cokernel.π (coprod.desc f g) := by
rw [coprod.inr_desc_assoc]
_ = coprod.inr ≫ (0 : P ⨿ Q ⟶ cokernel (coprod.desc f g)) := by rw [cokernel.condition]
_ = 0 := HasZeroMorphisms.comp_zero _ _
HasColimit.mk
{ cocone :=
PushoutCocone.mk a' b' <| by
simp only [Cofork.π_ofπ] at ha' hb'
rw [ha', hb']
isColimit :=
PushoutCocone.IsColimit.mk _
(fun s =>
cokernel.desc (coprod.desc f g) (b ≫ PushoutCocone.inr s) <|
coprod.hom_ext
(calc
coprod.inl ≫ coprod.desc f g ≫ b ≫ PushoutCocone.inr s = f ≫ b ≫ PushoutCocone.inr s := by
rw [coprod.inl_desc_assoc]
_ = f ≫ a ≫ PushoutCocone.inl s := by rw [PushoutCocone.condition]
_ = 0 ≫ PushoutCocone.inl s := by rw [← Category.assoc, eq_whisker hfa]
_ = coprod.inl ≫ 0 := by rw [comp_zero, zero_comp])
(calc
coprod.inr ≫ coprod.desc f g ≫ b ≫ PushoutCocone.inr s = g ≫ b ≫ PushoutCocone.inr s := by
rw [coprod.inr_desc_assoc]
_ = 0 ≫ PushoutCocone.inr s := by rw [← Category.assoc, eq_whisker hgb]
_ = coprod.inr ≫ 0 := by rw [comp_zero, zero_comp]))
(fun s =>
(cancel_epi a).1 <| by
rw [CokernelCofork.π_ofπ] at ha'
have reassoced {W : C} (h : cokernel (coprod.desc f g) ⟶ W) :
a ≫ a' ≫ h = cokernel.π (coprod.desc f g) ≫ h := by rw [← Category.assoc, eq_whisker ha']
simp [reassoced, PushoutCocone.condition s])
(fun s =>
(cancel_epi b).1 <| by
rw [CokernelCofork.π_ofπ] at hb'
have reassoced' {W : C} (h : cokernel (coprod.desc f g) ⟶ W) :
b ≫ b' ≫ h = cokernel.π (coprod.desc f g) ≫ h := by rw [← Category.assoc, eq_whisker hb']
simp [reassoced'])
fun s m h₁ _ =>
(cancel_epi (cokernel.π (coprod.desc f g))).1 <|
calc
cokernel.π (coprod.desc f g) ≫ m = (a ≫ a') ≫ m :=
by
congr
exact ha'.symm
_ = a ≫ PushoutCocone.inl s := by rw [Category.assoc, h₁]
_ = b ≫ PushoutCocone.inr s := (PushoutCocone.condition s)
_ = cokernel.π (coprod.desc f g) ≫ cokernel.desc (coprod.desc f g) (b ≫ PushoutCocone.inr s) _ := by
rw [cokernel.π_desc] }
