Documentation

Mathlib.LinearAlgebra.Matrix.Dual

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)