Forgetting the scalars of a topological module

A topological module over a topological ring R is in particular a topological abelian group, that is a topological ℤ-module for the canonical action of ℤ, and a continuous R-linear map is a continuous ℤ-linear map. This file packages that observation as the functor TopModuleCat.restrictScalarsInt : TopModuleCat R ⥤ TopModuleCat ℤ and proves that it preserves homology: the kernel of a continuous linear map and the cokernel with its quotient topology do not see the scalars, so the functor preserves kernels and cokernels, hence homology.

The target ring is ℤ and not an arbitrary ring S with a ring homomorphism S →+* R: only for ℤ does every topological R-module carry a canonical S-module structure, the one every statement about topological abelian groups already uses, and restricting scalars along Int.castRingHom R would produce the structure Module.compHom, which agrees with the canonical one only propositionally. The application is continuous cohomology: Mathlib's continuousCohomology n X for X : TopRep R G is the homology of a complex of topological R-modules, and forgetting the scalars identifies it with the cohomology of the underlying topological representation over ℤ, on which the explicit low-degree descriptions are stated.

Main definitions

• TopModuleCat.restrictScalarsInt: the functor forgetting the scalars, with its instances Additive and PreservesHomology.
• TopModuleCat.restrictScalarsInt.kerEquiv, TopModuleCat.restrictScalarsInt.cokerEquiv: the kernel and the cokernel of a continuous linear map, computed after forgetting the scalars, are the kernel and the cokernel computed before.

Main results

• TopModuleCat.restrictScalarsInt.preservesHomology: forgetting the scalars preserves homology, so that CategoryTheory.ShortComplex.mapHomologyIso identifies the homology computed after forgetting the scalars with the underlying topological abelian group of the homology.

The functor

def TopModuleCat.restrictScalarsInt {R : Type u} [Ring R] [TopologicalSpace R] : CategoryTheory.Functor (TopModuleCat R) (TopModuleCat ℤ)

Forgetting the scalars of a topological R-module: the underlying topological abelian group, as a topological ℤ-module for the canonical action of ℤ, with a continuous R-linear map read as a continuous ℤ-linear map. The body is exposed because a consumer must see that the underlying type of restrictScalarsInt.obj M is that of M before it can name its elements.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopModuleCat.restrictScalarsInt_obj {R : Type u} [Ring R] [TopologicalSpace R] (M : TopModuleCat R) : restrictScalarsInt.obj M = ↧↑M.toModuleCat

The object underlying M after forgetting the scalars is M as a topological ℤ-module.

theorem TopModuleCat.restrictScalarsInt_map_hom {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : Hom.hom (restrictScalarsInt.map f) = ContinuousLinearMap.restrictScalars ℤ (Hom.hom f)

Forgetting the scalars of a morphism restricts its scalars to ℤ.

@[simp]

theorem TopModuleCat.restrictScalarsInt_map_apply {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) (x : ↑M.toModuleCat) : (CategoryTheory.ConcreteCategory.hom (restrictScalarsInt.map f)) x = (CategoryTheory.ConcreteCategory.hom f) x

Forgetting the scalars does not change the underlying function of a morphism.

instance TopModuleCat.instAdditiveIntRestrictScalarsInt {R : Type u} [Ring R] [TopologicalSpace R] : restrictScalarsInt.Additive

Kernels

def TopModuleCat.restrictScalarsInt.kerEquiv {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : ↑(ker (restrictScalarsInt.map f)).toModuleCat ≃L[ℤ] ↑(restrictScalarsInt.obj (ker f)).toModuleCat

The kernel of f, computed after forgetting the scalars, is the kernel of f computed before, as a topological ℤ-module.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopModuleCat.restrictScalarsInt.coe_kerEquiv_apply {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) (x : ↑(ker (restrictScalarsInt.map f)).toModuleCat) : ↑((kerEquiv f) x) = ↑x

kerEquiv is the identity on the underlying elements.

noncomputable def TopModuleCat.restrictScalarsInt.kerIso {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : ker (restrictScalarsInt.map f) ≅ restrictScalarsInt.obj (ker f)

The kernel of f, computed after forgetting the scalars, is the kernel of f computed before, as an isomorphism in TopModuleCat ℤ.

Equations

• TopModuleCat.restrictScalarsInt.kerIso f = TopModuleCat.ofIso (TopModuleCat.restrictScalarsInt.kerEquiv f)

@[simp]

theorem TopModuleCat.restrictScalarsInt.kerIso_hom_comp_map_kerι {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (kerIso f).hom (restrictScalarsInt.map (kerι f)) = kerι (restrictScalarsInt.map f)

kerIso is compatible with the inclusions of the kernels.

@[simp]

theorem TopModuleCat.restrictScalarsInt.kerIso_hom_comp_map_kerι_assoc {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) {Z : TopModuleCat ℤ} (h : restrictScalarsInt.obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (kerIso f).hom (CategoryTheory.CategoryStruct.comp (restrictScalarsInt.map (kerι f)) h) = CategoryTheory.CategoryStruct.comp (kerι (restrictScalarsInt.map f)) h

kerIso is compatible with the inclusions of the kernels.

instance TopModuleCat.restrictScalarsInt.preservesKernel {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) restrictScalarsInt

Cokernels

noncomputable def TopModuleCat.restrictScalarsInt.cokerEquiv {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : ↑(coker (restrictScalarsInt.map f)).toModuleCat ≃L[ℤ] ↑(restrictScalarsInt.obj (coker f)).toModuleCat

The cokernel of f, computed after forgetting the scalars, is the cokernel of f computed before, as a topological ℤ-module. Both carry the quotient topology of N.

Equations

• TopModuleCat.restrictScalarsInt.cokerEquiv f = { toLinearEquiv := Submodule.Quotient.restrictScalarsEquiv ℤ (↑(TopModuleCat.Hom.hom f)).range, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TopModuleCat.restrictScalarsInt.cokerEquiv_mk {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) (x : ↑N.toModuleCat) : (cokerEquiv f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x

cokerEquiv sends the class of x to the class of x.

noncomputable def TopModuleCat.restrictScalarsInt.cokerIso {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : coker (restrictScalarsInt.map f) ≅ restrictScalarsInt.obj (coker f)

The cokernel of f, computed after forgetting the scalars, is the cokernel of f computed before, as an isomorphism in TopModuleCat ℤ.

Equations

• TopModuleCat.restrictScalarsInt.cokerIso f = TopModuleCat.ofIso (TopModuleCat.restrictScalarsInt.cokerEquiv f)

@[simp]

theorem TopModuleCat.restrictScalarsInt.cokerπ_comp_cokerIso_hom {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (cokerπ (restrictScalarsInt.map f)) (cokerIso f).hom = restrictScalarsInt.map (cokerπ f)

cokerIso is compatible with the projections onto the cokernels.

@[simp]

theorem TopModuleCat.restrictScalarsInt.cokerπ_comp_cokerIso_hom_assoc {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) {Z : TopModuleCat ℤ} (h : restrictScalarsInt.obj (coker f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cokerπ (restrictScalarsInt.map f)) (CategoryTheory.CategoryStruct.comp (cokerIso f).hom h) = CategoryTheory.CategoryStruct.comp (restrictScalarsInt.map (cokerπ f)) h

cokerIso is compatible with the projections onto the cokernels.

instance TopModuleCat.restrictScalarsInt.preservesCokernel {R : Type u} [Ring R] [TopologicalSpace R] {M N : TopModuleCat R} (f : M ⟶ N) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) restrictScalarsInt

instance TopModuleCat.restrictScalarsInt.preservesHomology {R : Type u} [Ring R] [TopologicalSpace R] : restrictScalarsInt.PreservesHomology