Forgetting the scalars of a topological representation

A continuous representation of a monoid G on a topological R-module V is in particular a continuous representation on the underlying topological abelian group, that is on V as a topological ℤ-module for the canonical action of ℤ, because every operator is additive and continuous. This file packages that observation at the three levels at which Mathlib states continuous representation theory: ContRepresentation.restrictScalarsInt on representations, ContIntertwiningMap.restrictScalarsInt on continuous intertwining maps, and the functor TopRep.restrictScalarsInt : TopRep k G ⥤ TopRep ℤ G on the category of topological representations. It then records that the two functors from which Mathlib builds continuous cohomology, the coinduction TopRep.coind₁Functor and the invariants TopRep.invariantsFunctor, commute with forgetting the scalars: the coinduced representation of the underlying additive representation is the underlying additive representation of the coinduced one, on the nose on the function space C(G, V), and the invariants of the underlying additive representation are the underlying topological abelian group of the invariants.

The reason for stopping at ℤ is explained in TauCeti.Algebra.Category.ModuleCat.Topology.RestrictScalars: only the canonical ℤ-module structure exists on every topological module without a choice.

Main definitions

• ContRepresentation.restrictScalarsInt, ContIntertwiningMap.restrictScalarsInt: a continuous representation, and a continuous intertwining map, read over ℤ.
• TopRep.restrictScalarsInt: the functor TopRep k G ⥤ TopRep ℤ G forgetting the scalars.
• TopRep.coind₁RestrictScalarsIntIso: coinduction commutes with forgetting the scalars.
• TopRep.invariantsRestrictScalarsIntIso: taking invariants commutes with forgetting the scalars.

Main results

• TopRep.coind₁ι_comp_coind₁RestrictScalarsIntIso_hom and TopRep.coind₁Functor_map_comp_coind₁RestrictScalarsIntIso_hom: the identification of the coinduced representations is compatible with the unit TopRep.coind₁ι and with the maps induced by TopRep.coind₁Functor.
• TopRep.invariantsRestrictScalarsIntIso_hom_comp_map: the identification of the invariants is compatible with the maps induced by TopRep.invariantsFunctor.

Continuous representations and intertwining maps

def ContRepresentation.restrictScalarsInt {R : Type u_1} [Ring R] {G : Type u_2} [Monoid G] {V : Type u_3} [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] (π : ContRepresentation R G V) : ContRepresentation ℤ G V

A continuous representation on a topological R-module, read as a continuous representation on the underlying topological abelian group: each operator is restricted to a continuous ℤ-linear map. Its behaviour is ContRepresentation.restrictScalarsInt_apply: the operators are the same functions as before.

Equations

• π.restrictScalarsInt = { toMonoidHom := { toFun := fun (g : G) => ContinuousLinearMap.restrictScalars ℤ (π g), map_one' := ⋯, map_mul' := ⋯ } }

@[simp]

theorem ContRepresentation.restrictScalarsInt_apply {R : Type u_1} [Ring R] {G : Type u_2} [Monoid G] {V : Type u_3} [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] (π : ContRepresentation R G V) (g : G) (v : V) : (π.restrictScalarsInt g) v = (π g) v

The operators of π.restrictScalarsInt are those of π.

def ContIntertwiningMap.restrictScalarsInt {R : Type u_1} [Ring R] {G : Type u_2} [Monoid G] {V : Type u_3} {W : Type u_4} [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f : ContIntertwiningMap π₁ π₂) : ContIntertwiningMap π₁.restrictScalarsInt π₂.restrictScalarsInt

A continuous intertwining map between representations on topological R-modules, read as a continuous intertwining map between the underlying additive representations.

Equations

• f.restrictScalarsInt = { toContinuousLinearMap := ContinuousLinearMap.restrictScalars ℤ f.toContinuousLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem ContIntertwiningMap.restrictScalarsInt_apply {R : Type u_1} [Ring R] {G : Type u_2} [Monoid G] {V : Type u_3} {W : Type u_4} [AddCommGroup V] [Module R V] [TopologicalSpace V] [IsTopologicalAddGroup V] [AddCommGroup W] [Module R W] [TopologicalSpace W] [IsTopologicalAddGroup W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f : ContIntertwiningMap π₁ π₂) (v : V) : f.restrictScalarsInt v = f v

Restricting the scalars of an intertwining map does not change its underlying function.

The functor on topological representations

def TopRep.restrictScalarsInt {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] : CategoryTheory.Functor (TopRep k G) (TopRep ℤ G)

Forgetting the scalars of a topological representation: the functor TopRep k G ⥤ TopRep ℤ G sending a representation on a topological k-module to the same representation on the underlying topological abelian group. The body is exposed because a consumer must see that the underlying type of restrictScalarsInt.obj X is that of X before it can name its elements.

Equations

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

@[simp]

theorem TopRep.restrictScalarsInt_obj_V {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] (X : TopRep k G) : ↑(restrictScalarsInt.obj X) = ↑X

The underlying type of a representation is unchanged by forgetting the scalars.

@[simp]

theorem TopRep.restrictScalarsInt_obj_ρ_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] (X : TopRep k G) (g : G) (x : ↑X) : ((restrictScalarsInt.obj X).ρ g) x = (X.ρ g) x

The operators of a representation are unchanged by forgetting the scalars.

@[simp]

theorem TopRep.restrictScalarsInt_map_hom_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] {X Y : TopRep k G} (f : X ⟶ Y) (x : ↑(restrictScalarsInt.obj X)) : (Hom.hom (restrictScalarsInt.map f)) x = (Hom.hom f) x

The underlying function of a morphism is unchanged by forgetting the scalars.

instance TopRep.instAdditiveIntRestrictScalarsInt {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] : restrictScalarsInt.Additive

instance TopRep.instDiscreteTopologyVIntObjRestrictScalarsInt {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] (X : TopRep k G) [DiscreteTopology ↑X] : DiscreteTopology ↑(restrictScalarsInt.obj X)

Forgetting the scalars preserves discreteness of the underlying type. This is TopRep.restrictScalarsInt_obj_V read as an instance: the equality holds by definition but not at reducible transparency, so instance search cannot see through the functor on its own.

noncomputable def TopRep.resRestrictScalarsIntMap {k : Type v} [Ring k] [TopologicalSpace k] {G H : Type u} [Group G] [Group H] (phi : H →* G) {X : TopRep k G} {Y : TopRep k H} (f : res phi X ⟶ Y) : res phi (restrictScalarsInt.obj X) ⟶ restrictScalarsInt.obj Y

The scalar-restricted coefficient map used when the acting group changes.

Equations

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

@[simp]

theorem TopRep.resRestrictScalarsIntMap_hom_apply {k : Type v} [Ring k] [TopologicalSpace k] {G H : Type u} [Group G] [Group H] (phi : H →* G) {X : TopRep k G} {Y : TopRep k H} (f : res phi X ⟶ Y) (x : ↑(res phi (restrictScalarsInt.obj X))) : (Hom.hom (resRestrictScalarsIntMap phi f)) x = (Hom.hom f) x

resRestrictScalarsIntMap has the same underlying function as the original coefficient map.

Compatibility with coinduction and invariants

def TopRep.coind₁RestrictScalarsIntIso {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : (restrictScalarsInt.obj X).coind₁ ≅ restrictScalarsInt.obj X.coind₁

Coinduction commutes with forgetting the scalars: both sides are the representation of G on C(G, X.V) by g • f = x ↦ ρ(g) (f (g⁻¹ x)), read over ℤ.

Equations

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

@[simp]

theorem TopRep.coind₁RestrictScalarsIntIso_hom_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (f : C(G, ↑(restrictScalarsInt.obj X))) : (Hom.hom X.coind₁RestrictScalarsIntIso.hom) f = f

coind₁RestrictScalarsIntIso is the identity on the function space C(G, X.V).

@[simp]

theorem TopRep.coind₁RestrictScalarsIntIso_inv_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (f : C(G, ↑X)) : (Hom.hom X.coind₁RestrictScalarsIntIso.inv) f = f

The inverse of coind₁RestrictScalarsIntIso is the identity on the function space C(G, X.V).

theorem TopRep.coind₁ι_comp_coind₁RestrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : CategoryTheory.CategoryStruct.comp (ofHom (restrictScalarsInt.obj X).ρ.coind₁ι) X.coind₁RestrictScalarsIntIso.hom = restrictScalarsInt.map (ofHom X.ρ.coind₁ι)

The identification of the coinduced representations is compatible with the unit TopRep.coind₁ι, the inclusion of a representation as the constant functions.

theorem TopRep.coind₁ι_comp_coind₁RestrictScalarsIntIso_hom_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) {Z : TopRep ℤ G} (h : restrictScalarsInt.obj X.coind₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (ofHom (restrictScalarsInt.obj X).ρ.coind₁ι) (CategoryTheory.CategoryStruct.comp X.coind₁RestrictScalarsIntIso.hom h) = CategoryTheory.CategoryStruct.comp (restrictScalarsInt.map (ofHom X.ρ.coind₁ι)) h

The identification of the coinduced representations is compatible with the unit TopRep.coind₁ι, the inclusion of a representation as the constant functions.

@[simp]

theorem TopRep.coind₁Functor_map_comp_coind₁RestrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep k G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((coind₁Functor ℤ G).map (restrictScalarsInt.map f)) Y.coind₁RestrictScalarsIntIso.hom = CategoryTheory.CategoryStruct.comp X.coind₁RestrictScalarsIntIso.hom (restrictScalarsInt.map ((coind₁Functor k G).map f))

The identification of the coinduced representations is compatible with the maps induced by TopRep.coind₁Functor.

@[simp]

theorem TopRep.coind₁Functor_map_comp_coind₁RestrictScalarsIntIso_hom_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep k G} (f : X ⟶ Y) {Z : TopRep ℤ G} (h : restrictScalarsInt.obj Y.coind₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (ofHom (ContRepresentation.coind₁Map (Hom.hom (restrictScalarsInt.map f)))) (CategoryTheory.CategoryStruct.comp Y.coind₁RestrictScalarsIntIso.hom h) = CategoryTheory.CategoryStruct.comp X.coind₁RestrictScalarsIntIso.hom (CategoryTheory.CategoryStruct.comp (restrictScalarsInt.map (ofHom (ContRepresentation.coind₁Map (Hom.hom f)))) h)

The identification of the coinduced representations is compatible with the maps induced by TopRep.coind₁Functor.

def TopRep.invariantsRestrictScalarsIntEquiv {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] (X : TopRep k G) : ↑(restrictScalarsInt.obj X).invariants.toModuleCat ≃L[ℤ] ↑(TopModuleCat.restrictScalarsInt.obj X.invariants).toModuleCat

Taking invariants commutes with forgetting the scalars, as topological ℤ-modules: the invariants of the underlying additive representation are the underlying topological abelian group of the invariants.

Equations

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

@[simp]

theorem TopRep.coe_invariantsRestrictScalarsIntEquiv_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] (X : TopRep k G) (x : ↑(restrictScalarsInt.obj X).invariants.toModuleCat) : ↑(X.invariantsRestrictScalarsIntEquiv x) = ↑x

invariantsRestrictScalarsIntEquiv is the identity on the underlying elements.

noncomputable def TopRep.invariantsRestrictScalarsIntIso {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] (X : TopRep k G) : (invariantsFunctor ℤ G).obj (restrictScalarsInt.obj X) ≅ TopModuleCat.restrictScalarsInt.obj ((invariantsFunctor k G).obj X)

Taking invariants commutes with forgetting the scalars, as an isomorphism in TopModuleCat ℤ.

Equations

• X.invariantsRestrictScalarsIntIso = TopModuleCat.ofIso X.invariantsRestrictScalarsIntEquiv

@[simp]

theorem TopRep.coe_invariantsRestrictScalarsIntIso_hom_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] (X : TopRep k G) (x : ↑(restrictScalarsInt.obj X).invariants.toModuleCat) : ↑((CategoryTheory.ConcreteCategory.hom X.invariantsRestrictScalarsIntIso.hom) x) = ↑x

invariantsRestrictScalarsIntIso is the identity on the underlying invariant elements.

@[simp]

theorem TopRep.coe_invariantsRestrictScalarsIntIso_inv_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] (X : TopRep k G) (x : ↑X.invariants.toModuleCat) : ↑((CategoryTheory.ConcreteCategory.hom X.invariantsRestrictScalarsIntIso.inv) x) = ↑x

The inverse of invariantsRestrictScalarsIntIso is the identity on the underlying invariant elements.

@[simp]

theorem TopRep.invariantsRestrictScalarsIntIso_hom_comp_map {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] {X Y : TopRep k G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp X.invariantsRestrictScalarsIntIso.hom (TopModuleCat.restrictScalarsInt.map ((invariantsFunctor k G).map f)) = CategoryTheory.CategoryStruct.comp ((invariantsFunctor ℤ G).map (restrictScalarsInt.map f)) Y.invariantsRestrictScalarsIntIso.hom

The identification of the invariants is compatible with the maps induced by TopRep.invariantsFunctor.

@[simp]

theorem TopRep.invariantsRestrictScalarsIntIso_hom_comp_map_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] {X Y : TopRep k G} (f : X ⟶ Y) {Z : TopModuleCat ℤ} (h : TopModuleCat.restrictScalarsInt.obj ↧↥Y.ρ.invariants ⟶ Z) : CategoryTheory.CategoryStruct.comp X.invariantsRestrictScalarsIntIso.hom (CategoryTheory.CategoryStruct.comp (TopModuleCat.restrictScalarsInt.map (TopModuleCat.ofHom (Hom.hom f).mapInvariants)) h) = CategoryTheory.CategoryStruct.comp (TopModuleCat.ofHom (Hom.hom (restrictScalarsInt.map f)).mapInvariants) (CategoryTheory.CategoryStruct.comp Y.invariantsRestrictScalarsIntIso.hom h)

The identification of the invariants is compatible with the maps induced by TopRep.invariantsFunctor.