English
Adjointness of matrices is equivalent to adjointness of the corresponding linear maps under a fixed basis, via toLin₂' or toLin₂ constructions.
Русский
Сопряжённость матриц эквивалентна сопряжённости соответствующих линейных отображений через привязку к базису.
LaTeX
$$$\\text{isAdjointPair_toLinearMap₂} :\\;\\text{IsAdjointPair } J J' A A' \\iff \\text{LinearMap IsAdjointPair } (\\text{toLin } A)(\\text{toLin } A').$$$
Lean4
@[simp]
theorem isAdjointPair_toLinearMap₂ :
LinearMap.IsAdjointPair (Matrix.toLinearMap₂ b₁ b₁ J) (Matrix.toLinearMap₂ b₂ b₂ J') (Matrix.toLin b₁ b₂ A)
(Matrix.toLin b₂ b₁ A') ↔
Matrix.IsAdjointPair J J' A A' :=
by
rw [isAdjointPair_iff_comp_eq_compl₂]
have h : ∀ B B' : M₁ →ₗ[R] M₂ →ₗ[R] R, B = B' ↔ LinearMap.toMatrix₂ b₁ b₂ B = LinearMap.toMatrix₂ b₁ b₂ B' :=
by
intro B B'
constructor <;> intro h
· rw [h]
· exact (LinearMap.toMatrix₂ b₁ b₂).injective h
simp_rw [h, LinearMap.toMatrix₂_comp b₂ b₂, LinearMap.toMatrix₂_compl₂ b₁ b₁, LinearMap.toMatrix_toLin,
LinearMap.toMatrix₂_toLinearMap₂]
rfl
