Dual space, linear maps and matrices.

This file contains some results about matrices and dual spaces.

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

def dotProductEquiv (R : Type u_1) (n : Type u_2) [CommSemiring R] [Fintype n] [DecidableEq n] : (n → R) ≃ₗ[R] Module.Dual R (n → R)

The dot product as a linear equivalence to the dual.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem dotProductEquiv_apply_apply (R : Type u_1) (n : Type u_2) [CommSemiring R] [Fintype n] [DecidableEq n] (v w : n → R) : ((dotProductEquiv R n) v) w = v ⬝ᵥ w

@[simp]

theorem dotProductEquiv_symm_apply (R : Type u_1) (n : Type u_2) [CommSemiring R] [Fintype n] [DecidableEq n] (f : Module.Dual R (n → R)) (i : n) : (dotProductEquiv R n).symm f i = f ((LinearMap.single R (fun (a : n) => R) i) 1)