Linear maps and matrices

This file defines the maps to send matrices to a linear map, and to send linear maps between modules with a finite bases to matrices. This defines a linear equivalence between linear maps between finite-dimensional vector spaces and matrices indexed by the respective bases.

Main definitions

In the list below, and in all this file, R is a commutative ring (semiring is sometimes enough), M and its variations are R-modules, ι, κ, n and m are finite types used for indexing.

• LinearMap.toMatrix: given bases v₁ : ι → M₁ and v₂ : κ → M₂, the R-linear equivalence from M₁ →ₗ[R] M₂ to Matrix κ ι R
• Matrix.toLin: the inverse of LinearMap.toMatrix
• LinearMap.toMatrix': the R-linear equivalence from (m → R) →ₗ[R] (n → R) to Matrix m n R (with the standard basis on m → R and n → R)
• Matrix.toLin': the inverse of LinearMap.toMatrix'
• algEquivMatrix: given a basis indexed by n, the R-algebra equivalence between R-endomorphisms of M and Matrix n n R

Issues

This file was originally written without attention to non-commutative rings, and so mostly only works in the commutative setting. This should be fixed.

In particular, Matrix.mulVec gives us a linear equivalence Matrix m n R ≃ₗ[R] (n → R) →ₗ[Rᵐᵒᵖ] (m → R) while Matrix.vecMul gives us a linear equivalence Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] (n → R). At present, the first equivalence is developed in detail but only for commutative rings (and we omit the distinction between Rᵐᵒᵖ and R), while the second equivalence is developed only in brief, but for not-necessarily-commutative rings.

Naming is slightly inconsistent between the two developments. In the original (commutative) development linear is abbreviated to lin, although this is not consistent with the rest of mathlib. In the new (non-commutative) development linear is not abbreviated, and declarations use _right to indicate they use the right action of matrices on vectors (via Matrix.vecMul). When the two developments are made uniform, the names should be made uniform, too, by choosing between linear and lin consistently, and (presumably) adding _left where necessary.

Tags

linear_map, matrix, linear_equiv, diagonal, det, trace

def Matrix.vecMulLinear {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) : (m → R) →ₗ[R] n → R

Matrix.vecMul M is a linear map.

Equations

• M.vecMulLinear = { toFun := fun (x : m → R) => Matrix.vecMul x M, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matrix.vecMulLinear_apply {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) (x : m → R) : M.vecMulLinear x = Matrix.vecMul x M

theorem Matrix.coe_vecMulLinear {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) : ⇑M.vecMulLinear = fun (v : m → R) => Matrix.vecMul v M

@[simp]

theorem Matrix.vecMul_stdBasis {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] (M : Matrix m n R) (i : m) (j : n) : Matrix.vecMul ((LinearMap.stdBasis R (fun (x : m) => R) i) 1) M j = M i j

theorem range_vecMulLinear {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] (M : Matrix m n R) : LinearMap.range M.vecMulLinear = Submodule.span R (Set.range M)

theorem Matrix.vecMul_injective_iff {m : Type u_3} {n : Type u_4} [Fintype m] {R : Type u_5} [CommRing R] {M : Matrix m n R} : (Function.Injective fun (v : m → R) => Matrix.vecMul v M) ↔ LinearIndependent R fun (i : m) => M i

def LinearMap.toMatrixRight' {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] : ((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ] Matrix m n R

Linear maps (m → R) →ₗ[R] (n → R) are linearly equivalent over Rᵐᵒᵖ to Matrix m n R, by having matrices act by right multiplication.

Equations

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

@[reducible, inline]

abbrev Matrix.toLinearMapRight' {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] : Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] n → R

A Matrix m n R is linearly equivalent over Rᵐᵒᵖ to a linear map (m → R) →ₗ[R] (n → R), by having matrices act by right multiplication.

Equations

• Matrix.toLinearMapRight' = LinearMap.toMatrixRight'.symm

@[simp]

theorem Matrix.toLinearMapRight'_apply {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] (M : Matrix m n R) (v : m → R) : (Matrix.toLinearMapRight' M) v = Matrix.vecMul v M

@[simp]

theorem Matrix.toLinearMapRight'_mul {R : Type u_1} [Semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype l] [DecidableEq l] (M : Matrix l m R) (N : Matrix m n R) : Matrix.toLinearMapRight' (M * N) = Matrix.toLinearMapRight' N ∘ₗ Matrix.toLinearMapRight' M

theorem Matrix.toLinearMapRight'_mul_apply {R : Type u_1} [Semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype l] [DecidableEq l] (M : Matrix l m R) (N : Matrix m n R) (x : l → R) : (Matrix.toLinearMapRight' (M * N)) x = (Matrix.toLinearMapRight' N) ((Matrix.toLinearMapRight' M) x)

@[simp]

theorem Matrix.toLinearMapRight'_one {R : Type u_1} [Semiring R] {m : Type u_3} [Fintype m] [DecidableEq m] : Matrix.toLinearMapRight' 1 = LinearMap.id

@[simp]

theorem Matrix.toLinearEquivRight'OfInv_apply {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : n → R) : ∀ (a_1 : m), (Matrix.toLinearEquivRight'OfInv hMM' hM'M) a a_1 = (Matrix.toLinearMapRight' M') a a_1

@[simp]

theorem Matrix.toLinearEquivRight'OfInv_symm_apply {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : m → R) : ∀ (a_1 : n), (Matrix.toLinearEquivRight'OfInv hMM' hM'M).symm a a_1 = (Matrix.toLinearMapRight' M) a a_1

def Matrix.toLinearEquivRight'OfInv {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : (n → R) ≃ₗ[R] m → R

If M and M' are each other's inverse matrices, they provide an equivalence between n → A and m → A corresponding to M.vecMul and M'.vecMul.

Equations

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

From this point on, we only work with commutative rings, and fail to distinguish between Rᵐᵒᵖ and R. This should eventually be remedied.

def Matrix.mulVecLin {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) : (n → R) →ₗ[R] m → R

Matrix.mulVec M is a linear map.

Equations

• M.mulVecLin = { toFun := M.mulVec, map_add' := ⋯, map_smul' := ⋯ }

theorem Matrix.coe_mulVecLin {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) : ⇑M.mulVecLin = M.mulVec

@[simp]

theorem Matrix.mulVecLin_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) (v : n → R) : M.mulVecLin v = M.mulVec v

@[simp]

theorem Matrix.mulVecLin_zero {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] : Matrix.mulVecLin 0 = 0

@[simp]

theorem Matrix.mulVecLin_add {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) (N : Matrix m n R) : (M + N).mulVecLin = M.mulVecLin + N.mulVecLin

@[simp]

theorem Matrix.mulVecLin_transpose {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype m] (M : Matrix m n R) : M.transpose.mulVecLin = M.vecMulLinear

@[simp]

theorem Matrix.vecMulLinear_transpose {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) : M.transpose.vecMulLinear = M.mulVecLin

theorem Matrix.mulVecLin_submatrix {R : Type u_1} [CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype n] [Fintype l] (f₁ : m → k) (e₂ : n ≃ l) (M : Matrix k l R) : (M.submatrix f₁ ⇑e₂).mulVecLin = LinearMap.funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ LinearMap.funLeft R R ⇑e₂.symm

theorem Matrix.mulVecLin_reindex {R : Type u_1} [CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype n] [Fintype l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R) : ((Matrix.reindex e₁ e₂) M).mulVecLin = ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ M.mulVecLin ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)

A variant of Matrix.mulVecLin_submatrix that keeps around LinearEquivs.

@[simp]

theorem Matrix.mulVecLin_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [Fintype n] [DecidableEq n] : Matrix.mulVecLin 1 = LinearMap.id

@[simp]

theorem Matrix.mulVecLin_mul {R : Type u_1} [CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [Fintype n] [Fintype m] (M : Matrix l m R) (N : Matrix m n R) : (M * N).mulVecLin = M.mulVecLin ∘ₗ N.mulVecLin

theorem Matrix.ker_mulVecLin_eq_bot_iff {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] {M : Matrix m n R} : LinearMap.ker M.mulVecLin = ⊥ ↔ ∀ (v : n → R), M.mulVec v = 0 → v = 0

theorem Matrix.mulVec_stdBasis {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix m n R) (i : m) (j : n) : M.mulVec ((LinearMap.stdBasis R (fun (x : n) => R) j) 1) i = M i j

@[simp]

theorem Matrix.mulVec_stdBasis_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] [DecidableEq n] (M : Matrix m n R) (j : n) : M.mulVec ((LinearMap.stdBasis R (fun (x : n) => R) j) 1) = M.transpose j

theorem Matrix.range_mulVecLin {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M : Matrix m n R) : LinearMap.range M.mulVecLin = Submodule.span R (Set.range M.transpose)

theorem Matrix.mulVec_injective_iff {m : Type u_4} {n : Type u_5} [Fintype n] {R : Type u_6} [CommRing R] {M : Matrix m n R} : Function.Injective M.mulVec ↔ LinearIndependent R fun (i : n) => M.transpose i

def LinearMap.toMatrix' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] : ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R

Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to Matrix m n R.

Equations

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

def Matrix.toLin' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] : Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R

A Matrix m n R is linearly equivalent to a linear map (n → R) →ₗ[R] (m → R).

Note that the forward-direction does not require DecidableEq and is Matrix.vecMulLin.

Equations

• Matrix.toLin' = LinearMap.toMatrix'.symm

theorem Matrix.toLin'_apply' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) : Matrix.toLin' M = M.mulVecLin

@[simp]

theorem LinearMap.toMatrix'_symm {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] : LinearMap.toMatrix'.symm = Matrix.toLin'

@[simp]

theorem Matrix.toLin'_symm {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] : Matrix.toLin'.symm = LinearMap.toMatrix'

@[simp]

theorem LinearMap.toMatrix'_toLin' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) : LinearMap.toMatrix' (Matrix.toLin' M) = M

@[simp]

theorem Matrix.toLin'_toMatrix' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (f : (n → R) →ₗ[R] m → R) : Matrix.toLin' (LinearMap.toMatrix' f) = f

@[simp]

theorem LinearMap.toMatrix'_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (f : (n → R) →ₗ[R] m → R) (i : m) (j : n) : LinearMap.toMatrix' f i j = f (fun (j' : n) => if j' = j then 1 else 0) i

@[simp]

theorem Matrix.toLin'_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) (v : n → R) : (Matrix.toLin' M) v = M.mulVec v

@[simp]

theorem Matrix.toLin'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : Matrix.toLin' 1 = LinearMap.id

@[simp]

theorem LinearMap.toMatrix'_id {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : LinearMap.toMatrix' LinearMap.id = 1

@[simp]

theorem LinearMap.toMatrix'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : LinearMap.toMatrix' 1 = 1

@[simp]

theorem Matrix.toLin'_mul {R : Type u_1} [CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) : Matrix.toLin' (M * N) = Matrix.toLin' M ∘ₗ Matrix.toLin' N

@[simp]

theorem Matrix.toLin'_submatrix {R : Type u_1} [CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype l] [DecidableEq l] (f₁ : m → k) (e₂ : n ≃ l) (M : Matrix k l R) : Matrix.toLin' (M.submatrix f₁ ⇑e₂) = LinearMap.funLeft R R f₁ ∘ₗ Matrix.toLin' M ∘ₗ LinearMap.funLeft R R ⇑e₂.symm

theorem Matrix.toLin'_reindex {R : Type u_1} [CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype l] [DecidableEq l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R) : Matrix.toLin' ((Matrix.reindex e₁ e₂) M) = ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ Matrix.toLin' M ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)

A variant of Matrix.toLin'_submatrix that keeps around LinearEquivs.

theorem Matrix.toLin'_mul_apply {R : Type u_1} [CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) (x : n → R) : (Matrix.toLin' (M * N)) x = (Matrix.toLin' M) ((Matrix.toLin' N) x)

Shortcut lemma for Matrix.toLin'_mul and LinearMap.comp_apply

theorem LinearMap.toMatrix'_comp {R : Type u_1} [CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype l] [DecidableEq l] (f : (n → R) →ₗ[R] m → R) (g : (l → R) →ₗ[R] n → R) : LinearMap.toMatrix' (f ∘ₗ g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g

theorem LinearMap.toMatrix'_mul {R : Type u_1} [CommSemiring R] {m : Type u_4} [Fintype m] [DecidableEq m] (f : (m → R) →ₗ[R] m → R) (g : (m → R) →ₗ[R] m → R) : LinearMap.toMatrix' (f * g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g

@[simp]

theorem LinearMap.toMatrix'_algebraMap {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (x : R) : LinearMap.toMatrix' ((algebraMap R (Module.End R (n → R))) x) = (Matrix.scalar n) x

theorem Matrix.ker_toLin'_eq_bot_iff {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] {M : Matrix n n R} : LinearMap.ker (Matrix.toLin' M) = ⊥ ↔ ∀ (v : n → R), M.mulVec v = 0 → v = 0

theorem Matrix.range_toLin' {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix m n R) : LinearMap.range (Matrix.toLin' M) = Submodule.span R (Set.range M.transpose)

@[simp]

theorem Matrix.toLin'OfInv_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : m → R) : ∀ (a_1 : n), (Matrix.toLin'OfInv hMM' hM'M) a a_1 = (Matrix.toLin' M') a a_1

@[simp]

theorem Matrix.toLin'OfInv_symm_apply {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : n → R) : ∀ (a_1 : m), (Matrix.toLin'OfInv hMM' hM'M).symm a a_1 = (Matrix.toLin' M) a a_1

def Matrix.toLin'OfInv {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] [Fintype m] [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : (m → R) ≃ₗ[R] n → R

If M and M' are each other's inverse matrices, they provide an equivalence between m → A and n → A corresponding to M.mulVec and M'.mulVec.

Equations

• Matrix.toLin'OfInv hMM' hM'M = let __src := Matrix.toLin' M'; { toFun := ⇑(Matrix.toLin' M'), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(Matrix.toLin' M), left_inv := ⋯, right_inv := ⋯ }

def LinearMap.toMatrixAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : ((n → R) →ₗ[R] n → R) ≃ₐ[R] Matrix n n R

Linear maps (n → R) →ₗ[R] (n → R) are algebra equivalent to Matrix n n R.

Equations

• LinearMap.toMatrixAlgEquiv' = AlgEquiv.ofLinearEquiv LinearMap.toMatrix' ⋯ ⋯

def Matrix.toLinAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : Matrix n n R ≃ₐ[R] (n → R) →ₗ[R] n → R

A Matrix n n R is algebra equivalent to a linear map (n → R) →ₗ[R] (n → R).

Equations

• Matrix.toLinAlgEquiv' = LinearMap.toMatrixAlgEquiv'.symm

@[simp]

theorem LinearMap.toMatrixAlgEquiv'_symm {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : LinearMap.toMatrixAlgEquiv'.symm = Matrix.toLinAlgEquiv'

@[simp]

theorem Matrix.toLinAlgEquiv'_symm {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : Matrix.toLinAlgEquiv'.symm = LinearMap.toMatrixAlgEquiv'

@[simp]

theorem LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix n n R) : LinearMap.toMatrixAlgEquiv' (Matrix.toLinAlgEquiv' M) = M

@[simp]

theorem Matrix.toLinAlgEquiv'_toMatrixAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f : (n → R) →ₗ[R] n → R) : Matrix.toLinAlgEquiv' (LinearMap.toMatrixAlgEquiv' f) = f

@[simp]

theorem LinearMap.toMatrixAlgEquiv'_apply {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f : (n → R) →ₗ[R] n → R) (i : n) (j : n) : LinearMap.toMatrixAlgEquiv' f i j = f (fun (j' : n) => if j' = j then 1 else 0) i

@[simp]

theorem Matrix.toLinAlgEquiv'_apply {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix n n R) (v : n → R) : (Matrix.toLinAlgEquiv' M) v = M.mulVec v

theorem Matrix.toLinAlgEquiv'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : Matrix.toLinAlgEquiv' 1 = LinearMap.id

@[simp]

theorem LinearMap.toMatrixAlgEquiv'_id {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] : LinearMap.toMatrixAlgEquiv' LinearMap.id = 1

theorem LinearMap.toMatrixAlgEquiv'_comp {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f : (n → R) →ₗ[R] n → R) (g : (n → R) →ₗ[R] n → R) : LinearMap.toMatrixAlgEquiv' (f ∘ₗ g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g

theorem LinearMap.toMatrixAlgEquiv'_mul {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f : (n → R) →ₗ[R] n → R) (g : (n → R) →ₗ[R] n → R) : LinearMap.toMatrixAlgEquiv' (f * g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g

def LinearMap.toMatrix {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) : (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R

Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases.

Equations

• LinearMap.toMatrix v₁ v₂ = (v₁.equivFun.arrowCongr v₂.equivFun).trans LinearMap.toMatrix'

theorem LinearMap.toMatrix_eq_toMatrix' {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] : LinearMap.toMatrix (Pi.basisFun R n) (Pi.basisFun R n) = LinearMap.toMatrix'

LinearMap.toMatrix' is a particular case of LinearMap.toMatrix, for the standard basis Pi.basisFun R n.

def Matrix.toLin {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) : Matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂

Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence between matrices over R indexed by the bases and linear maps M₁ →ₗ M₂.

Equations

• Matrix.toLin v₁ v₂ = (LinearMap.toMatrix v₁ v₂).symm

theorem Matrix.toLin_eq_toLin' {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] : Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin'

Matrix.toLin' is a particular case of Matrix.toLin, for the standard basis Pi.basisFun R n.

@[simp]

theorem LinearMap.toMatrix_symm {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) : (LinearMap.toMatrix v₁ v₂).symm = Matrix.toLin v₁ v₂

@[simp]

theorem Matrix.toLin_symm {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) : (Matrix.toLin v₁ v₂).symm = LinearMap.toMatrix v₁ v₂

@[simp]

theorem Matrix.toLin_toMatrix {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) : (Matrix.toLin v₁ v₂) ((LinearMap.toMatrix v₁ v₂) f) = f

@[simp]

theorem LinearMap.toMatrix_toLin {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (M : Matrix m n R) : (LinearMap.toMatrix v₁ v₂) ((Matrix.toLin v₁ v₂) M) = M

theorem LinearMap.toMatrix_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) : (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i

theorem LinearMap.toMatrix_transpose_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (j : n) : ((LinearMap.toMatrix v₁ v₂) f).transpose j = ⇑(v₂.repr (f (v₁ j)))

theorem LinearMap.toMatrix_apply' {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) : (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i

theorem LinearMap.toMatrix_transpose_apply' {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (j : n) : ((LinearMap.toMatrix v₁ v₂) f).transpose j = ⇑(v₂.repr (f (v₁ j)))

theorem LinearMap.toMatrix_id {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : (LinearMap.toMatrix v₁ v₁) LinearMap.id = 1

This will be a special case of LinearMap.toMatrix_id_eq_basis_toMatrix.

@[simp]

theorem LinearMap.toMatrix_one {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : (LinearMap.toMatrix v₁ v₁) 1 = 1

@[simp]

theorem Matrix.toLin_one {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : (Matrix.toLin v₁ v₁) 1 = LinearMap.id

theorem LinearMap.toMatrix_reindexRange {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq M₁] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) : (LinearMap.toMatrix v₁.reindexRange v₂.reindexRange) f ⟨v₂ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (LinearMap.toMatrix v₁ v₂) f k i

@[simp]

theorem LinearMap.toMatrix_algebraMap {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (x : R) : (LinearMap.toMatrix v₁ v₁) ((algebraMap R (Module.End R M₁)) x) = (Matrix.scalar n) x

theorem LinearMap.toMatrix_mulVec_repr {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (x : M₁) : ((LinearMap.toMatrix v₁ v₂) f).mulVec ⇑(v₁.repr x) = ⇑(v₂.repr (f x))

@[simp]

theorem LinearMap.toMatrix_basis_equiv {R : Type u_1} [CommSemiring R] {l : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype l] [DecidableEq l] (b : Basis l R M₁) (b' : Basis l R M₂) : (LinearMap.toMatrix b' b) ↑(b'.equiv b (Equiv.refl l)) = 1

theorem Matrix.toLin_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (M : Matrix m n R) (v : M₁) : ((Matrix.toLin v₁ v₂) M) v = ∑ j : m, M.mulVec (⇑(v₁.repr v)) j • v₂ j

@[simp]

theorem Matrix.toLin_self {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (M : Matrix m n R) (i : n) : ((Matrix.toLin v₁ v₂) M) (v₁ i) = ∑ j : m, M j i • v₂ j

theorem LinearMap.toMatrix_comp {R : Type u_1} [CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Basis l R M₃) [Finite l] [DecidableEq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) : (LinearMap.toMatrix v₁ v₃) (f ∘ₗ g) = (LinearMap.toMatrix v₂ v₃) f * (LinearMap.toMatrix v₁ v₂) g

theorem LinearMap.toMatrix_mul {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₁) : (LinearMap.toMatrix v₁ v₁) (f * g) = (LinearMap.toMatrix v₁ v₁) f * (LinearMap.toMatrix v₁ v₁) g

theorem LinearMap.toMatrix_pow {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (k : ℕ) : (LinearMap.toMatrix v₁ v₁) f ^ k = (LinearMap.toMatrix v₁ v₁) (f ^ k)

theorem Matrix.toLin_mul {R : Type u_1} [CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Basis l R M₃) [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) : (Matrix.toLin v₁ v₃) (A * B) = (Matrix.toLin v₂ v₃) A ∘ₗ (Matrix.toLin v₁ v₂) B

theorem Matrix.toLin_mul_apply {R : Type u_1} [CommSemiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Basis l R M₃) [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) (x : M₁) : ((Matrix.toLin v₁ v₃) (A * B)) x = ((Matrix.toLin v₂ v₃) A) (((Matrix.toLin v₁ v₂) B) x)

Shortcut lemma for Matrix.toLin_mul and LinearMap.comp_apply.

@[simp]

theorem Matrix.toLinOfInv_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : M₁) : (Matrix.toLinOfInv v₁ v₂ hMM' hM'M) a = ((Matrix.toLin v₁ v₂) M) a

@[simp]

theorem Matrix.toLinOfInv_symm_apply {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) (a : M₂) : (Matrix.toLinOfInv v₁ v₂ hMM' hM'M).symm a = ((Matrix.toLin v₂ v₁) M') a

def Matrix.toLinOfInv {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : M₁ ≃ₗ[R] M₂

If M and M are each other's inverse matrices, Matrix.toLin M and Matrix.toLin M' form a linear equivalence.

Equations

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

def LinearMap.toMatrixAlgEquiv {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : (M₁ →ₗ[R] M₁) ≃ₐ[R] Matrix n n R

Given a basis of a module M₁ over a commutative ring R, we get an algebra equivalence between linear maps M₁ →ₗ M₁ and square matrices over R indexed by the basis.

Equations

• LinearMap.toMatrixAlgEquiv v₁ = AlgEquiv.ofLinearEquiv (LinearMap.toMatrix v₁ v₁) ⋯ ⋯

def Matrix.toLinAlgEquiv {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : Matrix n n R ≃ₐ[R] M₁ →ₗ[R] M₁

Given a basis of a module M₁ over a commutative ring R, we get an algebra equivalence between square matrices over R indexed by the basis and linear maps M₁ →ₗ M₁.

Equations

• Matrix.toLinAlgEquiv v₁ = (LinearMap.toMatrixAlgEquiv v₁).symm

@[simp]

theorem LinearMap.toMatrixAlgEquiv_symm {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : (LinearMap.toMatrixAlgEquiv v₁).symm = Matrix.toLinAlgEquiv v₁

@[simp]

theorem Matrix.toLinAlgEquiv_symm {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : (Matrix.toLinAlgEquiv v₁).symm = LinearMap.toMatrixAlgEquiv v₁

@[simp]

theorem Matrix.toLinAlgEquiv_toMatrixAlgEquiv {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) : (Matrix.toLinAlgEquiv v₁) ((LinearMap.toMatrixAlgEquiv v₁) f) = f

@[simp]

theorem LinearMap.toMatrixAlgEquiv_toLinAlgEquiv {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (M : Matrix n n R) : (LinearMap.toMatrixAlgEquiv v₁) ((Matrix.toLinAlgEquiv v₁) M) = M

theorem LinearMap.toMatrixAlgEquiv_apply {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i : n) (j : n) : (LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i

theorem LinearMap.toMatrixAlgEquiv_transpose_apply {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n) : ((LinearMap.toMatrixAlgEquiv v₁) f).transpose j = ⇑(v₁.repr (f (v₁ j)))

theorem LinearMap.toMatrixAlgEquiv_apply' {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i : n) (j : n) : (LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i

theorem LinearMap.toMatrixAlgEquiv_transpose_apply' {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n) : ((LinearMap.toMatrixAlgEquiv v₁) f).transpose j = ⇑(v₁.repr (f (v₁ j)))

theorem Matrix.toLinAlgEquiv_apply {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (M : Matrix n n R) (v : M₁) : ((Matrix.toLinAlgEquiv v₁) M) v = ∑ j : n, M.mulVec (⇑(v₁.repr v)) j • v₁ j

@[simp]

theorem Matrix.toLinAlgEquiv_self {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (M : Matrix n n R) (i : n) : ((Matrix.toLinAlgEquiv v₁) M) (v₁ i) = ∑ j : n, M j i • v₁ j

theorem LinearMap.toMatrixAlgEquiv_id {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : (LinearMap.toMatrixAlgEquiv v₁) LinearMap.id = 1

theorem Matrix.toLinAlgEquiv_one {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) : (Matrix.toLinAlgEquiv v₁) 1 = LinearMap.id

theorem LinearMap.toMatrixAlgEquiv_reindexRange {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k : n) (i : n) : (LinearMap.toMatrixAlgEquiv v₁.reindexRange) f ⟨v₁ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (LinearMap.toMatrixAlgEquiv v₁) f k i

theorem LinearMap.toMatrixAlgEquiv_comp {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₁) : (LinearMap.toMatrixAlgEquiv v₁) (f ∘ₗ g) = (LinearMap.toMatrixAlgEquiv v₁) f * (LinearMap.toMatrixAlgEquiv v₁) g

theorem LinearMap.toMatrixAlgEquiv_mul {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (f : M₁ →ₗ[R] M₁) (g : M₁ →ₗ[R] M₁) : (LinearMap.toMatrixAlgEquiv v₁) (f * g) = (LinearMap.toMatrixAlgEquiv v₁) f * (LinearMap.toMatrixAlgEquiv v₁) g

theorem Matrix.toLinAlgEquiv_mul {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (A : Matrix n n R) (B : Matrix n n R) : (Matrix.toLinAlgEquiv v₁) (A * B) = (Matrix.toLinAlgEquiv v₁) A ∘ₗ (Matrix.toLinAlgEquiv v₁) B

@[simp]

theorem Matrix.toLin_finTwoProd_apply {R : Type u_1} [CommSemiring R] (a : R) (b : R) (c : R) (d : R) (x : R × R) : ((Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) (Matrix.of ![![a, b], ![c, d]])) x = (a * x.1 + b * x.2, c * x.1 + d * x.2)

theorem Matrix.toLin_finTwoProd {R : Type u_1} [CommSemiring R] (a : R) (b : R) (c : R) (d : R) : (Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) (Matrix.of ![![a, b], ![c, d]]) = (a • LinearMap.fst R R R + b • LinearMap.snd R R R).prod (c • LinearMap.fst R R R + d • LinearMap.snd R R R)

@[simp]

theorem toMatrix_distrib_mul_action_toLinearMap {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Basis n R M₁) (x : R) : (LinearMap.toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun (x_1 : n) => x

theorem LinearMap.toMatrix_prodMap {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) [DecidableEq n] [DecidableEq m] [DecidableEq (n ⊕ m)] (φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) : (LinearMap.toMatrix (v₁.prod v₂) (v₁.prod v₂)) (LinearMap.prodMap φ₁ φ₂) = Matrix.fromBlocks ((LinearMap.toMatrix v₁ v₁) φ₁) 0 0 ((LinearMap.toMatrix v₂ v₂) φ₂)

theorem Algebra.toMatrix_lmul' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) (i : m) (j : m) : (LinearMap.toMatrix b b) ((Algebra.lmul R S) x) i j = (b.repr (x * b j)) i

@[simp]

theorem Algebra.toMatrix_lsmul {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : R) : (LinearMap.toMatrix b b) ((Algebra.lsmul R R S) x) = Matrix.diagonal fun (x_1 : m) => x

noncomputable def Algebra.leftMulMatrix {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) : S →ₐ[R] Matrix m m R

leftMulMatrix b x is the matrix corresponding to the linear map fun y ↦ x * y.

leftMulMatrix_eq_repr_mul gives a formula for the entries of leftMulMatrix.

This definition is useful for doing (more) explicit computations with LinearMap.mulLeft, such as the trace form or norm map for algebras.

Equations

• Algebra.leftMulMatrix b = { toFun := fun (x : S) => (LinearMap.toMatrix b b) ((Algebra.lmul R S) x), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem Algebra.leftMulMatrix_apply {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) : (Algebra.leftMulMatrix b) x = (LinearMap.toMatrix b b) ((Algebra.lmul R S) x)

theorem Algebra.leftMulMatrix_eq_repr_mul {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) (i : m) (j : m) : (Algebra.leftMulMatrix b) x i j = (b.repr (x * b j)) i

theorem Algebra.leftMulMatrix_mulVec_repr {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) (y : S) : ((Algebra.leftMulMatrix b) x).mulVec ⇑(b.repr y) = ⇑(b.repr (x * y))

@[simp]

theorem Algebra.toMatrix_lmul_eq {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) (x : S) : (LinearMap.toMatrix b b) (LinearMap.mulLeft R x) = (Algebra.leftMulMatrix b) x

theorem Algebra.leftMulMatrix_injective {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Basis m R S) : Function.Injective ⇑(Algebra.leftMulMatrix b)

theorem Algebra.smul_leftMulMatrix {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Ring T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (b : Basis m R S) (c : Basis n S T) (x : T) (ik : m × n) (jk : m × n) : (Algebra.leftMulMatrix (b.smul c)) x ik jk = (Algebra.leftMulMatrix b) ((Algebra.leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1

theorem Algebra.smul_leftMulMatrix_algebraMap {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Ring T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (b : Basis m R S) (c : Basis n S T) (x : S) : (Algebra.leftMulMatrix (b.smul c)) ((algebraMap S T) x) = Matrix.blockDiagonal fun (x_1 : n) => (Algebra.leftMulMatrix b) x

theorem Algebra.smul_leftMulMatrix_algebraMap_eq {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Ring T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (b : Basis m R S) (c : Basis n S T) (x : S) (i : m) (j : m) (k : n) : (Algebra.leftMulMatrix (b.smul c)) ((algebraMap S T) x) (i, k) (j, k) = (Algebra.leftMulMatrix b) x i j

theorem Algebra.smul_leftMulMatrix_algebraMap_ne {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [Ring T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] {m : Type u_4} {n : Type u_5} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (b : Basis m R S) (c : Basis n S T) (x : S) (i : m) (j : m) {k : n} {k' : n} (h : k ≠ k') : (Algebra.leftMulMatrix (b.smul c)) ((algebraMap S T) x) (i, k) (j, k') = 0

def algEquivMatrix' {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] : Module.End R (n → R) ≃ₐ[R] Matrix n n R

The natural equivalence between linear endomorphisms of finite free modules and square matrices is compatible with the algebra structures.

Equations

• algEquivMatrix' = let __src := LinearMap.toMatrix'; { toFun := (↑__src).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def LinearEquiv.algConj {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) : Module.End R M₁ ≃ₐ[R] Module.End R M₂

A linear equivalence of two modules induces an equivalence of algebras of their endomorphisms.

Equations

• e.algConj = let __src := e.conj; { toFun := (↑__src).toFun, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def algEquivMatrix {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] {M : Type u_3} [AddCommGroup M] [Module R M] [Fintype n] (h : Basis n R M) : Module.End R M ≃ₐ[R] Matrix n n R

A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.

Equations

• algEquivMatrix h = h.equivFun.algConj.trans algEquivMatrix'

theorem Basis.linearMap_repr_symm_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) : ∀ (a : ι₂ × ι₁ →₀ R), (b₁.linearMap b₂).repr.symm a = (Matrix.toLin b₁ b₂) ((Finsupp.total (ι₂ × ι₁) (Matrix ι₂ ι₁ R) R ⇑(Matrix.stdBasis R ι₂ ι₁)) a)

@[simp]

theorem Basis.linearMap_repr_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) : ∀ (a : M₁ →ₗ[R] M₂), (b₁.linearMap b₂).repr a = (Matrix.stdBasis R ι₂ ι₁).repr ((LinearMap.toMatrix b₁ b₂) a)

noncomputable def Basis.linearMap {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) : Basis (ι₂ × ι₁) R (M₁ →ₗ[R] M₂)

The standard basis of the space linear maps between two modules induced by a basis of the domain and codomain.

If M₁ and M₂ are modules with basis b₁ and b₂ respectively indexed by finite types ι₁ and ι₂, then Basis.linearMap b₁ b₂ is the basis of M₁ →ₗ[R] M₂ indexed by ι₂ × ι₁ where (i, j) indexes the linear map that sends b j to b i and sends all other basis vectors to 0.

Equations

• b₁.linearMap b₂ = (Matrix.stdBasis R ι₂ ι₁).map (LinearMap.toMatrix b₁ b₂).symm

theorem Basis.linearMap_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (ij : ι₂ × ι₁) : (b₁.linearMap b₂) ij = (Matrix.toLin b₁ b₂) ((Matrix.stdBasis R ι₂ ι₁) ij)

theorem Basis.linearMap_apply_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) (ij : ι₂ × ι₁) (k : ι₁) : ((b₁.linearMap b₂) ij) (b₁ k) = if ij.2 = k then b₂ ij.1 else 0

@[simp]

theorem Basis.end_repr_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) : ∀ (a : M →ₗ[R] M), b.end.repr a = (Matrix.stdBasis R ι ι).repr ((LinearMap.toMatrix b b) a)

theorem Basis.end_repr_symm_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) : ∀ (a : ι × ι →₀ R), b.end.repr.symm a = (Matrix.toLin b b) ((Finsupp.total (ι × ι) (Matrix ι ι R) R ⇑(Matrix.stdBasis R ι ι)) a)

@[reducible, inline]

noncomputable abbrev Basis.end {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) : Basis (ι × ι) R (Module.End R M)

The standard basis of the endomorphism algebra of a module induced by a basis of the module.

If M is a module with basis b indexed by a finite type ι, then Basis.end b is the basis of Module.End R M indexed by ι × ι where (i, j) indexes the linear map that sends b j to b i and sends all other basis vectors to 0.

Equations

• b.end = b.linearMap b

theorem Basis.end_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) (ij : ι × ι) : b.end ij = (Matrix.toLin b b) ((Matrix.stdBasis R ι ι) ij)

theorem Basis.end_apply_apply {R : Type u_1} {M : Type u_2} {ι : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) (ij : ι × ι) (k : ι) : (b.end ij) (b k) = if ij.2 = k then b ij.1 else 0