Module docstring
{"# 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
"}
map_real_smul
theorem
{G} [FunLike G E F] [AddMonoidHomClass G E F] (f : G) (hf : Continuous f) (c : ℝ) (x : E) : f (c • x) = c • f x
Full source
/-- A continuous additive map between two vector spaces over `ℝ` is `ℝ`-linear. -/
theorem map_real_smul {G} [FunLike G E F] [AddMonoidHomClass G E F] (f : G) (hf : Continuous f)
(c : ℝ) (x : E) :
f (c • x) = c • f x :=
suffices (fun c : ℝ => f (c • x)) = fun c : ℝ => c • f x from congr_fun this c
Rat.isDenseEmbedding_coe_real.dense.equalizer (hf.comp <| continuous_id.smul continuous_const)
(continuous_id.smul continuous_const) (funext fun r => map_ratCast_smul f ℝ ℝ r x)Informal description
Let $E$ and $F$ be topological vector spaces over $\mathbb{R}$, and let $f \colon E \to F$ be a continuous additive map. Then for any real number $c \in \mathbb{R}$ and any vector $x \in E$, we have $f(c \cdot x) = c \cdot f(x)$.
AddMonoidHom.toRealLinearMap
definition
(f : E →+ F) (hf : Continuous f) : E →L[ℝ] F
Full source
/-- Reinterpret a continuous additive homomorphism between two real vector spaces
as a continuous real-linear map. -/
def toRealLinearMap (f : E →+ F) (hf : Continuous f) : E →L[ℝ] F :=
⟨{ toFun := f
map_add' := f.map_add
map_smul' := map_real_smul f hf }, hf⟩Informal description
Given a continuous additive homomorphism \( f : E \to F \) between two real vector spaces \( E \) and \( F \), the function `AddMonoidHom.toRealLinearMap` reinterprets \( f \) as a continuous real-linear map \( E \to_{\text{L}[\mathbb{R}]} F \). This map preserves addition and scalar multiplication, i.e., \( f(x + y) = f(x) + f(y) \) and \( f(c \cdot x) = c \cdot f(x) \) for all \( x, y \in E \) and \( c \in \mathbb{R} \).
AddMonoidHom.coe_toRealLinearMap
theorem
(f : E →+ F) (hf : Continuous f) : ⇑(f.toRealLinearMap hf) = f
Full source
@[simp]
theorem coe_toRealLinearMap (f : E →+ F) (hf : Continuous f) : ⇑(f.toRealLinearMap hf) = f :=
rflInformal description
For any continuous additive homomorphism $f \colon E \to F$ between real vector spaces, the underlying function of the induced continuous real-linear map $f_{\text{lin}} \colon E \to_{\text{L}[\mathbb{R}]} F$ coincides with $f$, i.e., $f_{\text{lin}} = f$ as functions.
AddEquiv.toRealLinearEquiv
definition
(e : E ≃+ F) (h₁ : Continuous e) (h₂ : Continuous e.symm) : E ≃L[ℝ] F
Full source
/-- Reinterpret a continuous additive equivalence between two real vector spaces
as a continuous real-linear map. -/
def AddEquiv.toRealLinearEquiv (e : E ≃+ F) (h₁ : Continuous e) (h₂ : Continuous e.symm) :
E ≃L[ℝ] F :=
{ e, e.toAddMonoidHom.toRealLinearMap h₁ with }Informal description
Given a continuous additive equivalence \( e : E \simeq F \) between two real topological vector spaces \( E \) and \( F \), where both \( e \) and its inverse \( e^{-1} \) are continuous, the function `AddEquiv.toRealLinearEquiv` reinterprets \( e \) as a continuous real-linear equivalence \( E \simeq_{\text{L}[\mathbb{R}]} F \). This equivalence preserves addition and scalar multiplication, i.e., \( e(x + y) = e(x) + e(y) \) and \( e(c \cdot x) = c \cdot e(x) \) for all \( x, y \in E \) and \( c \in \mathbb{R} \).
Real.isScalarTower
instance
[T2Space E] {A : Type*} [TopologicalSpace A] [Ring A] [Algebra ℝ A] [Module A E] [ContinuousSMul ℝ A]
[ContinuousSMul A E] : IsScalarTower ℝ A E
Full source
/-- 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. -/
instance (priority := 900) Real.isScalarTower [T2Space E] {A : Type*} [TopologicalSpace A] [Ring A]
[Algebra ℝ A] [Module A E] [ContinuousSMul ℝ A] [ContinuousSMul A E] : IsScalarTower ℝ A E :=
⟨fun r x y => map_real_smul ((smulAddHom A E).flip y) (continuous_id.smul continuous_const) r x⟩Informal description
For any topological $\mathbb{R}$-algebra $A$ and any topological $\mathbb{R}$-module $E$ that is also a topological $A$-module, the scalar multiplication structures of $\mathbb{R}$ and $A$ on $E$ form a scalar tower. This means that for any $r \in \mathbb{R}$, $a \in A$, and $x \in E$, we have $(r \cdot a) \cdot x = r \cdot (a \cdot x)$.