English
Equivalence between adjoint-pair properties under a prime transform: (J, J', A, A') adjointness is equivalent to the transformed (P^T J P, P^T J' P, P A, A' P^{-1}).
Русский
Эквивалентность сопряжённости при преобразовании по основанию: сохранение свойства сопряжённости после замены на P^T J P и соответствующие преобразования матриц.
LaTeX
$$$(P^{\\top} J P) IsAdjointPair (P^{\\top} J P) A_1 A_2 \\iff J IsAdjointPair J (P A_1 P^{-1}) (P A_2 P^{-1}).$$$
Lean4
@[simp]
theorem isAdjointPair_toLinearMap₂' :
LinearMap.IsAdjointPair (Matrix.toLinearMap₂' R J) (Matrix.toLinearMap₂' R J') (Matrix.toLin' A)
(Matrix.toLin' A') ↔
Matrix.IsAdjointPair J J' A A' :=
by
rw [isAdjointPair_iff_comp_eq_compl₂]
have h : ∀ B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R, B = B' ↔ LinearMap.toMatrix₂' R B = LinearMap.toMatrix₂' R B' :=
by
intro B B'
constructor <;> intro h
· rw [h]
· exact (LinearMap.toMatrix₂' R).injective h
simp_rw [h, LinearMap.toMatrix₂'_comp, LinearMap.toMatrix₂'_compl₂, LinearMap.toMatrix'_toLin',
LinearMap.toMatrix'_toLinearMap₂']
rfl
