# 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

### Bilinear versions of matrix products #

The definitions in this section are stated with two extra rings, to allow for non-commutative rings.

source
def Matrix.vecMulBilin {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [Semiring R] [Semiring S] [NonUnitalNonAssocSemiring A] [Module R A] [Module S A] [SMulCommClass S R A] [SMulCommClass S A A] [IsScalarTower R A A] [Fintype m] :
(m → A) →ₗ[R] Matrix m n A →ₗ[S] n → A

`Matrix.vecMul` as a bilinear map.

When `A` is non-commutative, this can be instantiated as `vecMulBilin A Aᵐᵒᵖ`

Equations

- Matrix.vecMulBilin R S = { toFun := fun (x : m → A) => { toFun := fun (M : Matrix m n A) => Matrix.vecMul x M, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem Matrix.vecMulBilin_apply {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [Semiring R] [Semiring S] [NonUnitalNonAssocSemiring A] [Module R A] [Module S A] [SMulCommClass S R A] [SMulCommClass S A A] [IsScalarTower R A A] [Fintype m] (v : m → A) (M : Matrix m n A) :
((vecMulBilin R S) v) M = vecMul v M
source
def Matrix.mulVecBilin {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [Semiring R] [Semiring S] [NonUnitalNonAssocSemiring A] [Module R A] [Module S A] [SMulCommClass S R A] [SMulCommClass S A A] [IsScalarTower R A A] [Fintype n] :
Matrix m n A →ₗ[R] (n → A) →ₗ[S] m → A

`Matrix.mulVec` as a bilinear map.

When `A` is non-commutative, this can be instantiated as `mulVecBilin A Aᵐᵒᵖ`

Equations

- Matrix.mulVecBilin R S = { toFun := fun (M : Matrix m n A) => { toFun := fun (x : n → A) => M.mulVec x, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem Matrix.mulVecBilin_apply {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [Semiring R] [Semiring S] [NonUnitalNonAssocSemiring A] [Module R A] [Module S A] [SMulCommClass S R A] [SMulCommClass S A A] [IsScalarTower R A A] [Fintype n] (M : Matrix m n A) (v : n → A) :
((mulVecBilin R S) M) v = M.mulVec v
source
def vecMulVecBilin {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [Semiring R] [Semiring S] [NonUnitalNonAssocSemiring A] [Module R A] [Module S A] [SMulCommClass S R A] [SMulCommClass S A A] [IsScalarTower R A A] :
(m → A) →ₗ[R] (n → A) →ₗ[S] Matrix m n A

`vecMulVec` as a bilinear map.

When `A` is noncommutative, `R` and `S` can be instantiated as `vecMulVecLinear A Aᵐᵒᵖ`.

Equations

- vecMulVecBilin R S = { toFun := fun (x : m → A) => { toFun := fun (y : n → A) => Matrix.vecMulVec x y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem vecMulVecBilin_apply_apply {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [Semiring R] [Semiring S] [NonUnitalNonAssocSemiring A] [Module R A] [Module S A] [SMulCommClass S R A] [SMulCommClass S A A] [IsScalarTower R A A] (x : m → A) (y : n → A) :
((vecMulVecBilin R S) x) y = Matrix.vecMulVec x y
source
def dotProductBilin {m : Type u_2} (R : Type u_4) (S : Type u_5) {A : Type u_6} [Semiring R] [Semiring S] [NonUnitalNonAssocSemiring A] [Module R A] [Module S A] [SMulCommClass S R A] [SMulCommClass S A A] [IsScalarTower R A A] [Fintype m] :
(m → A) →ₗ[R] (m → A) →ₗ[S] A

`vecMulVec` as a bilinear map.

When `A` is noncommutative, `R` and `S` can be instantiated as `vecMulVecLinear A Aᵐᵒᵖ`.

Equations

- dotProductBilin R S = { toFun := fun (x : m → A) => { toFun := fun (y : m → A) => x ⬝ᵥ y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem dotProductBilin_apply_apply {m : Type u_2} (R : Type u_4) (S : Type u_5) {A : Type u_6} [Semiring R] [Semiring S] [NonUnitalNonAssocSemiring A] [Module R A] [Module S A] [SMulCommClass S R A] [SMulCommClass S A A] [IsScalarTower R A A] [Fintype m] (x y : m → A) :
((dotProductBilin R S) x) y = x ⬝ᵥ y
source
@[reducible, inline]
abbrev 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.

Note this is a special case of `Matrix.vecMulBilin`.

Equations

- M.vecMulLinear = (Matrix.vecMulBilin R R ᵐᵒᵖ).flip M

Instances For

source
@[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 = vecMul x M
source
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) => vecMul v M
source
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.row)
source
theorem Matrix.vecMul_injective_iff {R : Type u_1} [Semiring R] {m : Type u_3} {n : Type u_4} [Fintype m] {M : Matrix m n R} :
(Function.Injective fun (v : m → R) => vecMul v M) ↔ LinearIndependent R M.row
source
theorem Matrix.linearIndependent_rows_of_isUnit {R : Type u_1} [Semiring R] {m : Type u_3} [Fintype m] {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) :
LinearIndependent R A.row
source
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.

Instances For

source
@[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

Instances For

source
@[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) :
(toLinearMapRight' M) v = vecMul v M
source
@[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) :
toLinearMapRight' (M * N) = toLinearMapRight' N ∘ₗ toLinearMapRight' M
source
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) :
(toLinearMapRight' (M * N)) x = (toLinearMapRight' N) ((toLinearMapRight' M) x)
source
@[simp]
theorem Matrix.toLinearMapRight'_one {R : Type u_1} [Semiring R] {m : Type u_3} [Fintype m] [DecidableEq m] :
toLinearMapRight' 1 = LinearMap.id
source
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

- Matrix.toLinearEquivRight'OfInv hMM' hM'M = { toFun := ⇑(Matrix.toLinearMapRight' M'), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(Matrix.toLinearMapRight' M), left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[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✝ : m) :
(toLinearEquivRight'OfInv hMM' hM'M) a a✝ = (toLinearMapRight' M') a a✝
source
@[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✝ : n) :
(toLinearEquivRight'OfInv hMM' hM'M).symm a a✝ = (toLinearMapRight' M) a a✝

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

source
@[reducible, inline]
abbrev 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` as a linear map.

Note this is a special case of `Matrix.mulVecBilin`.

Equations

- M.mulVecLin = (Matrix.mulVecBilin R R) M

Instances For

source
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
source
@[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
source
@[simp]
theorem Matrix.mulVecLin_zero {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] :
mulVecLin 0 = 0
source
@[simp]
theorem Matrix.mulVecLin_add {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] (M N : Matrix m n R) :
(M + N).mulVecLin = M.mulVecLin + N.mulVecLin
source
@[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
source
@[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
source
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
source
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) :
((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 `LinearEquiv`s.

source
@[simp]
theorem Matrix.mulVecLin_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [Fintype n] [DecidableEq n] :
mulVecLin 1 = LinearMap.id
source
@[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
source
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
source
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.col)
source
theorem Matrix.mulVec_injective_iff {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [Fintype n] {M : Matrix m n R} :
Function.Injective M.mulVec ↔ LinearIndependent R M.col
source
theorem Matrix.linearIndependent_cols_of_isUnit {R : Type u_1} [CommSemiring R] {m : Type u_4} [Fintype m] {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) :
LinearIndependent R A.col
source
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.

Instances For

source
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.mulVecLin`.

Equations

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

Instances For

source
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) :
toLin' M = M.mulVecLin
source
@[simp]
theorem LinearMap.toMatrix'_symm {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] :
toMatrix'.symm = Matrix.toLin'
source
@[simp]
theorem Matrix.toLin'_symm {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] :
toLin'.symm = LinearMap.toMatrix'
source
@[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) :
toMatrix' (Matrix.toLin' M) = M
source
@[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) :
toLin' (LinearMap.toMatrix' f) = f
source
@[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) :
toMatrix' f i j = f (fun (j' : n) => if j' = j then 1 else 0) i
source
@[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) :
(toLin' M) v = M.mulVec v
source
@[simp]
theorem LinearMap.toMatrix'_mulVec {R : Type u_1} [CommSemiring R] {m : Type u_4} {n : Type u_5} [DecidableEq n] [Fintype n] (f : (n → R) →ₗ[R] m → R) (v : n → R) :
(toMatrix' f).mulVec v = f v
source
@[simp]
theorem Matrix.toLin'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
toLin' 1 = LinearMap.id
source
@[simp]
theorem LinearMap.toMatrix'_id {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
toMatrix' id = 1
source
@[simp]
theorem LinearMap.toMatrix'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
toMatrix' 1 = 1
source
@[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) :
toLin' (M * N) = toLin' M ∘ₗ toLin' N
source
@[simp]
theorem Matrix.toLin'_pow {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix n n R) (k : ℕ) :
toLin' (M ^ k) = toLin' M ^ k
source
@[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) :
toLin' (M.submatrix f₁ ⇑e₂) = LinearMap.funLeft R R f₁ ∘ₗ toLin' M ∘ₗ LinearMap.funLeft R R ⇑e₂.symm
source
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) :
toLin' ((reindex e₁ e₂) M) = ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ toLin' M ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)

A variant of `Matrix.toLin'_submatrix` that keeps around `LinearEquiv`s.

source
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) :
(toLin' (M * N)) x = (toLin' M) ((toLin' N) x)

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

source
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) :
toMatrix' (f ∘ₗ g) = toMatrix' f * toMatrix' g
source
theorem LinearMap.toMatrix'_mul {R : Type u_1} [CommSemiring R] {m : Type u_4} [Fintype m] [DecidableEq m] (f g : (m → R) →ₗ[R] m → R) :
toMatrix' (f * g) = toMatrix' f * toMatrix' g
source
@[simp]
theorem LinearMap.toMatrix'_algebraMap {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (x : R) :
toMatrix' ((algebraMap R (Module.End R (n → R))) x) = (Matrix.scalar n) x
source
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 (toLin' M) = ⊥ ↔ ∀ (v : n → R), M.mulVec v = 0 → v = 0
source
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 (toLin' M) = Submodule.span R (Set.range M.col)
source
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 = { toFun := ⇑(Matrix.toLin' M'), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(Matrix.toLin' M), left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[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✝ : m) :
(toLin'OfInv hMM' hM'M).symm a a✝ = (toLin' M) a a✝
source
@[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✝ : n) :
(toLin'OfInv hMM' hM'M) a a✝ = (toLin' M') a a✝
source
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' ⋯ ⋯

Instances For

source
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

Instances For

source
@[simp]
theorem LinearMap.toMatrixAlgEquiv'_symm {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
toMatrixAlgEquiv'.symm = Matrix.toLinAlgEquiv'
source
@[simp]
theorem Matrix.toLinAlgEquiv'_symm {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
toLinAlgEquiv'.symm = LinearMap.toMatrixAlgEquiv'
source
@[simp]
theorem LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv' {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (M : Matrix n n R) :
toMatrixAlgEquiv' (Matrix.toLinAlgEquiv' M) = M
source
@[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) :
toLinAlgEquiv' (LinearMap.toMatrixAlgEquiv' f) = f
source
@[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 j : n) :
toMatrixAlgEquiv' f i j = f (fun (j' : n) => if j' = j then 1 else 0) i
source
@[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) :
(toLinAlgEquiv' M) v = M.mulVec v
source
theorem Matrix.toLinAlgEquiv'_one {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
toLinAlgEquiv' 1 = LinearMap.id
source
@[simp]
theorem LinearMap.toMatrixAlgEquiv'_id {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] :
toMatrixAlgEquiv' id = 1
source
theorem LinearMap.toMatrixAlgEquiv'_comp {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f g : (n → R) →ₗ[R] n → R) :
toMatrixAlgEquiv' (f ∘ₗ g) = toMatrixAlgEquiv' f * toMatrixAlgEquiv' g
source
theorem LinearMap.toMatrixAlgEquiv'_mul {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] (f g : (n → R) →ₗ[R] n → R) :
toMatrixAlgEquiv' (f * g) = toMatrixAlgEquiv' f * toMatrixAlgEquiv' g
source
@[simp]
theorem LinearMap.isUnit_toMatrix'_iff {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] {f : (n → R) →ₗ[R] n → R} :
IsUnit (toMatrix' f) ↔ IsUnit f
source
@[simp]
theorem Matrix.isUnit_toLin'_iff {R : Type u_1} [CommSemiring R] {n : Type u_5} [DecidableEq n] [Fintype n] {M : Matrix n n R} :
IsUnit (toLin' M) ↔ IsUnit M
source
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₁ : Module.Basis n R M₁) (v₂ : Module.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'

Instances For

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

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

source
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₁ : Module.Basis n R M₁) (v₂ : Module.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

Instances For

source
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] :
toLin (Pi.basisFun R n) (Pi.basisFun R m) = toLin'

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

source
@[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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) :
(toMatrix v₁ v₂).symm = Matrix.toLin v₁ v₂
source
@[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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) :
(toLin v₁ v₂).symm = LinearMap.toMatrix v₁ v₂
source
@[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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) :
(toLin v₁ v₂) ((LinearMap.toMatrix v₁ v₂) f) = f
source
@[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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (M : Matrix m n R) :
(toMatrix v₁ v₂) ((Matrix.toLin v₁ v₂) M) = M
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
(toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (j : n) :
((toMatrix v₁ v₂) f).transpose j = ⇑(v₂.repr (f (v₁ j)))
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
(toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (j : n) :
((toMatrix v₁ v₂) f).transpose j = ⇑(v₂.repr (f (v₁ j)))
source
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₁ : Module.Basis n R M₁) :
(toMatrix v₁ v₁) id = 1

This will be a special case of `LinearMap.toMatrix_id_eq_basis_toMatrix`.

source
@[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₁ : Module.Basis n R M₁) :
(toMatrix v₁ v₁) 1 = 1
source
@[simp]
theorem LinearMap.toMatrix_singleton {R : Type u_1} [CommSemiring R] {ι : Type u_7} [Unique ι] (f : R →ₗ[R] R) (i j : ι) :
(toMatrix (Module.Basis.singleton ι R) (Module.Basis.singleton ι R)) f i j = f 1
source
@[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₁ : Module.Basis n R M₁) :
(toLin v₁ v₁) 1 = LinearMap.id
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [DecidableEq M₁] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
(toMatrix v₁.reindexRange v₂.reindexRange) f ⟨v₂ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrix v₁ v₂) f k i
source
@[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₁ : Module.Basis n R M₁) (x : R) :
(toMatrix v₁ v₁) ((algebraMap R (Module.End R M₁)) x) = (Matrix.scalar n) x
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] M₂) (x : M₁) :
((toMatrix v₁ v₂) f).mulVec ⇑(v₁.repr x) = ⇑(v₂.repr (f x))
source
@[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 : Module.Basis l R M₁) (b' : Module.Basis l R M₂) :
(toMatrix b' b) ↑(b'.equiv b (Equiv.refl l)) = 1
source
theorem LinearMap.toMatrix_smulBasis_left {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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {G : Type u_7} [Group G] [DistribMulAction G M₁] [SMulCommClass G R M₁] (g : G) (f : M₁ →ₗ[R] M₂) :
(toMatrix (g • v₁) v₂) f = (toMatrix v₁ v₂) (f ∘ₗ DistribMulAction.toLinearMap R M₁ g)
source
theorem LinearMap.toMatrix_smulBasis_right {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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {G : Type u_7} [Group G] [DistribMulAction G M₂] [SMulCommClass G R M₂] (g : G) (f : M₁ →ₗ[R] M₂) :
(toMatrix v₁ (g • v₂)) f = (toMatrix v₁ v₂) (DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f)
source
theorem LinearMap.toMatrix_toSpanSingleton {R : Type u_1} [CommSemiring R] {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {M₂ : Type u_6} [AddCommMonoid M₂] [Module R M₂] (v₁ : Module.Basis n R R) (v₂ : Module.Basis m R M₂) (x : M₂) :
(toMatrix v₁ v₂) (toSpanSingleton R M₂ x) = Matrix.vecMulVec ⇑(v₂.repr x) ⇑v₁

The matrix of `toSpanSingleton R M₂ x` given by bases `v₁` and `v₂` is equal to `vecMulVec (v₂.repr x) v₁`. When `v₁ = Module.Basis.singleton` then this is the column matrix of `v₂.repr x`.

source
@[simp]
theorem LinearMap.toMatrix_smulRight {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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (f : M₁ →ₗ[R] R) (x : M₂) :
(toMatrix v₁ v₂) (f.smulRight x) = Matrix.vecMulVec (⇑(v₂.repr x)) (⇑f ∘ ⇑v₁)
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (M : Matrix m n R) (v : M₁) :
((toLin v₁ v₂) M) v = ∑ j : m, M.mulVec (⇑(v₁.repr v)) j • v₂ j
source
@[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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (M : Matrix m n R) (i : n) :
((toLin v₁ v₂) M) (v₁ i) = ∑ j : m, M j i • v₂ j
source
theorem Matrix.toLin_apply_eq_zero_iff {m : Type u_3} {n : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] {R : Type u_7} {M₁ : Type u_8} {M₂ : Type u_9} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {v₁ : Module.Basis n R M₁} {v₂ : Module.Basis m R M₂} {A : Matrix m n R} {x : M₁} :
((toLin v₁ v₂) A) x = 0 ↔ ∀ (j : m), A.mulVec (⇑(v₁.repr x)) j = 0
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Module.Basis l R M₃) [Finite l] [DecidableEq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
(toMatrix v₁ v₃) (f ∘ₗ g) = (toMatrix v₂ v₃) f * (toMatrix v₁ v₂) g
source
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₁ : Module.Basis n R M₁) (f g : M₁ →ₗ[R] M₁) :
(toMatrix v₁ v₁) (f * g) = (toMatrix v₁ v₁) f * (toMatrix v₁ v₁) g
source
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₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (k : ℕ) :
(toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Module.Basis l R M₃) [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) :
(toLin v₁ v₃) (A * B) = (toLin v₂ v₃) A ∘ₗ (toLin v₁ v₂) B
source
@[simp]
theorem Matrix.toLin_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₁ : Module.Basis n R M₁) (A : Matrix n n R) (k : ℕ) :
(toLin v₁ v₁) (A ^ k) = (toLin v₁ v₁) A ^ k
source
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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {M₃ : Type u_7} [AddCommMonoid M₃] [Module R M₃] (v₃ : Module.Basis l R M₃) [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) (x : M₁) :
((toLin v₁ v₃) (A * B)) x = ((toLin v₂ v₃) A) (((toLin v₁ v₂) B) x)

Shortcut lemma for `Matrix.toLin_mul` and `LinearMap.comp_apply`.

source
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₁ : Module.Basis n R M₁) (v₂ : Module.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

- Matrix.toLinOfInv v₁ v₂ hMM' hM'M = { toFun := ⇑((Matrix.toLin v₁ v₂) M), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑((Matrix.toLin v₂ v₁) M'), left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[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₁ : Module.Basis n R M₁) (v₂ : Module.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₁) :
(toLinOfInv v₁ v₂ hMM' hM'M) a = ((toLin v₁ v₂) M) a
source
@[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₁ : Module.Basis n R M₁) (v₂ : Module.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₂) :
(toLinOfInv v₁ v₂ hMM' hM'M).symm a = ((toLin v₂ v₁) M') a
source
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₁ : Module.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₁) ⋯ ⋯

Instances For

source
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₁ : Module.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

Instances For

source
@[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₁ : Module.Basis n R M₁) :
(toMatrixAlgEquiv v₁).symm = Matrix.toLinAlgEquiv v₁
source
@[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₁ : Module.Basis n R M₁) :
(toLinAlgEquiv v₁).symm = LinearMap.toMatrixAlgEquiv v₁
source
@[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₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) :
(toLinAlgEquiv v₁) ((LinearMap.toMatrixAlgEquiv v₁) f) = f
source
@[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₁ : Module.Basis n R M₁) (M : Matrix n n R) :
(toMatrixAlgEquiv v₁) ((Matrix.toLinAlgEquiv v₁) M) = M
source
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₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i j : n) :
(toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
source
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₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n) :
((toMatrixAlgEquiv v₁) f).transpose j = ⇑(v₁.repr (f (v₁ j)))
source
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₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (i j : n) :
(toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
source
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₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n) :
((toMatrixAlgEquiv v₁) f).transpose j = ⇑(v₁.repr (f (v₁ j)))
source
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₁ : Module.Basis n R M₁) (M : Matrix n n R) (v : M₁) :
((toLinAlgEquiv v₁) M) v = ∑ j : n, M.mulVec (⇑(v₁.repr v)) j • v₁ j
source
@[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₁ : Module.Basis n R M₁) (M : Matrix n n R) (i : n) :
((toLinAlgEquiv v₁) M) (v₁ i) = ∑ j : n, M j i • v₁ j
source
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₁ : Module.Basis n R M₁) :
(toMatrixAlgEquiv v₁) id = 1
source
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₁ : Module.Basis n R M₁) :
(toLinAlgEquiv v₁) 1 = LinearMap.id
source
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₁ : Module.Basis n R M₁) [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) :
(toMatrixAlgEquiv v₁.reindexRange) f ⟨v₁ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrixAlgEquiv v₁) f k i
source
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₁ : Module.Basis n R M₁) (f g : M₁ →ₗ[R] M₁) :
(toMatrixAlgEquiv v₁) (f ∘ₗ g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g
source
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₁ : Module.Basis n R M₁) (f g : M₁ →ₗ[R] M₁) :
(toMatrixAlgEquiv v₁) (f * g) = (toMatrixAlgEquiv v₁) f * (toMatrixAlgEquiv v₁) g
source
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₁ : Module.Basis n R M₁) (A B : Matrix n n R) :
(toLinAlgEquiv v₁) (A * B) = (toLinAlgEquiv v₁) A ∘ₗ (toLinAlgEquiv v₁) B
source
@[simp]
theorem LinearMap.isUnit_toMatrix_iff {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Module.Basis n R M₁) {f : M₁ →ₗ[R] M₁} :
IsUnit ((toMatrix v₁ v₁) f) ↔ IsUnit f
source
@[simp]
theorem Matrix.isUnit_toLin_iff {R : Type u_1} [CommSemiring R] {n : Type u_4} [Fintype n] [DecidableEq n] {M₁ : Type u_5} [AddCommMonoid M₁] [Module R M₁] (v₁ : Module.Basis n R M₁) {M : Matrix n n R} :
IsUnit ((toLin v₁ v₁) M) ↔ IsUnit M
source
@[simp]
theorem Matrix.toLin_finTwoProd_apply {R : Type u_1} [CommSemiring R] (a b c d : R) (x : R × R) :
((toLin (Module.Basis.finTwoProd R) (Module.Basis.finTwoProd R)) !![a, b; c, d]) x = (a * x.1 + b * x.2, c * x.1 + d * x.2)
source
theorem Matrix.toLin_finTwoProd {R : Type u_1} [CommSemiring R] (a b c d : R) :
(toLin (Module.Basis.finTwoProd R) (Module.Basis.finTwoProd R)) !![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)
source
@[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₁ : Module.Basis n R M₁) (x : R) :
(LinearMap.toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun (x_1 : n) => x
source
theorem LinearMap.toMatrix_prodMap {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₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [DecidableEq m] [DecidableEq (n ⊕ m)] (φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) :
(toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) = Matrix.fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂)
source
theorem Algebra.toMatrix_lmul' {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x : S) (i j : m) :
(LinearMap.toMatrix b b) ((lmul R S) x) i j = (b.repr (x * b j)) i
source
@[simp]
theorem Algebra.toMatrix_lsmul {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x : R) :
(LinearMap.toMatrix b b) ((lsmul R R S) x) = Matrix.diagonal fun (x_1 : m) => x
source
noncomputable def Algebra.leftMulMatrix {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.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' := ⋯ }

Instances For

source
theorem Algebra.leftMulMatrix_apply {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x : S) :
(leftMulMatrix b) x = (LinearMap.toMatrix b b) ((lmul R S) x)
source
theorem Algebra.leftMulMatrix_eq_repr_mul {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x : S) (i j : m) :
(leftMulMatrix b) x i j = (b.repr (x * b j)) i
source
theorem Algebra.leftMulMatrix_mulVec_repr {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x y : S) :
((leftMulMatrix b) x).mulVec ⇑(b.repr y) = ⇑(b.repr (x * y))
source
@[simp]
theorem Algebra.toMatrix_lmul_eq {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) (x : S) :
(LinearMap.toMatrix b b) (LinearMap.mulLeft R x) = (leftMulMatrix b) x
source
theorem Algebra.leftMulMatrix_injective {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) :
Function.Injective ⇑(leftMulMatrix b)
source
@[simp]
theorem Algebra.smul_leftMulMatrix {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] {m : Type u_3} [Fintype m] [DecidableEq m] (b : Module.Basis m R S) {G : Type u_4} [Group G] [DistribMulAction G S] [SMulCommClass G R S] [SMulCommClass G S S] (g : G) (x : S) :
(leftMulMatrix (g • b)) x = (leftMulMatrix b) x
source
theorem LinearMap.restrictScalars_toMatrix {R : Type u_1} [CommSemiring R] {m : Type u_3} [Fintype m] [DecidableEq m] {A : Type u_4} {M : Type u_5} {n : Type u_6} [Fintype n] [DecidableEq n] [CommSemiring A] [AddCommMonoid M] [Module R M] [Module A M] [Algebra R A] [IsScalarTower R A M] (bA : Module.Basis m R A) (bM : Module.Basis n A M) (f : M →ₗ[A] M) :
(toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) = (Matrix.comp n n m m R) (((toMatrix bM bM) f).map ⇑(Algebra.leftMulMatrix bA))
source
theorem Algebra.smulTower_leftMulMatrix {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring 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 : Module.Basis m R S) (c : Module.Basis n S T) (x : T) (ik jk : m × n) :
(leftMulMatrix (b.smulTower c)) x ik jk = (leftMulMatrix b) ((leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1
source
theorem Algebra.smulTower_leftMulMatrix_algebraMap {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring 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 : Module.Basis m R S) (c : Module.Basis n S T) (x : S) :
(leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) = Matrix.blockDiagonal fun (x_1 : n) => (leftMulMatrix b) x
source
theorem Algebra.smulTower_leftMulMatrix_algebraMap_eq {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring 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 : Module.Basis m R S) (c : Module.Basis n S T) (x : S) (i j : m) (k : n) :
(leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k) = (leftMulMatrix b) x i j
source
theorem Algebra.smulTower_leftMulMatrix_algebraMap_ne {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring 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 : Module.Basis m R S) (c : Module.Basis n S T) (x : S) (i j : m) {k k' : n} (h : k ≠ k') :
(leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') = 0
source
def algEquivMatrix' {R : Type u_1} [CommSemiring R] {n : Type u_3} [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' = LinearMap.toMatrixAlgEquiv'

Instances For

source
def LinearEquiv.algConj (R : Type u_1) {S : Type u_2} [CommSemiring R] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Semiring S] [Module S M₁] [Module S M₂] [SMulCommClass S R M₁] [SMulCommClass S R M₂] [SMul R S] [IsScalarTower R S M₁] [IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) :
Module.End S M₁ ≃ₐ[R] Module.End S M₂

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

Equations

- LinearEquiv.algConj R e = { toEquiv := e.conjRingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem LinearEquiv.algConj_symm_apply_apply (R : Type u_1) {S : Type u_2} [CommSemiring R] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Semiring S] [Module S M₁] [Module S M₂] [SMulCommClass S R M₁] [SMulCommClass S R M₂] [SMul R S] [IsScalarTower R S M₁] [IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) (f : M₂ →ₗ[S] M₂) (a✝ : M₁) :
((algConj R e).symm f) a✝ = e.symm (f (e a✝))
source
@[simp]
theorem LinearEquiv.algConj_apply_apply (R : Type u_1) {S : Type u_2} [CommSemiring R] {M₁ : Type u_5} {M₂ : Type u_6} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Semiring S] [Module S M₁] [Module S M₂] [SMulCommClass S R M₁] [SMulCommClass S R M₂] [SMul R S] [IsScalarTower R S M₁] [IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) (f : M₁ →ₗ[S] M₁) (a✝ : M₂) :
((algConj R e) f) a✝ = e (f (e.symm a✝))
source
def algEquivMatrix {R : Type u_1} [CommSemiring R] {n : Type u_3} [DecidableEq n] {M : Type u_4} [AddCommMonoid M] [Module R M] [Fintype n] (h : Module.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 = (LinearEquiv.algConj R h.equivFun).trans algEquivMatrix'

Instances For

source
noncomputable def Module.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

Instances For

source
theorem Module.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.linearCombination R ⇑(Matrix.stdBasis R ι₂ ι₁)) a✝)
source
@[simp]
theorem Module.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✝)
source
theorem Module.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)
source
theorem Module.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
source
@[reducible, inline]
noncomputable abbrev Module.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 (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

Instances For

source
theorem Module.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.linearCombination R ⇑(Matrix.stdBasis R ι ι)) a✝)
source
@[simp]
theorem Module.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✝)
source
theorem Module.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)
source
theorem Module.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
source
def endVecRingEquivMatrixEnd (ι : Type u_1) [Fintype ι] [DecidableEq ι] (A : Type u_3) [Semiring A] (M : Type u_4) [AddCommMonoid M] [Module A M] :
Module.End A (ι → M) ≃+* Matrix ι ι (Module.End A M)

Let `M` be an `A`-module. Every `A`-linear map `Mⁿ → Mⁿ` corresponds to a `n×n`-matrix whose entries are `A`-linear maps `M → M`. In another word, we have`End(Mⁿ) ≅ Matₙₓₙ(End(M))` defined by: `(f : Mⁿ → Mⁿ) ↦ (x ↦ f (0, ..., x at j-th position, ..., 0) i)ᵢⱼ` and `m : Matₙₓₙ(End(M)) ↦ (v ↦ ∑ⱼ mᵢⱼ(vⱼ))`.

See also `LinearMap.toMatrix'`

Equations

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

Instances For

source
def endVecAlgEquivMatrixEnd (ι : Type u_1) [Fintype ι] [DecidableEq ι] (R : Type u_2) [CommSemiring R] (A : Type u_3) [Semiring A] [Algebra R A] (M : Type u_4) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] :
Module.End A (ι → M) ≃ₐ[R] Matrix ι ι (Module.End A M)

Let `M` be an `A`-module. Every `A`-linear map `Mⁿ → Mⁿ` corresponds to a `n×n`-matrix whose entries are `R`-linear maps `M → M`. In another word, we have`End(Mⁿ) ≅ Matₙₓₙ(End(M))` defined by: `(f : Mⁿ → Mⁿ) ↦ (x ↦ f (0, ..., x at j-th position, ..., 0) i)ᵢⱼ` and `m : Matₙₓₙ(End(M)) ↦ (v ↦ ∑ⱼ mᵢⱼ(vⱼ))`.

See also `LinearMap.toMatrix'`

Equations

- endVecAlgEquivMatrixEnd ι R A M = { toEquiv := (endVecRingEquivMatrixEnd ι A M).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem endVecAlgEquivMatrixEnd_apply_apply (ι : Type u_1) [Fintype ι] [DecidableEq ι] (R : Type u_2) [CommSemiring R] (A : Type u_3) [Semiring A] [Algebra R A] (M : Type u_4) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (f : Module.End A (ι → M)) (i j : ι) (x : M) :
((endVecAlgEquivMatrixEnd ι R A M) f i j) x = f (Pi.single j x) i
source
@[simp]
theorem endVecAlgEquivMatrixEnd_symm_apply_apply (ι : Type u_1) [Fintype ι] [DecidableEq ι] (R : Type u_2) [CommSemiring R] (A : Type u_3) [Semiring A] [Algebra R A] (M : Type u_4) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (m : Matrix ι ι (Module.End A M)) (x : ι → M) (i : ι) :
((endVecAlgEquivMatrixEnd ι R A M).symm m) x i = ∑ j : ι, (m i j) (x j)