English
If T is a LinearPMap with dense domain, then the graph of its adjoint equals the adjoint of its graph.
Русский
Если T — линейное частичное отображение с плотной областью определения, то граф сопряжения T совпадает с сопряжением графа T.
LaTeX
$$$T^{\\dagger}.\\mathrm{graph} = T.\\mathrm{graph}.adjoint$$$
Lean4
theorem _root_.LinearPMap.adjoint_graph_eq_graph_adjoint (hT : Dense (T.domain : Set E)) : T†.graph = T.graph.adjoint :=
by
ext x
simp only [mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, mem_adjoint_iff, forall_exists_index,
forall_apply_eq_imp_iff]
constructor
· rintro ⟨hx, h⟩ a ha
rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]
· intro h
simp_rw [sub_eq_zero] at h
have hx : x.fst ∈ T†.domain := by
apply mem_adjoint_domain_of_exists
use x.snd
rintro ⟨a, ha⟩
rw [← inner_conj_symm, ← h a ha, inner_conj_symm]
use hx
apply hT.eq_of_inner_right
rintro ⟨a, ha⟩
rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩]
