English
The map r A is an epimorphism: r A is epi.
Русский
Отображение r A является эпиморфизмом.
LaTeX
$$$\\operatorname{Epi}(\\mathrm{r}\\ A)$$$
Lean4
instance epi_r {A : C} : Epi (r A) :=
by
have hlp : prod.lift (𝟙 A) (0 : A ⟶ A) ≫ Limits.prod.snd = 0 := prod.lift_snd _ _
let hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) (0 : A ⟶ A)) hlp) :=
by
refine Fork.IsLimit.mk _ (fun s => Fork.ι s ≫ Limits.prod.fst) ?_ ?_
· intro s
apply Limits.prod.hom_ext <;> simp
· intro s m h
haveI : Mono (prod.lift (𝟙 A) (0 : A ⟶ A)) := mono_of_mono_fac (prod.lift_fst _ _)
apply (cancel_mono (prod.lift (𝟙 A) (0 : A ⟶ A))).1
convert h
apply Limits.prod.hom_ext <;> simp
let hp2 : IsColimit (CokernelCofork.ofπ (Limits.prod.snd : A ⨯ A ⟶ A) hlp) := epiIsCokernelOfKernel _ hp1
apply NormalMonoCategory.epi_of_zero_cancel
intro Z z hz
have h : prod.lift (𝟙 A) (0 : A ⟶ A) ≫ cokernel.π (diag A) ≫ z = 0 := by rw [← Category.assoc, hz]
obtain ⟨t, ht⟩ := CokernelCofork.IsColimit.desc' hp2 _ h
rw [CokernelCofork.π_ofπ] at ht
have htt : t = 0 := by
rw [← Category.id_comp t]
change 𝟙 A ≫ t = 0
rw [← Limits.prod.lift_snd (𝟙 A) (𝟙 A), Category.assoc, ht, ← Category.assoc, cokernel.condition, zero_comp]
apply (cancel_epi (cokernel.π (diag A))).1
rw [← ht, htt, comp_zero, comp_zero]
