English
Restricting A to a dense submodule and taking the adjoint as a PMap agrees with the adjoint of A interpreted as a PMap on the full space.
Русский
Ограничение A до плотной подмодуля и взятие сопряженного как PMap совпадает с сопряженным оператора A, трактуемым как PMap на всей области.
LaTeX
$$A.toPMap p).adjoint = A.adjoint.toPMap ⊤$$
Lean4
/-- Restricting `A` to a dense submodule and taking the `LinearPMap.adjoint` is the same
as taking the `ContinuousLinearMap.adjoint` interpreted as a `LinearPMap`. -/
theorem toPMap_adjoint_eq_adjoint_toPMap_of_dense (hp : Dense (p : Set E)) :
(A.toPMap p).adjoint = A.adjoint.toPMap ⊤ := by
ext x y hxy
· simp only [LinearMap.toPMap_domain, Submodule.mem_top, iff_true, LinearPMap.mem_adjoint_domain_iff,
LinearMap.coe_comp, innerₛₗ_apply_coe]
exact ((innerSL 𝕜 x).comp <| A.comp <| Submodule.subtypeL _).cont
refine LinearPMap.adjoint_apply_eq hp _ fun v => ?_
simp only [adjoint_inner_left, LinearMap.toPMap_apply, coe_coe]
