Real scalars for continuous linear endomorphisms over real algebras

For a topological module E over a commutative real algebra 𝕜 (for example an RCLike field), restricting the scalar action along ℝ → 𝕜 gives a real algebra structure on the continuous linear endomorphisms E →L[𝕜] E, compatible with the 𝕜-action.

Main definitions and results

• ContinuousLinearMap.realAlgebra: the Algebra ℝ (E →L[𝕜] E) structure obtained by restricting scalars along ℝ → 𝕜.
• ContinuousLinearMap.realIsScalarTower: with this structure, IsScalarTower ℝ 𝕜 (E →L[𝕜] E).

Neither declaration is registered as a global typeclass instance when this module is imported. At 𝕜 = ℝ and 𝕜 = ℂ, and whenever E carries its own real structure, Mathlib's ContinuousLinearMap.algebra already provides a real algebra structure. Enable the real algebra locally with attribute [local instance] ContinuousLinearMap.realAlgebra.

@[reducible]

def ContinuousLinearMap.realAlgebra {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [Algebra ℝ 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [ContinuousConstSMul 𝕜 E] [IsTopologicalAddGroup E] : Algebra ℝ (E →L[𝕜] E)

The real algebra structure on continuous linear endomorphisms of a topological module over a commutative real algebra 𝕜, obtained by restricting scalars along ℝ → 𝕜, so that r • T = algebraMap ℝ 𝕜 r • T.

theorem ContinuousLinearMap.realIsScalarTower {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [Algebra ℝ 𝕜] [TopologicalSpace E] [AddCommGroup E] [Module 𝕜 E] [ContinuousConstSMul 𝕜 E] [IsTopologicalAddGroup E] : IsScalarTower ℝ 𝕜 (E →L[𝕜] E)

With ContinuousLinearMap.realAlgebra, the real and 𝕜-scalar actions on continuous linear endomorphisms form a scalar tower.