Dual space, linear maps and matrices. #
This file contains some results on the matrix corresponding to the transpose of a linear map (in the dual space).
Tags #
matrix, linear_map, transpose, dual
@[simp]
theorem
LinearMap.toMatrix_transpose
{K : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{ι₁ : Type u_4}
{ι₂ : Type u_5}
[Field K]
[AddCommGroup V₁]
[Module K V₁]
[AddCommGroup V₂]
[Module K V₂]
[Fintype ι₁]
[Fintype ι₂]
[DecidableEq ι₁]
[DecidableEq ι₂]
{B₁ : Basis ι₁ K V₁}
{B₂ : Basis ι₂ K V₂}
(u : V₁ →ₗ[K] V₂)
:
(LinearMap.toMatrix (Basis.dualBasis B₂) (Basis.dualBasis B₁)) (Module.Dual.transpose u) = Matrix.transpose ((LinearMap.toMatrix B₁ B₂) u)
@[simp]
theorem
Matrix.toLin_transpose
{K : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{ι₁ : Type u_4}
{ι₂ : Type u_5}
[Field K]
[AddCommGroup V₁]
[Module K V₁]
[AddCommGroup V₂]
[Module K V₂]
[Fintype ι₁]
[Fintype ι₂]
[DecidableEq ι₁]
[DecidableEq ι₂]
{B₁ : Basis ι₁ K V₁}
{B₂ : Basis ι₂ K V₂}
(M : Matrix ι₁ ι₂ K)
:
(Matrix.toLin (Basis.dualBasis B₁) (Basis.dualBasis B₂)) (Matrix.transpose M) = Module.Dual.transpose ((Matrix.toLin B₂ B₁) M)