English
Under a unit P, the adjoint-pair relation is preserved by the similarity transform: J → P^T J P, A → P A P^{-1}.
Русский
При обратимой матрице P отношение сопряжённости сохраняется после подобного преобразования: J преобразуется в P^T J P, A в P A P^{-1}.
LaTeX
$$$(P^T J P) IsAdjointPair (P^T J P) A_1 A_2 \\iff J IsAdjointPair J (P A_1 P^{-1}) (P A_2 P^{-1}).$$$
Lean4
theorem isAdjointPair_equiv (P : Matrix n n R) (h : IsUnit P) :
(Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹) :=
by
have h' : IsUnit P.det := P.isUnit_iff_isUnit_det.mp h
let u := P.nonsingInvUnit h'
let v := Pᵀ.nonsingInvUnit (P.isUnit_det_transpose h')
let x := A₁ᵀ * Pᵀ * J
let y := J * P * A₂
suffices x * u = v * y ↔ v⁻¹ * x = y * u⁻¹
by
dsimp only [Matrix.IsAdjointPair]
simp only [Matrix.transpose_mul]
simp only [← mul_assoc, P.transpose_nonsing_inv]
convert this using 2
· rw [mul_assoc, mul_assoc, ← mul_assoc J]
rfl
· rw [mul_assoc, mul_assoc, ← mul_assoc _ _ J]
rfl
rw [Units.eq_mul_inv_iff_mul_eq]
conv_rhs => rw [mul_assoc]
rw [v.inv_mul_eq_iff_eq_mul]
