The dual of a submodule

Restricting continuous linear functionals from E to a submodule S is precomposition with the inclusion S.subtypeL. Its kernel is the annihilator of S, and by the Hahn–Banach theorem it is surjective. Moreover, the quotient norm of a functional modulo the annihilator equals the norm of its restriction, since a norm-preserving extension of the restriction is a representative of the same class. Hence restriction descends to an isometric identification of the quotient of the continuous dual of E by the annihilator of S with the continuous dual of S. This is the counterpart of the identification of the dual of E ⧸ S with the annihilator of S.

The annihilator is Mathlib's Submodule.orthogonalBilin for topDualPairing. No completeness or closedness assumption is needed, and E may be seminormed. The kernel computation holds over any nontrivially normed field; surjectivity and the isometry use the Hahn–Banach theorem exists_extension_norm_eq, so they are stated over fields satisfying IsRCLikeNormedField. Over such fields, a vector outside a closed submodule is also separated from it by a continuous linear functional vanishing on the submodule.

This is the standard subspace-duality theorem; see Megginson, An Introduction to Banach Space Theory, §2.6. It is the continuous analogue of Mathlib's algebraic Subspace.quotAnnihilatorEquiv.

theorem Submodule.ker_precomp_subtypeL {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (S : Submodule 𝕜 E) : (↑(ContinuousLinearMap.precomp 𝕜 S.subtypeL)).ker = orthogonalBilin (topDualPairing 𝕜 E).flip S

Restriction to a submodule kills exactly the annihilator of that submodule.

theorem Submodule.surjective_precomp_subtypeL {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [IsRCLikeNormedField 𝕜] (S : Submodule 𝕜 E) : Function.Surjective ⇑(ContinuousLinearMap.precomp 𝕜 S.subtypeL)

Every continuous linear functional on a submodule is the restriction of a continuous linear functional on the whole space.

theorem Submodule.exists_dual_forall_mem_eq_zero_ne_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [IsRCLikeNormedField 𝕜] {S : Submodule 𝕜 E} (hS : IsClosed ↑S) {x : E} (hx : x ∉ S) : ∃ (f : StrongDual 𝕜 E), (∀ y ∈ S, f y = 0) ∧ f x ≠ 0

A vector outside a closed submodule is detected by a continuous linear functional vanishing on the submodule.

noncomputable def Submodule.quotientAnnihilatorEquivDual {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [IsRCLikeNormedField 𝕜] (S : Submodule 𝕜 E) : StrongDual 𝕜 E ⧸ orthogonalBilin (topDualPairing 𝕜 E).flip S ≃ₗᵢ[𝕜] StrongDual 𝕜 ↥S

The continuous dual of a submodule is isometrically the quotient of the continuous dual of the whole space by the annihilator of the submodule. The map sends the class of a functional to its restriction.

@[simp]

theorem Submodule.quotientAnnihilatorEquivDual_mk {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [IsRCLikeNormedField 𝕜] (S : Submodule 𝕜 E) (f : StrongDual 𝕜 E) : S.quotientAnnihilatorEquivDual (Quotient.mk f) = f ∘SL S.subtypeL

The identification of the dual of a submodule restricts a representative functional.

@[simp]

theorem Submodule.quotientAnnihilatorEquivDual_symm_comp_subtypeL {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [IsRCLikeNormedField 𝕜] (S : Submodule 𝕜 E) (f : StrongDual 𝕜 E) : S.quotientAnnihilatorEquivDual.symm (f ∘SL S.subtypeL) = Quotient.mk f

The inverse identification sends the restriction of a functional to its class.

theorem Submodule.quotientAnnihilatorEquivDual_naturality {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [IsRCLikeNormedField 𝕜] (S : Submodule 𝕜 E) (R : Submodule 𝕜 F) (T : E →L[𝕜] F) (Ts : ↥S →L[𝕜] ↥R) (h : R.subtypeL ∘SL Ts = T ∘SL S.subtypeL) (f : StrongDual 𝕜 F) : R.quotientAnnihilatorEquivDual (Quotient.mk f) ∘SL Ts = S.quotientAnnihilatorEquivDual (Quotient.mk (f ∘SL T))

The identification of the dual of a submodule is natural under a commuting square of continuous linear maps. The square condition says that Ts is the restriction of T to maps from S to R; on representatives, the induced map of quotients is precomposition with T.