Comparing linear and additive operator norms #
A continuous semilinear map and a bounded additive homomorphism with the same values have the same operator norm. This comparison lets completion results for bounded additive homomorphisms apply to continuous linear operators without unfolding either operator-norm definition.
theorem
ContinuousLinearMap.norm_eq_normedAddGroupHom
{𝕜 : Type u_1}
{𝕜₂ : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup F]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜₂ F]
{σ : 𝕜 →+* 𝕜₂}
[RingHomIsometric σ]
(f : E →SL[σ] F)
(g : NormedAddGroupHom E F)
(h : ∀ (x : E), f x = g x)
:
A continuous semilinear map and a bounded additive homomorphism with the same values have the same operator norm.