English
Every epimorphism in ModuleCat R is a normal epimorphism (i.e., a cokernel of its kernel).
Русский
Каждый эпиморфизм в ModuleCat R является нормальным эпиморфизмом (то есть является cokernel модуля-ядра).
LaTeX
$$$\forall f\, (\text{Epi } f)\ \Rightarrow\ (\mathrm{NormalEpi}(f))$$$
Lean4
/-- In the category of modules, every epimorphism is normal. -/
def normalEpi (hf : Epi f) : NormalEpi f where
W := of R (LinearMap.ker f.hom)
g := ofHom (LinearMap.ker f.hom).subtype
w := hom_ext <| LinearMap.comp_ker_subtype _
isColimit :=
/- The following invalid Lean code might help you understand what's going on here:
```
calc f.ker.subtype.range.quotient
≃ₗ[R] f.ker.quotient : Submodule.quotEquivOfEq _ _ (Submodule.range_subtype _)
... ≃ₗ[R] f.range : LinearMap.quotKerEquivRange f
... ≃ₗ[R] N : LinearEquiv.ofTop _ (range_eq_top_of_epi _)
```
-/
IsCokernel.cokernelIso _ _ (cokernelIsColimit _)
(LinearEquiv.toModuleIso
(Submodule.quotEquivOfEq _ _ (Submodule.range_subtype _) ≪≫ₗ LinearMap.quotKerEquivRange f.hom ≪≫ₗ
LinearEquiv.ofTop _ (range_eq_top_of_epi _))) <|
by ext; rfl
