Continuous additive maps are ℝ-linear #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_smul ℝ E]
{F : Type u_2}
[add_comm_group F]
[module ℝ F]
[topological_space F]
[has_continuous_smul ℝ F]
[t2_space F]
{G : Type u_3}
[add_monoid_hom_class G E F]
(f : G)
(hf : continuous ⇑f)
(c : ℝ)
(x : E) :
A continuous additive map between two vector spaces over ℝ is ℝ-linear.
def
add_monoid_hom.to_real_linear_map
{E : Type u_1}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_smul ℝ E]
{F : Type u_2}
[add_comm_group F]
[module ℝ F]
[topological_space F]
[has_continuous_smul ℝ F]
[t2_space F]
(f : E →+ F)
(hf : continuous ⇑f) :
Reinterpret a continuous additive homomorphism between two real vector spaces as a continuous real-linear map.
Equations
- f.to_real_linear_map hf = {to_linear_map := {to_fun := ⇑f, map_add' := _, map_smul' := _}, cont := hf}
@[simp]
theorem
add_monoid_hom.coe_to_real_linear_map
{E : Type u_1}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_smul ℝ E]
{F : Type u_2}
[add_comm_group F]
[module ℝ F]
[topological_space F]
[has_continuous_smul ℝ F]
[t2_space F]
(f : E →+ F)
(hf : continuous ⇑f) :
⇑(f.to_real_linear_map hf) = ⇑f
def
add_equiv.to_real_linear_equiv
{E : Type u_1}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_smul ℝ E]
{F : Type u_2}
[add_comm_group F]
[module ℝ F]
[topological_space F]
[has_continuous_smul ℝ F]
[t2_space F]
(e : E ≃+ F)
(h₁ : continuous ⇑e)
(h₂ : continuous ⇑(e.symm)) :
Reinterpret a continuous additive equivalence between two real vector spaces as a continuous real-linear map.
Equations
- e.to_real_linear_equiv h₁ h₂ = {to_linear_equiv := {to_fun := e.to_fun, map_add' := _, map_smul' := _, inv_fun := e.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := h₁, continuous_inv_fun := h₂}
@[protected, instance]
def
real.is_scalar_tower
{E : Type u_1}
[add_comm_group E]
[module ℝ E]
[topological_space E]
[has_continuous_smul ℝ E]
[t2_space E]
{A : Type u_2}
[topological_space A]
[ring A]
[algebra ℝ A]
[module A E]
[has_continuous_smul ℝ A]
[has_continuous_smul A E] :
is_scalar_tower ℝ 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.