Continuous additive maps are ℝ-linear

In this file we prove that a continuous map f : E →+ F between two topological vector spaces over ℝ is ℝ-linear

theorem map_real_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [T2Space F] {G : Type u_3} [FunLike G E F] [AddMonoidHomClass G E F] (f : G) (hf : Continuous ⇑f) (c : ℝ) (x : E) : f (c • x) = c • f x

A continuous additive map between two vector spaces over ℝ is ℝ-linear.

def AddMonoidHom.toRealLinearMap {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [T2Space F] (f : E →+ F) (hf : Continuous ⇑f) : E →L[ℝ] F

Reinterpret a continuous additive homomorphism between two real vector spaces as a continuous real-linear map.

Equations

• f.toRealLinearMap hf = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, cont := hf }

@[simp]

theorem AddMonoidHom.coe_toRealLinearMap {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [T2Space F] (f : E →+ F) (hf : Continuous ⇑f) : ⇑(f.toRealLinearMap hf) = ⇑f

def AddEquiv.toRealLinearEquiv {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [T2Space F] (e : E ≃+ F) (h₁ : Continuous ⇑e) (h₂ : Continuous ⇑e.symm) : E ≃L[ℝ] F

Reinterpret a continuous additive equivalence between two real vector spaces as a continuous real-linear map.

Equations

• e.toRealLinearEquiv h₁ h₂ = { toFun := e.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[instance 900]

instance Real.isScalarTower {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousSMul ℝ E] [T2Space E] {A : Type u_3} [TopologicalSpace A] [Ring A] [Algebra ℝ A] [Module A E] [ContinuousSMul ℝ A] [ContinuousSMul A E] : IsScalarTower ℝ A E

A topological group carries at most one structure of a topological ℝ-module, so for any topological ℝ-algebra A (e.g. A = ℂ) and any topological group that is both a topological ℝ-module and a topological A-module, these structures agree.