English
The matrix of the adjoint of a linear map f with respect to ONBs v₁, v₂ is the conjugate transpose of the matrix of f with respect to the swapped bases; i.e., matrix of adjoint equals conjugate transpose of original.
Русский
Матрица сопряжённого отображения f по базисам v₁, v₂ равна сопряжённой по отношению к исходной матрице; то есть матрица adjoint f равна коньюгированной транспонированной матрице f.
LaTeX
$$$\text{toLin } v_2^{\text{toBasis}} v_1^{\text{toBasis}} A^{\top} = \operatorname{adjoint}(\text{toLin } v_1^{\text{toBasis}} v_2^{\text{toBasis}} A)$ for A a matrix$$
Lean4
/-- The linear map associated to the conjugate transpose of a matrix corresponding to two
orthonormal bases is the adjoint of the linear map associated to the matrix. -/
theorem toLin_conjTranspose (A : Matrix m n 𝕜) :
toLin v₂.toBasis v₁.toBasis Aᴴ = adjoint (toLin v₁.toBasis v₂.toBasis A) :=
by
refine eq_adjoint_iff_basis v₂.toBasis v₁.toBasis _ _ |>.mpr fun i j ↦ ?_
simp_rw [toLin_self]
simp [sum_inner, inner_smul_left, inner_sum, inner_smul_right, orthonormal_iff_ite.mp v₁.orthonormal,
orthonormal_iff_ite.mp v₂.orthonormal]
