Extending an ℝ-linear functional to a 𝕜-linear functional

In this file we provide a way to extend a (optionally, continuous) ℝ-linear map to a (continuous) 𝕜-linear map in a way that bounds the norm by the norm of the original map, when 𝕜 is either ℝ (the extension is trivial) or ℂ. We formulate the extension uniformly, by assuming RCLike 𝕜.

We motivate the form of the extension as follows. Note that fc : F →ₗ[𝕜] 𝕜 is determined fully by re fc: for all x : F, fc (I • x) = I * fc x, so im (fc x) = -re (fc (I • x)). Therefore, given an fr : F →ₗ[ℝ] ℝ, we define fc x = fr x - fr (I • x) * I.

In Mathlib/Analysis/Normed/Module/RCLike/Extend.lean we show that this extension is isometric. This is separate to avoid importing material about the operator norm into files about more elementary properties, like locally convex spaces.

Main definitions

• LinearMap.extendRCLike
• ContinuousLinearMap.extendRCLike

noncomputable def Module.Dual.extendRCLike {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Dual ℝ F) : Dual 𝕜 F

Extend fr : Dual ℝ F to Dual 𝕜 F in a way that will also be continuous and have its norm (as a continuous linear map) equal to ‖fr‖ when fr is itself continuous on a normed space.

Equations

• fr.extendRCLike = { toFun := fun (x : F) => ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x)), map_add' := ⋯, map_smul' := ⋯ }

theorem Module.Dual.extendRCLike_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Dual ℝ F) (x : F) : fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

@[simp]

theorem Module.Dual.re_extendRCLike_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Dual ℝ F) (x : F) : RCLike.re (fr.extendRCLike x) = fr x

@[simp]

theorem Module.Dual.im_extendRCLike_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (g : Dual ℝ F) (x : F) : RCLike.im (g.extendRCLike x) = -g (RCLike.I • x)

theorem Module.Dual.norm_extendRCLike_apply_sq {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Dual ℝ F) (x : F) : ‖fr.extendRCLike x‖ ^ 2 = fr ((starRingEnd 𝕜) (fr.extendRCLike x) • x)

noncomputable def Module.Dual.extendRCLikeₗ {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] : Dual ℝ F ≃ₗ[ℝ] Dual 𝕜 F

The extension Module.Dual.extendRCLike as a linear equivalence between the algebraic duals.

Equations

• Module.Dual.extendRCLikeₗ = { toFun := Module.Dual.extendRCLike, map_add' := ⋯, map_smul' := ⋯, invFun := fun (f : Module.Dual 𝕜 F) => RCLike.reLm ∘ₗ ↑ℝ f, left_inv := ⋯, right_inv := ⋯ }

theorem Module.Dual.extendRCLikeₗ_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (f : Dual 𝕜 F) : extendRCLikeₗ.symm f = RCLike.reLm ∘ₗ ↑ℝ f

theorem Module.Dual.extendRCLikeₗ_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Dual ℝ F) : extendRCLikeₗ fr = fr.extendRCLike

noncomputable def StrongDual.extendRCLike {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : StrongDual 𝕜 F

Extend fr : StrongDual ℝ F to StrongDual 𝕜 F.

It would be possible to use LinearMap.mkContinuous here, but we would need to know that the continuity of fr implies it has bounded norm and we want to avoid that dependency here.

Norm properties of this extension can be found in Mathlib/Analysis/Normed/Module/RCLike/Extend.lean.

Equations

• fr.extendRCLike = { toLinearMap := Module.Dual.extendRCLike ↑fr, cont := ⋯ }

theorem StrongDual.extendRCLike_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) (x : F) : fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

@[simp]

theorem StrongDual.re_extendRCLike_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (g : StrongDual ℝ F) (x : F) : RCLike.re (g.extendRCLike x) = g x

@[deprecated StrongDual.re_extendRCLike_apply (since := "2026-02-24")]

theorem RCLike.re_extendTo𝕜ₗ {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (g : StrongDual ℝ F) (x : F) : re (g.extendRCLike x) = g x

Alias of StrongDual.re_extendRCLike_apply.

@[simp]

theorem StrongDual.im_extendRCLike_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (g : StrongDual ℝ F) (x : F) : RCLike.im (g.extendRCLike x) = -g (RCLike.I • x)

noncomputable def StrongDual.extendRCLikeₗ {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] : StrongDual ℝ F ≃ₗ[ℝ] StrongDual 𝕜 F

The extension StrongDual.extendRCLike as a linear equivalence between the algebraic duals.

When F is a normed space, this can be upgraded to an isometric linear equivalence, see StrondDual.extendRCLikeₗᵢ.

Equations

• One or more equations did not get rendered due to their size.

theorem StrongDual.extendRCLikeₗ_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (f : StrongDual 𝕜 F) : extendRCLikeₗ.symm f = ContinuousLinearMap.comp RCLike.reCLM (ContinuousLinearMap.restrictScalars ℝ f)

theorem StrongDual.extendRCLikeₗ_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : extendRCLikeₗ fr = fr.extendRCLike

@[deprecated StrongDual.extendRCLikeₗ (since := "2026-02-24")]

def RCLike.extendTo𝕜ₗ {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] : StrongDual ℝ F ≃ₗ[ℝ] StrongDual 𝕜 F

Alias of StrongDual.extendRCLikeₗ.

---

The extension StrongDual.extendRCLike as a linear equivalence between the algebraic duals.

When F is a normed space, this can be upgraded to an isometric linear equivalence, see StrondDual.extendRCLikeₗᵢ.

Equations

• @RCLike.extendTo𝕜ₗ = @StrongDual.extendRCLikeₗ

@[deprecated Module.Dual.extendRCLike (since := "2026-02-24")]

def LinearMap.extendTo𝕜' {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) : Module.Dual 𝕜 F

Alias of Module.Dual.extendRCLike.

---

Extend fr : Dual ℝ F to Dual 𝕜 F in a way that will also be continuous and have its norm (as a continuous linear map) equal to ‖fr‖ when fr is itself continuous on a normed space.

Equations

• @LinearMap.extendTo𝕜' = @Module.Dual.extendRCLike

@[deprecated Module.Dual.extendRCLike_apply (since := "2026-02-24")]

theorem LinearMap.extendTo𝕜'_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F) : fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

Alias of Module.Dual.extendRCLike_apply.

@[deprecated Module.Dual.re_extendRCLike_apply (since := "2026-02-24")]

theorem LinearMap.extendTo𝕜'_apply_re {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F) : RCLike.re (fr.extendRCLike x) = fr x

Alias of Module.Dual.re_extendRCLike_apply.

@[deprecated Module.Dual.norm_extendRCLike_apply_sq (since := "2026-02-24")]

theorem LinearMap.norm_extendTo𝕜'_apply_sq {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F) : ‖fr.extendRCLike x‖ ^ 2 = fr ((starRingEnd 𝕜) (fr.extendRCLike x) • x)

Alias of Module.Dual.norm_extendRCLike_apply_sq.

@[deprecated Module.Dual.extendRCLike (since := "2026-02-24")]

def LinearMap.extendTo𝕜 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) : Module.Dual 𝕜 F

Alias of Module.Dual.extendRCLike.

---

Extend fr : Dual ℝ F to Dual 𝕜 F in a way that will also be continuous and have its norm (as a continuous linear map) equal to ‖fr‖ when fr is itself continuous on a normed space.

Equations

• @LinearMap.extendTo𝕜 = @Module.Dual.extendRCLike

@[deprecated Module.Dual.extendRCLike_apply (since := "2026-02-24")]

theorem LinearMap.extendTo𝕜_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F) : fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

Alias of Module.Dual.extendRCLike_apply.

@[deprecated StrongDual.extendRCLike (since := "2026-02-24")]

def ContinuousLinearMap.extendTo𝕜' {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : StrongDual 𝕜 F

Alias of StrongDual.extendRCLike.

---

Extend fr : StrongDual ℝ F to StrongDual 𝕜 F.

It would be possible to use LinearMap.mkContinuous here, but we would need to know that the continuity of fr implies it has bounded norm and we want to avoid that dependency here.

Norm properties of this extension can be found in Mathlib/Analysis/Normed/Module/RCLike/Extend.lean.

Equations

• @ContinuousLinearMap.extendTo𝕜' = @StrongDual.extendRCLike

@[deprecated StrongDual.extendRCLike_apply (since := "2026-02-24")]

theorem ContinuousLinearMap.extendTo𝕜'_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) (x : F) : fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

Alias of StrongDual.extendRCLike_apply.

@[deprecated StrongDual.extendRCLike (since := "2026-02-24")]

def ContinuousLinearMap.extendTo𝕜 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : StrongDual 𝕜 F

Alias of StrongDual.extendRCLike.

---

Extend fr : StrongDual ℝ F to StrongDual 𝕜 F.

It would be possible to use LinearMap.mkContinuous here, but we would need to know that the continuity of fr implies it has bounded norm and we want to avoid that dependency here.

Norm properties of this extension can be found in Mathlib/Analysis/Normed/Module/RCLike/Extend.lean.

Equations

• @ContinuousLinearMap.extendTo𝕜 = @StrongDual.extendRCLike

@[deprecated StrongDual.extendRCLike_apply (since := "2026-02-24")]

theorem ContinuousLinearMap.extendTo𝕜_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) (x : F) : fr.extendRCLike x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

Alias of StrongDual.extendRCLike_apply.