English
The construction moduleCatMkOfKerLERange furnishes a short complex in ModuleCat from f, g and a proof that range f ≤ ker g.
Русский
Конструкция moduleCatMkOfKerLERange строит короткий комплекс в ModuleCat из отображений f,g и доказательства, что образ f содержит подпредел ker g.
LaTeX
$$$\\text{moduleCatMkOfKerLERange}(f,g,hfg)$ is a ShortComplex in ModuleCat with $\\mathrm{range}(f) \\le \\ker(g)$$$
Lean4
/-- The explicit left homology data of a short complex of modules that is
given by a kernel and a quotient given by the `LinearMap` API. The projections to `K` and `H` are
not simp lemmas because the generic lemmas about `LeftHomologyData` are more useful here. -/
@[simps! K H i_hom π_hom]
def moduleCatLeftHomologyData : S.LeftHomologyData
where
K := ModuleCat.of R (LinearMap.ker S.g.hom)
H := ModuleCat.of R (LinearMap.ker S.g.hom ⧸ LinearMap.range S.moduleCatToCycles)
i := ModuleCat.ofHom (LinearMap.ker S.g.hom).subtype
π := ModuleCat.ofHom (LinearMap.range S.moduleCatToCycles).mkQ
wi := by aesop
hi := ModuleCat.kernelIsLimit _
wπ := by aesop
hπ := ModuleCat.cokernelIsColimit (ModuleCat.ofHom S.moduleCatToCycles)
