English
In FGModuleCat over Noetherian ring k, any morphism has a coimage-image comparison that is an isomorphism.
Русский
В FGModuleCat над кольцом k, удовлетворяющим условию Нотер, любой морфизм имеет сопоставление образ-кообразие, являющееся изоморфизмом.
LaTeX
$$$\\text{instIsIsoCoimageImageComparison} : IsIso(\\mathrm{Abelian.coimageImageComparison} f)$$$
Lean4
/-- `H⁰_cont(G, X) ≅ Xᴳ`. -/
noncomputable def continuousCohomologyZeroIso : (continuousCohomology R G 0) ≅ invariants R G :=
NatIso.ofComponents
(fun X ↦
(ofIsLimitKernelFork _ (by simp) _ (TopModuleCat.isLimitKer _)).left.homologyIso ≪≫
TopModuleCat.ofIso (kerHomogeneousCochainsZeroEquiv R G X _ (by simp)))
fun {X Y} f ↦ by
dsimp [continuousCohomology, HomologicalComplex.homologyMap]
rw [Category.assoc, ← Iso.inv_comp_eq]
rw [LeftHomologyData.leftHomologyIso_inv_naturality_assoc, Iso.inv_hom_id_assoc, ←
cancel_epi (LeftHomologyData.π _), leftHomologyπ_naturality'_assoc]
rfl
