Double adjoints of submodules and densely defined operators

The double adjoint of a closed submodule is the original submodule. As a consequence, the adjoint of a closed densely defined partial linear map has dense domain.

Main results

• Submodule.le_adjoint_adjoint: double adjoints contain the original submodule.
• Submodule.adjoint_adjoint_le: reverse inclusion for closed submodules.
• Submodule.adjoint_adjoint: equality for closed submodules.
• LinearPMap.dense_adjoint_domain: a closed densely defined operator has a densely defined adjoint.

Provenance

Adapted from the Kitware DKPS formalization, originally authored in ForTauCeti (copyright (c) 2026 Kitware, Inc.; authors Jon Crall and Claude Opus 5; Apache-2.0).

theorem Submodule.le_adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (g : Submodule 𝕜 (E × F)) : g ≤ g.adjoint.adjoint

Every submodule is contained in its double adjoint, without closedness or completeness assumptions.

theorem Submodule.adjoint_adjoint_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (g : Submodule 𝕜 (E × F)) (hg : IsClosed ↑g) : g.adjoint.adjoint ≤ g

The double adjoint of a closed submodule is contained in the submodule when the ambient inner product spaces are complete.

theorem Submodule.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (g : Submodule 𝕜 (E × F)) (hg : IsClosed ↑g) : g.adjoint.adjoint = g

Involutivity of the submodule adjoint on closed submodules.

This is the graph-level statement that makes the unbounded-operator adjoint theory close on itself: with LinearPMap.adjoint_graph_eq_graph_adjoint it says Γ(T††) = Γ(T) for closed densely defined T.

theorem LinearPMap.dense_adjoint_domain {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain) (hTc : T.IsClosed) : Dense ↑T.adjoint.domain

von Neumann's theorem. The adjoint of a closed densely defined partial linear map between complete inner product spaces has dense domain.