English
The category of topological modules over a topological ring carries a canonical CategoryWithHomology structure; in particular, one can form homology theories for chain complexes in this category.
Русский
Категория топологических модулей над топологическим кольцом обладает канонической структурой CategoryWithHomology; в частности, можно строить теорию гомологий для цепных комплексóов в этой категории.
LaTeX
$$$\text{CategoryWithHomology}(\text{TopModuleCat } R).$$$
Lean4
instance : CategoryWithHomology (TopModuleCat R) := by
constructor
intro S
let D₁ : S.LeftHomologyData := ⟨_, _, _, _, _, isLimitKer _, by simp, isColimitCoker _⟩
let D₂ : S.RightHomologyData := ⟨_, _, _, _, by simp, isColimitCoker _, _, isLimitKer _⟩
let F := ShortComplex.leftRightHomologyComparison' D₁ D₂
suffices IsIso F from ⟨⟨.ofIsIsoLeftRightHomologyComparison' D₁ D₂⟩⟩
have hF : Function.Bijective F :=
by
change Function.Bijective ((forget₂ _ (ModuleCat R)).map F)
rw [← ConcreteCategory.isIso_iff_bijective, ShortComplex.map_leftRightHomologyComparison']
infer_instance
have hF' : Topology.IsEmbedding F :=
by
refine
.of_comp F.1.2 D₂.ι.1.2
?_
-- `isEmbedding_of_isOpenQuotientMap_of_isInducing` is the key lemma that shows the two
-- definitions of homology give the same topology.
refine
isEmbedding_of_isOpenQuotientMap_of_isInducing D₁.i (F ≫ D₂.ι) D₁.π D₂.p ?_ .subtypeVal
(Submodule.isOpenQuotientMap_mkQ _).isQuotientMap (Submodule.isOpenQuotientMap_mkQ _)
(Subtype.val_injective.comp hF.1) ?_
·
rw [← ContinuousLinearMap.coe_comp', ← ContinuousLinearMap.coe_comp', ← hom_comp, ← hom_comp,
ShortComplex.π_leftRightHomologyComparison'_ι]
· suffices ∀ x y, S.g y = 0 → D₂.p y = D₂.p x → S.g x = 0 by simpa [Set.subset_def, D₁, kerι_apply S.g] using this
intro x y hy e
obtain ⟨z, hz⟩ := (Submodule.Quotient.eq _).mp e
obtain rfl := eq_sub_iff_add_eq.mp hz
simpa [show S.g (S.f z) = 0 from ConcreteCategory.congr_hom S.zero z] using hy
rw [← isIso_iff_of_reflects_iso _ (forget₂ (TopModuleCat R) TopCat), TopCat.isIso_iff_isHomeomorph,
isHomeomorph_iff_isEmbedding_surjective]
exact ⟨hF', hF.2⟩
