English
Every monomorphism in ModuleCat R is a normal monomorphism (i.e., a kernel of some morphism).
Русский
Каждый мономорфизм в ModuleCat R является нормальным мономорфизмом (то есть является ядром некоторого гомоморфизма).
LaTeX
$$$\forall f\, (\text{Mono } f)\ \Rightarrow\ (\mathrm{NormalMono}(f))$$$
Lean4
/-- In the category of modules, every monomorphism is normal. -/
def normalMono (hf : Mono f) : NormalMono f
where
Z := of R (N ⧸ LinearMap.range f.hom)
g := ofHom (LinearMap.range f.hom).mkQ
w := hom_ext <| LinearMap.range_mkQ_comp _
isLimit :=
/- The following [invalid Lean code](https://github.com/leanprover-community/lean/issues/341)
might help you understand what's going on here:
```
calc
M ≃ₗ[R] f.ker.quotient : (Submodule.quotEquivOfEqBot _ (ker_eq_bot_of_mono _)).symm
... ≃ₗ[R] f.range : LinearMap.quotKerEquivRange f
... ≃ₗ[R] r.range.mkQ.ker : LinearEquiv.ofEq _ _ (Submodule.ker_mkQ _).symm
```
-/
IsKernel.isoKernel _ _ (kernelIsLimit _)
(LinearEquiv.toModuleIso
((Submodule.quotEquivOfEqBot _ (ker_eq_bot_of_mono _)).symm ≪≫ₗ
(LinearMap.quotKerEquivRange f.hom ≪≫ₗ LinearEquiv.ofEq _ _ (Submodule.ker_mkQ _).symm))) <|
by ext; rfl
