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 B₂.dualBasis B₁.dualBasis) (Module.Dual.transpose u) = ((LinearMap.toMatrix B₁ B₂) u).transpose
@[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 B₁.dualBasis B₂.dualBasis) M.transpose = Module.Dual.transpose ((Matrix.toLin B₂ B₁) M)