Mathlib.LinearAlgebra.Matrix.StdBasis

Basis.matrix definition

(b : Basis ι R M) : Basis (m × n × ι) R (Matrix m n M)

Full source

/-- The standard basis of `Matrix m n M` given a basis on `M`. -/
protected noncomputable def matrix (b : Basis ι R M) :
    Basis (m × n × ι) R (Matrix m n M) :=
  Basis.reindex (Pi.basis fun _ : m => Pi.basis fun _ : n => b)
    ((Equiv.sigmaEquivProd _ _).trans <| .prodCongr (.refl _) (Equiv.sigmaEquivProd _ _))
    |>.map (Matrix.ofLinearEquiv R)

Standard basis of matrices induced by a module basis

Informal description

Given a basis $b$ for an $R$-module $M$ indexed by $\iota$, the function `Basis.matrix` constructs the standard basis for the matrix space $\text{Matrix}_{m \times n}(M)$ over $R$. The new basis is indexed by triples $(i, j, k)$ where $i \in m$, $j \in n$, and $k \in \iota$, and the basis matrix corresponding to $(i, j, k)$ has the basis vector $b(k)$ in the $(i,j)$-th entry and zeros elsewhere. This is obtained by first constructing the product basis for the space of functions $m \times n \to M$ (using `Pi.basis`), reindexing via appropriate equivalences, and then mapping through the linear equivalence that identifies such functions with matrices.

Basis.matrix_apply theorem

 (b : Basis ι R M) (i : m) (j : n) (k : ι) [DecidableEq m] [DecidableEq n] :
  b.matrix m n (i, j, k) = Matrix.stdBasisMatrix i j (b k)

Full source

@[simp]
theorem matrix_apply (b : Basis ι R M) (i : m) (j : n) (k : ι) [DecidableEq m] [DecidableEq n] :
    b.matrix m n (i, j, k) = Matrix.stdBasisMatrix i j (b k) := by
  simp [Basis.matrix, Matrix.stdBasisMatrix_eq_of_single_single]

Explicit Form of Matrix Basis Vectors: $b.\text{matrix}\, (i,j,k) = \text{stdBasisMatrix}\, i\, j\, (b(k))$

Informal description

Let $b$ be a basis for an $R$-module $M$ indexed by $\iota$. For any indices $i \in m$, $j \in n$, and $k \in \iota$, the $(i,j,k)$-th basis vector in the standard basis for $\text{Matrix}_{m \times n}(M)$ is equal to the matrix with $b(k)$ in the $(i,j)$-th entry and zeros elsewhere. That is, $$b.\text{matrix}\, m\, n\, (i, j, k) = \text{stdBasisMatrix}\, i\, j\, (b(k)).$$

Matrix.stdBasis definition

: Basis (m × n) R (Matrix m n R)

Full source

/-- The standard basis of `Matrix m n R`. -/
noncomputable def stdBasis : Basis (m × n) R (Matrix m n R) :=
  Basis.reindex (Pi.basis fun _ : m => Pi.basisFun R n) (Equiv.sigmaEquivProd _ _)
    |>.map (ofLinearEquiv R)

Standard basis of matrices over $R$

Informal description

The standard basis of the space of $m \times n$ matrices over a ring $R$, where the basis vectors are the matrices with a single entry equal to $1$ at position $(i,j)$ and $0$ elsewhere, for each pair $(i,j) \in m \times n$.

Matrix.stdBasis_eq_stdBasisMatrix theorem

(i : m) (j : n) [DecidableEq m] [DecidableEq n] : stdBasis R m n (i, j) = stdBasisMatrix i j (1 : R)

Full source

theorem stdBasis_eq_stdBasisMatrix (i : m) (j : n) [DecidableEq m] [DecidableEq n] :
    stdBasis R m n (i, j) = stdBasisMatrix i j (1 : R) := by
  simp [stdBasis, stdBasisMatrix_eq_of_single_single]

Standard Basis Matrix Equals Elementary Matrix with Unit Entry

Informal description

For any indices $i \in m$ and $j \in n$ in a ring $R$, the standard basis matrix $\text{stdBasis}(R, m, n)(i, j)$ is equal to the matrix $\text{stdBasisMatrix}(i, j, 1)$, where $\text{stdBasisMatrix}(i, j, 1)$ is the matrix with a $1$ in the $(i,j)$-th entry and $0$ elsewhere.

Module.Free.matrix instance

{m n : Type*} [Finite m] [Finite n] : Module.Free R (Matrix m n M)

Full source

/-- The module of finite matrices is free. -/
instance matrix {m n : Type*} [Finite m] [Finite n] : Module.Free R (Matrix m n M) :=
  Module.Free.pi R _

Freeness of Matrix Modules over Finite Index Sets

Informal description

For finite types $m$ and $n$ and a free $R$-module $M$, the module of matrices $\text{Matrix}(m, n, M)$ is also free over $R$.

Main results