English
The adjoint of a subspace g of E × F is defined as the subspace of F × E obtained by transporting g across the L2 inner product on E × F and then taking an orthogonal complement.
Русский
Сопряжённость подмодуля g ⊆ E × F определяется как множество в F × E, полученное переносом g через соответствие со скалярным произведением L2 на E × F и взятием ортогонального дополнения.
LaTeX
$$$g^{\\perp} := (g.{\\text{map}}\\,(\\text{LinearEquiv.skewSwap}^{-1} \\circ \\text{WithLp}^{-1}))^{\\perp}\\\\text{ transported back to }(F\\times E)$$$
Lean4
/-- The adjoint of a submodule
Note that the adjoint is taken with respect to the L^2 inner product on `E × F`, which is defined
as `WithLp 2 (E × F)`. -/
protected noncomputable def adjoint (g : Submodule 𝕜 (E × F)) : Submodule 𝕜 (F × E) :=
(g.map <| (LinearEquiv.skewSwap 𝕜 F E).symm.trans (WithLp.linearEquiv 2 𝕜 (F × E)).symm).orthogonal.map
(WithLp.linearEquiv 2 𝕜 (F × E))
