Mathlib.LinearAlgebra.Matrix.ToLin

Matrix.vecMulLinear definition

[Fintype m] (M : Matrix m n R) : (m → R) →ₗ[R] n → R

Full source

/-- `Matrix.vecMul M` is a linear map. -/
def Matrix.vecMulLinear [Fintype m] (M : Matrix m n R) : (m → R) →ₗ[R] n → R where
  toFun x := x ᵥ* M
  map_add' _ _ := funext fun _ ↦ add_dotProduct _ _ _
  map_smul' _ _ := funext fun _ ↦ smul_dotProduct _ _ _

Linear map of vector-matrix multiplication

Informal description

Given a commutative ring $ R $ and a matrix $ M $ of size $ m \times n $ with entries in $ R $, the function `Matrix.vecMulLinear` maps a vector $ x $ of size $ m $ to the vector-matrix product $ x \cdot M $, which is a vector of size $ n $. This function is linear in $ x $.

Matrix.vecMulLinear_apply theorem

[Fintype m] (M : Matrix m n R) (x : m → R) : M.vecMulLinear x = x ᵥ* M

Full source

@[simp] theorem Matrix.vecMulLinear_apply [Fintype m] (M : Matrix m n R) (x : m → R) :
    M.vecMulLinear x = x ᵥ* M := rfl

Vector-matrix multiplication as linear map application

Informal description

For any commutative ring $R$, finite type $m$, and matrix $M \in \mathrm{Mat}_{m \times n}(R)$, the linear map $\mathrm{vecMulLinear}_M$ satisfies $\mathrm{vecMulLinear}_M(x) = x \cdot M$ for all vectors $x \in R^m$, where $\cdot$ denotes vector-matrix multiplication.

Matrix.coe_vecMulLinear theorem

[Fintype m] (M : Matrix m n R) : (M.vecMulLinear : _ → _) = M.vecMul

Full source

theorem Matrix.coe_vecMulLinear [Fintype m] (M : Matrix m n R) :
    (M.vecMulLinear : _ → _) = M.vecMul := rfl

Coefficient function of vector-matrix multiplication linear map equals vector-matrix multiplication

Informal description

For any commutative ring $R$ and any $m \times n$ matrix $M$ with entries in $R$, the underlying function of the linear map `M.vecMulLinear` is equal to the vector-matrix multiplication operation `M.vecMul`. That is, for any vector $x \in R^m$, we have $M.vecMulLinear(x) = x \cdot M$.

range_vecMulLinear theorem

(M : Matrix m n R) : LinearMap.range M.vecMulLinear = span R (range M.row)

Full source

theorem range_vecMulLinear (M : Matrix m n R) :
    LinearMap.range M.vecMulLinear = span R (range M.row) := by
  letI := Classical.decEq m
  simp_rw [range_eq_map, ← iSup_range_single, Submodule.map_iSup, range_eq_map, ←
    Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
    Matrix.vecMulLinear_apply, iSup_span, range_eq_iUnion, iUnion_singleton_eq_range,
    LinearMap.single, LinearMap.coe_mk, AddHom.coe_mk, row_def]
  unfold vecMul
  simp_rw [single_dotProduct, one_mul]

Range of Vector-Matrix Multiplication Equals Span of Rows

Informal description

For any commutative ring $R$ and any $m \times n$ matrix $M$ with entries in $R$, the range of the linear map $x \mapsto x \cdot M$ is equal to the $R$-linear span of the rows of $M$.

Matrix.vecMul_injective_iff theorem

{R : Type*} [Ring R] {M : Matrix m n R} : Function.Injective M.vecMul ↔ LinearIndependent R M.row

Full source

theorem Matrix.vecMul_injective_iff {R : Type*} [Ring R] {M : Matrix m n R} :
    Function.InjectiveFunction.Injective M.vecMul ↔ LinearIndependent R M.row := by
  rw [← coe_vecMulLinear]
  simp only [← LinearMap.ker_eq_bot, Fintype.linearIndependent_iff, Submodule.eq_bot_iff,
    LinearMap.mem_ker, vecMulLinear_apply, row_def]
  refine ⟨fun h c h0 ↦ congr_fun <| h c ?_, fun h c h0 ↦ funext <| h c ?_⟩
  · rw [← h0]
    ext i
    simp [vecMul, dotProduct]
  · rw [← h0]
    ext j
    simp [vecMul, dotProduct]

Injectivity of Vector-Matrix Multiplication Equals Linear Independence of Rows

Informal description

For any commutative ring $R$ and any $m \times n$ matrix $M$ with entries in $R$, the vector-matrix multiplication map $x \mapsto x \cdot M$ is injective if and only if the rows of $M$ are linearly independent over $R$.

Matrix.linearIndependent_rows_of_isUnit theorem

{R : Type*} [Ring R] {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) : LinearIndependent R A.row

Full source

lemma Matrix.linearIndependent_rows_of_isUnit {R : Type*} [Ring R] {A : Matrix m m R}
    [DecidableEq m] (ha : IsUnit A) : LinearIndependent R A.row := by
  rw [← Matrix.vecMul_injective_iff]
  exact Matrix.vecMul_injective_of_isUnit ha

Rows of Invertible Matrix are Linearly Independent

Informal description

For any commutative ring $R$ and any $m \times m$ matrix $A$ over $R$, if $A$ is invertible (i.e., $A$ is a unit in the ring of matrices), then the rows of $A$ are linearly independent over $R$.

LinearMap.toMatrixRight' definition

: ((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ] Matrix m n R

Full source

/-- Linear maps `(m → R) →ₗ[R] (n → R)` are linearly equivalent over `Rᵐᵒᵖ` to `Matrix m n R`,
by having matrices act by right multiplication.
-/
def LinearMap.toMatrixRight' : ((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ] Matrix m n R where
  toFun f i j := f (single R (fun _ ↦ R) i 1) j
  invFun := Matrix.vecMulLinear
  right_inv M := by
    ext i j
    simp
  left_inv f := by
    apply (Pi.basisFun R m).ext
    intro j; ext i
    simp
  map_add' f g := by
    ext i j
    simp only [Pi.add_apply, LinearMap.add_apply, Matrix.add_apply]
  map_smul' c f := by
    ext i j
    simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, Matrix.smul_apply]

Linear equivalence between linear maps and matrices via right multiplication

Informal description

The linear equivalence between the space of linear maps from $(m \to R)$ to $(n \to R)$ and the space of $m \times n$ matrices over $R$, where matrices act by right multiplication on vectors. Specifically, given a linear map $f : (m \to R) \to (n \to R)$, the corresponding matrix $M$ is defined by $M_{ij} = f(e_i)_j$, where $e_i$ is the $i$-th standard basis vector. The inverse operation constructs a linear map from a matrix by right multiplication.

Matrix.toLinearMapRight' abbrev

[DecidableEq m] : Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] n → R

Full source

/-- 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. -/
abbrev Matrix.toLinearMapRight' [DecidableEq m] : MatrixMatrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] n → R :=
  LinearEquiv.symm LinearMap.toMatrixRight'

Linear equivalence between matrices and linear maps via right multiplication

Informal description

Given a commutative ring $R$ and finite types $m$ and $n$, there exists a linear equivalence (over $R^\text{op}$) between the space of $m \times n$ matrices over $R$ and the space of linear maps from $(m \to R)$ to $(n \to R)$. This equivalence is constructed by having matrices act via right multiplication on vectors.

Matrix.toLinearMapRight'_apply theorem

(M : Matrix m n R) (v : m → R) : (Matrix.toLinearMapRight') M v = v ᵥ* M

Full source

@[simp]
theorem Matrix.toLinearMapRight'_apply (M : Matrix m n R) (v : m → R) :
    (Matrix.toLinearMapRight') M v = v ᵥ* M := rfl

Right matrix action as vector-matrix multiplication

Informal description

For any $m \times n$ matrix $M$ over a commutative ring $R$ and any vector $v \in m \to R$, the linear map associated to $M$ via right multiplication acts on $v$ as the vector-matrix product $v \cdot M$.

Matrix.toLinearMapRight'_mul theorem

 [Fintype l] [DecidableEq l] (M : Matrix l m R) (N : Matrix m n R) :
  Matrix.toLinearMapRight' (M * N) = (Matrix.toLinearMapRight' N).comp (Matrix.toLinearMapRight' M)

Full source

@[simp]
theorem Matrix.toLinearMapRight'_mul [Fintype l] [DecidableEq l] (M : Matrix l m R)
    (N : Matrix m n R) :
    Matrix.toLinearMapRight' (M * N) =
      (Matrix.toLinearMapRight' N).comp (Matrix.toLinearMapRight' M) :=
  LinearMap.ext fun _x ↦ (vecMul_vecMul _ M N).symm

Composition of Linear Maps Corresponds to Matrix Multiplication under Right Action

Informal description

Let $R$ be a commutative ring, and let $l$, $m$, and $n$ be finite types. For any matrices $M \in \text{Matrix}(l, m, R)$ and $N \in \text{Matrix}(m, n, R)$, the linear map associated with the matrix product $MN$ via right multiplication is equal to the composition of the linear maps associated with $N$ and $M$: $$\text{toLinearMapRight'}(MN) = \text{toLinearMapRight'}(N) \circ \text{toLinearMapRight'}(M).$$

Matrix.toLinearMapRight'_mul_apply theorem

 [Fintype l] [DecidableEq l] (M : Matrix l m R) (N : Matrix m n R) (x) :
  Matrix.toLinearMapRight' (M * N) x = Matrix.toLinearMapRight' N (Matrix.toLinearMapRight' M x)

Full source

theorem Matrix.toLinearMapRight'_mul_apply [Fintype l] [DecidableEq l] (M : Matrix l m R)
    (N : Matrix m n R) (x) :
    Matrix.toLinearMapRight' (M * N) x =
      Matrix.toLinearMapRight' N (Matrix.toLinearMapRight' M x) :=
  (vecMul_vecMul _ M N).symm

Right Matrix Multiplication Commutes with Linear Map Composition

Informal description

Let $R$ be a commutative ring, and let $l$, $m$, and $n$ be finite types. For any matrices $M \in \text{Matrix}(l, m, R)$ and $N \in \text{Matrix}(m, n, R)$, and any vector $x \in l \to R$, the linear map associated with the matrix product $MN$ via right multiplication satisfies $$(MN) \cdot_{\text{right}} x = N \cdot_{\text{right}} (M \cdot_{\text{right}} x),$$ where $\cdot_{\text{right}}$ denotes the right action of matrices on vectors.

Matrix.toLinearMapRight'_one theorem

: Matrix.toLinearMapRight' (1 : Matrix m m R) = LinearMap.id

Full source

@[simp]
theorem Matrix.toLinearMapRight'_one :
    Matrix.toLinearMapRight' (1 : Matrix m m R) = LinearMap.id := by
  ext
  simp [Module.End.one_apply]

Identity Matrix Yields Identity Linear Map under Right Multiplication

Informal description

The linear map associated with the identity matrix $1 \in \text{Matrix } m\ m\ R$ via right multiplication is equal to the identity linear map $\text{id} \colon (m \to R) \to (m \to R)$.

Matrix.toLinearEquivRight'OfInv definition

 [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

Full source

/-- 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`. -/
@[simps]
def Matrix.toLinearEquivRight'OfInv [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 :=
  { LinearMap.toMatrixRight'.symm M' with
    toFun := Matrix.toLinearMapRight' M'
    invFun := Matrix.toLinearMapRight' M
    left_inv := fun x ↦ by
      rw [← Matrix.toLinearMapRight'_mul_apply, hM'M, Matrix.toLinearMapRight'_one, id_apply]
    right_inv := fun x ↦ by
      rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply] }

Linear equivalence between tuple spaces via inverse matrix right multiplication

Informal description

Given finite types $m$ and $n$ and a commutative ring $R$, if $M$ is an $m \times n$ matrix and $M'$ is an $n \times m$ matrix such that $M M' = 1$ and $M' M = 1$, then there exists a linear equivalence between the spaces of $n$-tuples and $m$-tuples over $R$. This equivalence is constructed by right multiplication with $M'$ and $M$ respectively, where $M'$ maps $n$-tuples to $m$-tuples and $M$ maps back.

Matrix.mulVecLin definition

[Fintype n] (M : Matrix m n R) : (n → R) →ₗ[R] m → R

Full source

/-- `Matrix.mulVec M` is a linear map. -/
def Matrix.mulVecLin [Fintype n] (M : Matrix m n R) : (n → R) →ₗ[R] m → R where
  toFun := M.mulVec
  map_add' _ _ := funext fun _ ↦ dotProduct_add _ _ _
  map_smul' _ _ := funext fun _ ↦ dotProduct_smul _ _ _

Matrix-vector multiplication as a linear map

Informal description

Given a commutative ring $R$ and finite types $m$ and $n$, for any matrix $M$ in $\text{Matrix } m\ n\ R$, the function $\text{mulVecLin } M$ is the linear map from $n$-tuples of $R$ to $m$-tuples of $R$ defined by matrix-vector multiplication. Specifically, for any vector $v : n \to R$, the result $\text{mulVecLin } M\ v$ equals the matrix-vector product $M \cdot v$.

Matrix.coe_mulVecLin theorem

[Fintype n] (M : Matrix m n R) : (M.mulVecLin : _ → _) = M.mulVec

Full source

theorem Matrix.coe_mulVecLin [Fintype n] (M : Matrix m n R) :
    (M.mulVecLin : _ → _) = M.mulVec := rfl

Coefficient Extraction: $\text{mulVecLin } M$ as Matrix-Vector Multiplication

Informal description

For any commutative ring $R$ and finite types $m$ and $n$, given a matrix $M \in \text{Matrix } m\ n\ R$, the underlying function of the linear map $\text{mulVecLin } M$ is equal to the matrix-vector multiplication function $M \cdot \text{vec}$.

Matrix.mulVecLin_apply theorem

[Fintype n] (M : Matrix m n R) (v : n → R) : M.mulVecLin v = M *ᵥ v

Full source

@[simp]
theorem Matrix.mulVecLin_apply [Fintype n] (M : Matrix m n R) (v : n → R) :
    M.mulVecLin v = M *ᵥ v :=
  rfl

Matrix-Vector Multiplication via Linear Map Application: $\text{mulVecLin}(M)(v) = M \cdot v$

Informal description

For any commutative ring $R$ and finite types $m$ and $n$, given a matrix $M \in \text{Matrix}_{m \times n}(R)$ and a vector $v \in R^n$, the application of the linear map $\text{mulVecLin}(M)$ to $v$ equals the matrix-vector product $M \cdot v$.

Matrix.mulVecLin_zero theorem

[Fintype n] : Matrix.mulVecLin (0 : Matrix m n R) = 0

Full source

@[simp]
theorem Matrix.mulVecLin_zero [Fintype n] : Matrix.mulVecLin (0 : Matrix m n R) = 0 :=
  LinearMap.ext zero_mulVec

Zero matrix yields zero linear map under matrix-vector multiplication

Informal description

For any commutative ring $R$ and finite types $m$ and $n$, the linear map associated with the zero matrix in $\text{Matrix } m\ n\ R$ is the zero linear map from $(n \to R)$ to $(m \to R)$.

Matrix.mulVecLin_add theorem

[Fintype n] (M N : Matrix m n R) : (M + N).mulVecLin = M.mulVecLin + N.mulVecLin

Full source

@[simp]
theorem Matrix.mulVecLin_add [Fintype n] (M N : Matrix m n R) :
    (M + N).mulVecLin = M.mulVecLin + N.mulVecLin :=
  LinearMap.ext fun _ ↦ add_mulVec _ _ _

Additivity of Matrix-Vector Multiplication Linear Map

Informal description

For any commutative ring $R$ and finite types $m$ and $n$, given two matrices $M, N \in \text{Matrix}_{m \times n}(R)$, the linear map associated with their sum equals the sum of their individual linear maps. That is, $(M + N).\text{mulVecLin} = M.\text{mulVecLin} + N.\text{mulVecLin}$.

Matrix.mulVecLin_transpose theorem

[Fintype m] (M : Matrix m n R) : Mᵀ.mulVecLin = M.vecMulLinear

Full source

@[simp] theorem Matrix.mulVecLin_transpose [Fintype m] (M : Matrix m n R) :
    Mᵀ.mulVecLin = M.vecMulLinear := by
  ext; simp [mulVec_transpose]

Transpose Swaps Matrix-Vector and Vector-Matrix Linear Maps

Informal description

For any commutative ring $R$ and finite types $m$ and $n$, given a matrix $M \in \text{Matrix}_{m \times n}(R)$, the linear map associated with matrix-vector multiplication by the transpose matrix $M^\top$ equals the linear map associated with vector-matrix multiplication by $M$. That is, $M^\top.\text{mulVecLin} = M.\text{vecMulLinear}$.

Matrix.vecMulLinear_transpose theorem

[Fintype n] (M : Matrix m n R) : Mᵀ.vecMulLinear = M.mulVecLin

Full source

@[simp] theorem Matrix.vecMulLinear_transpose [Fintype n] (M : Matrix m n R) :
    Mᵀ.vecMulLinear = M.mulVecLin := by
  ext; simp [vecMul_transpose]

Transpose Swaps Vector-Matrix and Matrix-Vector Linear Maps

Informal description

For any commutative ring $R$ and finite types $m$ and $n$, given a matrix $M \in \text{Matrix}_{m \times n}(R)$, the linear map associated with vector-matrix multiplication by the transpose matrix $M^\top$ equals the linear map associated with matrix-vector multiplication by $M$. That is, $M^\top.\text{vecMulLinear} = M.\text{mulVecLin}$.

Matrix.mulVecLin_submatrix theorem

 [Fintype n] [Fintype l] (f₁ : m → k) (e₂ : n ≃ l) (M : Matrix k l R) :
  (M.submatrix f₁ e₂).mulVecLin = funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ funLeft _ _ e₂.symm

Full source

theorem Matrix.mulVecLin_submatrix [Fintype n] [Fintype l] (f₁ : m → k) (e₂ : n ≃ l)
    (M : Matrix k l R) :
    (M.submatrix f₁ e₂).mulVecLin = funLeftfunLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ funLeft _ _ e₂.symm :=
  LinearMap.ext fun _ ↦ submatrix_mulVec_equiv _ _ _ _

Submatrix-Vector Multiplication as Composition of Linear Maps

Informal description

Let $R$ be a commutative ring, and let $k$, $l$, $m$, $n$ be finite types. Given a function $f_1 : m \to k$, an equivalence $e_2 : n \simeq l$, and a matrix $M \in \text{Matrix}_{k \times l}(R)$, the linear map associated with matrix-vector multiplication by the submatrix $M.\text{submatrix } f_1 e_2$ is equal to the composition of three linear maps: 1. The linear map $\text{funLeft } R R f_1$ induced by $f_1$ on the left, 2. The linear map $M.\text{mulVecLin}$ associated with $M$, 3. The linear map $\text{funLeft } R R e_2^{-1}$ induced by the inverse of $e_2$ on the right. In other words, $(M.\text{submatrix } f_1 e_2).\text{mulVecLin} = \text{funLeft } R R f_1 \circ M.\text{mulVecLin} \circ \text{funLeft } R R e_2^{-1}$.

Matrix.mulVecLin_reindex theorem

 [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₂)

Full source

/-- A variant of `Matrix.mulVecLin_submatrix` that keeps around `LinearEquiv`s. -/
theorem Matrix.mulVecLin_reindex [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₂) :=
  Matrix.mulVecLin_submatrix _ _ _

Reindexed Matrix-Vector Multiplication as Composition of Linear Equivalences

Informal description

Let $R$ be a commutative ring, and let $k$, $l$, $m$, and $n$ be finite types. Given equivalences $e_1 : k \simeq m$ and $e_2 : l \simeq n$, and a matrix $M \in \text{Matrix}_{k \times l}(R)$, the linear map associated with matrix-vector multiplication by the reindexed matrix $\text{reindex } e_1 e_2 M$ is equal to the composition of the following three linear maps: 1. The linear equivalence $\text{funCongrLeft } R R e_1^{-1}$ induced by the inverse of $e_1$ on the left, 2. The linear map $M.\text{mulVecLin}$ associated with $M$, 3. The linear equivalence $\text{funCongrLeft } R R e_2$ induced by $e_2$ on the right. In other words, \[ (\text{reindex } e_1 e_2 M).\text{mulVecLin} = \text{funCongrLeft } R R e_1^{-1} \circ M.\text{mulVecLin} \circ \text{funCongrLeft } R R e_2. \]

Matrix.mulVecLin_one theorem

[DecidableEq n] : Matrix.mulVecLin (1 : Matrix n n R) = LinearMap.id

Full source

@[simp]
theorem Matrix.mulVecLin_one [DecidableEq n] :
    Matrix.mulVecLin (1 : Matrix n n R) = LinearMap.id := by
  ext; simp [Matrix.one_apply, Pi.single_apply, eq_comm]

Identity Matrix Acts as Identity Linear Map via Matrix-Vector Multiplication

Informal description

For any finite type $n$ with decidable equality and any commutative ring $R$, the linear map associated with matrix-vector multiplication by the identity matrix $1 \in \text{Matrix}_{n \times n}(R)$ is equal to the identity linear map $\text{id} \colon (n \to R) \to (n \to R)$.

Matrix.mulVecLin_mul theorem

 [Fintype m] (M : Matrix l m R) (N : Matrix m n R) :
  Matrix.mulVecLin (M * N) = (Matrix.mulVecLin M).comp (Matrix.mulVecLin N)

Full source

@[simp]
theorem Matrix.mulVecLin_mul [Fintype m] (M : Matrix l m R) (N : Matrix m n R) :
    Matrix.mulVecLin (M * N) = (Matrix.mulVecLin M).comp (Matrix.mulVecLin N) :=
  LinearMap.ext fun _ ↦ (mulVec_mulVec _ _ _).symm

Composition of Matrix-Vector Multiplication Linear Maps

Informal description

Let $R$ be a commutative ring, and let $l$, $m$, and $n$ be finite types. For any matrices $M \in \text{Matrix } l\ m\ R$ and $N \in \text{Matrix } m\ n\ R$, the linear map associated with the matrix product $M \cdot N$ is equal to the composition of the linear maps associated with $M$ and $N$, i.e., \[ \text{mulVecLin}(M \cdot N) = \text{mulVecLin}(M) \circ \text{mulVecLin}(N). \]

Matrix.ker_mulVecLin_eq_bot_iff theorem

{M : Matrix m n R} : (LinearMap.ker M.mulVecLin) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0

Full source

theorem Matrix.ker_mulVecLin_eq_bot_iff {M : Matrix m n R} :
    (LinearMap.ker M.mulVecLin) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0 := by
  simp only [Submodule.eq_bot_iff, LinearMap.mem_ker, Matrix.mulVecLin_apply]

Matrix-Vector Multiplication Has Trivial Kernel if and only if Injective on Vectors

Informal description

For any matrix $M \in \text{Matrix}_{m \times n}(R)$ over a commutative ring $R$, the kernel of the linear map induced by matrix-vector multiplication is trivial if and only if the only solution to $M \cdot v = 0$ is the zero vector $v = 0$. In other words, \[ \text{ker}(M \cdot \text{vec}) = \{0\} \iff \forall v \in R^n, M \cdot v = 0 \implies v = 0. \]

Matrix.range_mulVecLin theorem

(M : Matrix m n R) : LinearMap.range M.mulVecLin = span R (range M.col)

Full source

theorem Matrix.range_mulVecLin (M : Matrix m n R) :
    LinearMap.range M.mulVecLin = span R (range M.col) := by
  rw [← vecMulLinear_transpose, range_vecMulLinear, row_transpose]

Range of Matrix-Vector Multiplication Equals Span of Columns

Informal description

For any matrix $M \in \text{Matrix}_{m \times n}(R)$ over a commutative ring $R$, the range of the linear map $v \mapsto M \cdot v$ is equal to the $R$-linear span of the columns of $M$. That is, \[ \text{range}(M \cdot \text{vec}) = \text{span}_R \{\text{col}_1(M), \dots, \text{col}_n(M)\}. \]

Matrix.mulVec_injective_iff theorem

{R : Type*} [CommRing R] {M : Matrix m n R} : Function.Injective M.mulVec ↔ LinearIndependent R M.col

Full source

theorem Matrix.mulVec_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R} :
    Function.InjectiveFunction.Injective M.mulVec ↔ LinearIndependent R M.col := by
  change Function.InjectiveFunction.Injective (fun x ↦ _) ↔ _
  simp_rw [← M.vecMul_transpose, vecMul_injective_iff, row_transpose]

Injectivity of Matrix-Vector Multiplication Equals Linear Independence of Columns

Informal description

Let $R$ be a commutative ring and $M$ be an $m \times n$ matrix with entries in $R$. The function $M \cdot \text{vec}$ (matrix-vector multiplication) is injective if and only if the columns of $M$ are linearly independent over $R$.

Matrix.linearIndependent_cols_of_isUnit theorem

{R : Type*} [CommRing R] [Fintype m] {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) : LinearIndependent R A.col

Full source

lemma Matrix.linearIndependent_cols_of_isUnit {R : Type*} [CommRing R] [Fintype m]
    {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) :
    LinearIndependent R A.col := by
  rw [← Matrix.mulVec_injective_iff]
  exact Matrix.mulVec_injective_of_isUnit ha

Linear Independence of Columns of an Invertible Matrix

Informal description

Let $R$ be a commutative ring and let $A$ be an $m \times m$ matrix with entries in $R$. If $A$ is invertible (i.e., $A$ is a unit in the ring of matrices), then the columns of $A$ are linearly independent over $R$.

LinearMap.toMatrix' definition

: ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R

Full source

/-- Linear maps `(n → R) →ₗ[R] (m → R)` are linearly equivalent to `Matrix m n R`. -/
def LinearMap.toMatrix' : ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R where
  toFun f := of fun i j ↦ f (Pi.single j 1) i
  invFun := Matrix.mulVecLin
  right_inv M := by
    ext i j
    simp only [Matrix.mulVec_single_one, Matrix.mulVecLin_apply, of_apply, transpose_apply]
  left_inv f := by
    apply (Pi.basisFun R n).ext
    intro j; ext i
    simp only [Pi.basisFun_apply, Matrix.mulVec_single_one,
      Matrix.mulVecLin_apply, of_apply, transpose_apply]
  map_add' f g := by
    ext i j
    simp only [Pi.add_apply, LinearMap.add_apply, of_apply, Matrix.add_apply]
  map_smul' c f := by
    ext i j
    simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, of_apply, Matrix.smul_apply]

Linear map to matrix equivalence

Informal description

The linear equivalence between linear maps from $(n \to R)$ to $(m \to R)$ and $m \times n$ matrices over a commutative ring $R$. Specifically, given a linear map $f : (n \to R) \to (m \to R)$, the corresponding matrix $M$ is defined by $M_{ij} = f(\text{Pi.single}_j(1))_i$, where $\text{Pi.single}_j(1)$ is the vector with $1$ in the $j$-th position and $0$ elsewhere. Conversely, given a matrix $M$, the corresponding linear map is the matrix-vector multiplication map $M \cdot \text{vec}$.

Matrix.toLin' definition

: Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R

Full source

/-- 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`. -/
def Matrix.toLin' : MatrixMatrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R :=
  LinearMap.toMatrix'.symm

Matrix to linear map equivalence

Informal description

The linear equivalence between $m \times n$ matrices over a commutative ring $R$ and linear maps from $(n \to R)$ to $(m \to R)$. Specifically, given a matrix $M$, the corresponding linear map is the matrix-vector multiplication map $v \mapsto M \cdot v$. Conversely, given a linear map $f$, the corresponding matrix is defined by $M_{ij} = f(e_j)_i$ where $e_j$ is the $j$-th standard basis vector.

Matrix.toLin'_apply' theorem

(M : Matrix m n R) : Matrix.toLin' M = M.mulVecLin

Full source

theorem Matrix.toLin'_apply' (M : Matrix m n R) : Matrix.toLin' M = M.mulVecLin :=
  rfl

Matrix-to-Linear-Map Equivalence Preserves Multiplication Action

Informal description

For any $m \times n$ matrix $M$ over a commutative ring $R$, the linear map $\text{Matrix.toLin'}(M)$ is equal to the matrix-vector multiplication map $M \cdot \text{vec}$.

LinearMap.toMatrix'_symm theorem

: (LinearMap.toMatrix'.symm : Matrix m n R ≃ₗ[R] _) = Matrix.toLin'

Full source

@[simp]
theorem LinearMap.toMatrix'_symm :
    (LinearMap.toMatrix'.symm : MatrixMatrix m n R ≃ₗ[R] _) = Matrix.toLin' :=
  rfl

Inverse of Linear Map to Matrix Equivalence is Matrix to Linear Map Equivalence

Informal description

The inverse of the linear equivalence `LinearMap.toMatrix'` is equal to the linear equivalence `Matrix.toLin'`. That is, the map that converts a matrix $M$ over a commutative ring $R$ to its corresponding linear map $(n \to R) \to (m \to R)$ is the inverse of the map that converts a linear map to its corresponding matrix.

Matrix.toLin'_symm theorem

: (Matrix.toLin'.symm : ((n → R) →ₗ[R] m → R) ≃ₗ[R] _) = LinearMap.toMatrix'

Full source

@[simp]
theorem Matrix.toLin'_symm :
    (Matrix.toLin'.symm : ((n → R) →ₗ[R] m → R) ≃ₗ[R] _) = LinearMap.toMatrix' :=
  rfl

Inverse of Matrix-to-Linear-Map Equivalence is Linear-Map-to-Matrix Equivalence

Informal description

The inverse of the linear equivalence `Matrix.toLin'` from $m \times n$ matrices over a commutative ring $R$ to linear maps $(n \to R) \to (m \to R)$ is equal to the linear equivalence `LinearMap.toMatrix'`.

LinearMap.toMatrix'_toLin' theorem

(M : Matrix m n R) : LinearMap.toMatrix' (Matrix.toLin' M) = M

Full source

@[simp]
theorem LinearMap.toMatrix'_toLin' (M : Matrix m n R) : LinearMap.toMatrix' (Matrix.toLin' M) = M :=
  LinearMap.toMatrix'.apply_symm_apply M

Matrix identity: $\text{toMatrix'} \circ \text{toLin'} = \text{id}$

Informal description

For any $m \times n$ matrix $M$ over a commutative ring $R$, the composition of the linear equivalences `Matrix.toLin'` and `LinearMap.toMatrix'` maps $M$ to itself. In other words, converting $M$ to a linear map and then back to a matrix yields the original matrix $M$.

Matrix.toLin'_toMatrix' theorem

(f : (n → R) →ₗ[R] m → R) : Matrix.toLin' (LinearMap.toMatrix' f) = f

Full source

@[simp]
theorem Matrix.toLin'_toMatrix' (f : (n → R) →ₗ[R] m → R) :
    Matrix.toLin' (LinearMap.toMatrix' f) = f :=
  Matrix.toLin'.apply_symm_apply f

Matrix-Linear Map Roundtrip Identity: $\text{toLin}' \circ \text{toMatrix}' = \text{id}$

Informal description

For any linear map $f \colon (n \to R) \to (m \to R)$ over a commutative ring $R$, the composition of the matrix-to-linear-map equivalence followed by the linear-map-to-matrix equivalence returns the original linear map. That is, if we first convert $f$ to its matrix representation $M$ via `LinearMap.toMatrix'` and then convert $M$ back to a linear map via `Matrix.toLin'`, we recover $f$.

LinearMap.toMatrix'_apply theorem

(f : (n → R) →ₗ[R] m → R) (i j) : LinearMap.toMatrix' f i j = f (fun j' ↦ if j' = j then 1 else 0) i

Full source

@[simp]
theorem LinearMap.toMatrix'_apply (f : (n → R) →ₗ[R] m → R) (i j) :
    LinearMap.toMatrix' f i j = f (fun j' ↦ if j' = j then 1 else 0) i := by
  simp only [LinearMap.toMatrix', LinearEquiv.coe_mk, of_apply]
  congr! with i
  split_ifs with h
  · rw [h, Pi.single_eq_same]
  apply Pi.single_eq_of_ne h

Matrix Entry Formula for Linear Maps on Standard Basis

Informal description

For any linear map $f \colon (n \to R) \to (m \to R)$ over a commutative ring $R$, and for any indices $i$ and $j$, the $(i,j)$-th entry of the matrix associated to $f$ via `LinearMap.toMatrix'` is given by $f(e_j)_i$, where $e_j$ is the standard basis vector with $1$ in the $j$-th position and $0$ elsewhere. In other words, $\text{LinearMap.toMatrix'}(f)_{i,j} = f(\delta_j)_i$, where $\delta_j(k) = 1$ if $k = j$ and $0$ otherwise.

Matrix.toLin'_apply theorem

(M : Matrix m n R) (v : n → R) : Matrix.toLin' M v = M *ᵥ v

Full source

@[simp]
theorem Matrix.toLin'_apply (M : Matrix m n R) (v : n → R) : Matrix.toLin' M v = M *ᵥ v :=
  rfl

Matrix-to-Linear-Map Action via Matrix-Vector Multiplication

Informal description

For any $m \times n$ matrix $M$ over a commutative ring $R$ and any vector $v \in R^n$, the linear map associated to $M$ via `Matrix.toLin'` acts on $v$ by matrix-vector multiplication, i.e., $\text{Matrix.toLin'}(M)(v) = M \cdot v$.

Matrix.toLin'_one theorem

: Matrix.toLin' (1 : Matrix n n R) = LinearMap.id

Full source

@[simp]
theorem Matrix.toLin'_one : Matrix.toLin' (1 : Matrix n n R) = LinearMap.id :=
  Matrix.mulVecLin_one

Identity Matrix Yields Identity Linear Map via `Matrix.toLin'`

Informal description

For any finite type $n$ and commutative ring $R$, the linear map associated to the identity matrix $1 \in \text{Matrix}_{n \times n}(R)$ via `Matrix.toLin'` is equal to the identity linear map $\text{id} \colon (n \to R) \to (n \to R)$.

LinearMap.toMatrix'_id theorem

: LinearMap.toMatrix' (LinearMap.id : (n → R) →ₗ[R] n → R) = 1

Full source

@[simp]
theorem LinearMap.toMatrix'_id : LinearMap.toMatrix' (LinearMap.id : (n → R) →ₗ[R] n → R) = 1 := by
  ext
  rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_apply]

Identity Linear Map Corresponds to Identity Matrix

Informal description

The matrix representation of the identity linear map $\text{id} \colon (n \to R) \to (n \to R)$ over a commutative ring $R$ is the identity matrix $1 \in \text{Matrix } n n R$.

LinearMap.toMatrix'_one theorem

: LinearMap.toMatrix' (1 : (n → R) →ₗ[R] n → R) = 1

Full source

@[simp]
theorem LinearMap.toMatrix'_one : LinearMap.toMatrix' (1 : (n → R) →ₗ[R] n → R) = 1 :=
  LinearMap.toMatrix'_id

Identity Endomorphism Corresponds to Identity Matrix

Informal description

The matrix representation of the identity endomorphism $1 \colon (n \to R) \to (n \to R)$ over a commutative ring $R$ is the identity matrix $1 \in \text{Matrix}_{n \times n}(R)$.

Matrix.toLin'_mul theorem

 [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) :
  Matrix.toLin' (M * N) = (Matrix.toLin' M).comp (Matrix.toLin' N)

Full source

@[simp]
theorem Matrix.toLin'_mul [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) :
    Matrix.toLin' (M * N) = (Matrix.toLin' M).comp (Matrix.toLin' N) :=
  Matrix.mulVecLin_mul _ _

Composition of Linear Maps Corresponds to Matrix Multiplication

Informal description

Let $R$ be a commutative ring, and let $l$, $m$, and $n$ be finite types. For any matrices $M \in \text{Matrix}(l, m, R)$ and $N \in \text{Matrix}(m, n, R)$, the linear map associated with the matrix product $M \cdot N$ is equal to the composition of the linear maps associated with $M$ and $N$, i.e., \[ \text{toLin'}(M \cdot N) = \text{toLin'}(M) \circ \text{toLin'}(N). \]

Matrix.toLin'_submatrix theorem

 [Fintype l] [DecidableEq l] (f₁ : m → k) (e₂ : n ≃ l) (M : Matrix k l R) :
  Matrix.toLin' (M.submatrix f₁ e₂) = funLeft R R f₁ ∘ₗ (Matrix.toLin' M) ∘ₗ funLeft _ _ e₂.symm

Full source

@[simp]
theorem Matrix.toLin'_submatrix [Fintype l] [DecidableEq l] (f₁ : m → k) (e₂ : n ≃ l)
    (M : Matrix k l R) :
    Matrix.toLin' (M.submatrix f₁ e₂) =
      funLeftfunLeft R R f₁ ∘ₗ (Matrix.toLin' M) ∘ₗ funLeft _ _ e₂.symm :=
  Matrix.mulVecLin_submatrix _ _ _

Submatrix-to-linear-map composition identity

Informal description

Let $R$ be a commutative ring, and let $k$, $l$, $m$, $n$ be finite types with $l$ having decidable equality. Given a function $f_1 : m \to k$, an equivalence $e_2 : n \simeq l$, and a matrix $M \in \text{Matrix}_{k \times l}(R)$, the linear map associated with the submatrix $M_{\text{submatrix } f_1 e_2}$ is equal to the composition of: 1. The linear map $\text{funLeft}_{R R} f_1$ induced by $f_1$ on the left, 2. The linear map $\text{Matrix.toLin' } M$ associated with $M$, 3. The linear map $\text{funLeft}_{R R} e_2^{-1}$ induced by the inverse of $e_2$ on the right. In other words, we have: \[ \text{Matrix.toLin' } (M_{\text{submatrix } f_1 e_2}) = \text{funLeft}_{R R} f_1 \circ \text{Matrix.toLin' } M \circ \text{funLeft}_{R R} e_2^{-1}. \]

Matrix.toLin'_reindex theorem

 [Fintype l] [DecidableEq l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R) :
  Matrix.toLin' (reindex e₁ e₂ M) =
    ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ (Matrix.toLin' M) ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)

Full source

/-- A variant of `Matrix.toLin'_submatrix` that keeps around `LinearEquiv`s. -/
theorem Matrix.toLin'_reindex [Fintype l] [DecidableEq l] (e₁ : k ≃ m) (e₂ : l ≃ n)
    (M : Matrix k l R) :
    Matrix.toLin' (reindex e₁ e₂ M) =
      ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ (Matrix.toLin' M) ∘ₗ
        ↑(LinearEquiv.funCongrLeft R R e₂) :=
  Matrix.mulVecLin_reindex _ _ _

Reindexed Matrix-to-Linear-Map Composition Identity

Informal description

Let $R$ be a commutative ring, and let $k$, $l$, $m$, $n$ be finite types with $l$ having decidable equality. Given equivalences $e_1 : k \simeq m$ and $e_2 : l \simeq n$, and a matrix $M \in \text{Matrix}_{k \times l}(R)$, the linear map associated with the reindexed matrix $\text{reindex } e_1 e_2 M$ is equal to the composition of: 1. The linear equivalence $\text{funCongrLeft } R R e_1^{-1}$ induced by the inverse of $e_1$ on the left, 2. The linear map $\text{Matrix.toLin' } M$ associated with $M$, 3. The linear equivalence $\text{funCongrLeft } R R e_2$ induced by $e_2$ on the right. In other words, we have: \[ \text{Matrix.toLin' } (\text{reindex } e_1 e_2 M) = \text{funCongrLeft } R R e_1^{-1} \circ \text{Matrix.toLin' } M \circ \text{funCongrLeft } R R e_2. \]

Matrix.toLin'_mul_apply theorem

 [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R) (x) :
  Matrix.toLin' (M * N) x = Matrix.toLin' M (Matrix.toLin' N x)

Full source

/-- Shortcut lemma for `Matrix.toLin'_mul` and `LinearMap.comp_apply` -/
theorem Matrix.toLin'_mul_apply [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R)
    (x) : Matrix.toLin' (M * N) x = Matrix.toLin' M (Matrix.toLin' N x) := by
  rw [Matrix.toLin'_mul, LinearMap.comp_apply]

Matrix Product Action Equals Composition of Actions: $\text{toLin'}(M \cdot N)(x) = \text{toLin'}(M)(\text{toLin'}(N)(x))$

Informal description

Let $R$ be a commutative ring, and let $l$, $m$, and $n$ be finite types with $m$ having decidable equality. For any matrices $M \in \text{Matrix}(l, m, R)$ and $N \in \text{Matrix}(m, n, R)$, and any vector $x \in n \to R$, the action of the matrix product $M \cdot N$ on $x$ equals the action of $M$ on the result of $N$ acting on $x$, i.e., \[ \text{toLin'}(M \cdot N)(x) = \text{toLin'}(M)(\text{toLin'}(N)(x)). \]

LinearMap.toMatrix'_comp theorem

 [Fintype l] [DecidableEq l] (f : (n → R) →ₗ[R] m → R) (g : (l → R) →ₗ[R] n → R) :
  LinearMap.toMatrix' (f.comp g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g

Full source

theorem LinearMap.toMatrix'_comp [Fintype l] [DecidableEq l] (f : (n → R) →ₗ[R] m → R)
    (g : (l → R) →ₗ[R] n → R) :
    LinearMap.toMatrix' (f.comp g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g := by
  suffices f.comp g = Matrix.toLin' (LinearMap.toMatrix' f * LinearMap.toMatrix' g) by
    rw [this, LinearMap.toMatrix'_toLin']
  rw [Matrix.toLin'_mul, Matrix.toLin'_toMatrix', Matrix.toLin'_toMatrix']

Matrix Representation of Linear Map Composition: $\text{toMatrix'}(f \circ g) = \text{toMatrix'}(f) \cdot \text{toMatrix'}(g)$

Informal description

Let $R$ be a commutative ring, and let $l$, $m$, and $n$ be finite types. For any linear maps $f \colon (n \to R) \to (m \to R)$ and $g \colon (l \to R) \to (n \to R)$, the matrix representation of the composition $f \circ g$ is equal to the product of the matrix representations of $f$ and $g$, i.e., \[ \text{toMatrix'}(f \circ g) = \text{toMatrix'}(f) \cdot \text{toMatrix'}(g). \]

LinearMap.toMatrix'_mul theorem

 [Fintype m] [DecidableEq m] (f g : (m → R) →ₗ[R] m → R) :
  LinearMap.toMatrix' (f * g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g

Full source

theorem LinearMap.toMatrix'_mul [Fintype m] [DecidableEq m] (f g : (m → R) →ₗ[R] m → R) :
    LinearMap.toMatrix' (f * g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g :=
  LinearMap.toMatrix'_comp f g

Matrix Representation of Linear Map Composition: $\text{toMatrix'}(f \circ g) = \text{toMatrix'}(f) \cdot \text{toMatrix'}(g)$

Informal description

Let $R$ be a commutative ring and let $m$ be a finite type with decidable equality. For any two linear maps $f, g \colon (m \to R) \to (m \to R)$, the matrix representation of the composition $f \circ g$ is equal to the product of their matrix representations, i.e., \[ \text{toMatrix'}(f \circ g) = \text{toMatrix'}(f) \cdot \text{toMatrix'}(g). \]

LinearMap.toMatrix'_algebraMap theorem

(x : R) : LinearMap.toMatrix' (algebraMap R (Module.End R (n → R)) x) = scalar n x

Full source

@[simp]
theorem LinearMap.toMatrix'_algebraMap (x : R) :
    LinearMap.toMatrix' (algebraMap R (Module.End R (n → R)) x) = scalar n x := by
  simp [Module.algebraMap_end_eq_smul_id, smul_eq_diagonal_mul]

Matrix Representation of Scalar Algebra Homomorphism: $\text{toMatrix'}(\text{algebraMap}(x)) = \text{scalar}_n(x)$

Informal description

For any element $x$ in a commutative ring $R$, the matrix representation of the algebra homomorphism $\text{algebraMap}_R(\text{End}_R(n \to R), x)$ is the scalar matrix $\text{scalar}_n(x)$, where $\text{scalar}_n(x)$ denotes the $n \times n$ diagonal matrix with all diagonal entries equal to $x$.

Matrix.ker_toLin'_eq_bot_iff theorem

{M : Matrix n n R} : LinearMap.ker (Matrix.toLin' M) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0

Full source

theorem Matrix.ker_toLin'_eq_bot_iff {M : Matrix n n R} :
    LinearMap.kerLinearMap.ker (Matrix.toLin' M) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0 :=
  Matrix.ker_mulVecLin_eq_bot_iff

Trivial Kernel of Matrix-Induced Linear Map if and only if Injective on Vectors

Informal description

For any square matrix $M$ of size $n \times n$ over a commutative ring $R$, the kernel of the linear map associated to $M$ is trivial if and only if the only solution to the equation $M \cdot v = 0$ is the zero vector $v = 0$. In other words, \[ \text{ker}(\text{Matrix.toLin' } M) = \{0\} \iff \forall v \in R^n, \, M \cdot v = 0 \implies v = 0. \]

Matrix.range_toLin' theorem

(M : Matrix m n R) : LinearMap.range (Matrix.toLin' M) = span R (range M.col)

Full source

theorem Matrix.range_toLin' (M : Matrix m n R) :
    LinearMap.range (Matrix.toLin' M) = span R (range M.col) :=
  Matrix.range_mulVecLin _

Range of Matrix-Vector Multiplication Equals Span of Columns

Informal description

For any $m \times n$ matrix $M$ over a commutative ring $R$, the range of the linear map associated to $M$ (via matrix-vector multiplication) is equal to the $R$-linear span of the columns of $M$. That is, \[ \text{range}(M \cdot \text{vec}) = \text{span}_R \{\text{col}_1(M), \dots, \text{col}_n(M)\}. \]

Matrix.toLin'OfInv definition

 [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

Full source

/-- 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`. -/
@[simps]
def Matrix.toLin'OfInv [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 :=
  { Matrix.toLin' M' with
    toFun := Matrix.toLin' M'
    invFun := Matrix.toLin' M
    left_inv := fun x ↦ by rw [← Matrix.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
    right_inv := fun x ↦ by
      rw [← Matrix.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply] }

Linear equivalence induced by inverse matrices

Informal description

Given an $m \times n$ matrix $M$ and an $n \times m$ matrix $M'$ over a commutative ring $R$ such that $M M' = I_m$ and $M' M = I_n$, the linear equivalence between the function spaces $m \to R$ and $n \to R$ is defined by the matrix-vector multiplication maps $v \mapsto M' \cdot v$ and $w \mapsto M \cdot w$, which are mutual inverses.

LinearMap.toMatrixAlgEquiv' definition

: ((n → R) →ₗ[R] n → R) ≃ₐ[R] Matrix n n R

Full source

/-- Linear maps `(n → R) →ₗ[R] (n → R)` are algebra equivalent to `Matrix n n R`. -/
def LinearMap.toMatrixAlgEquiv' : ((n → R) →ₗ[R] n → R) ≃ₐ[R] Matrix n n R :=
  AlgEquiv.ofLinearEquiv LinearMap.toMatrix' LinearMap.toMatrix'_one LinearMap.toMatrix'_mul

Algebra equivalence between linear endomorphisms and square matrices

Informal description

The algebra equivalence between the space of linear endomorphisms on $(n \to R)$ and the space of $n \times n$ matrices over a commutative ring $R$. Specifically, it maps a linear map $f \colon (n \to R) \to (n \to R)$ to the matrix $M$ defined by $M_{ij} = f(\text{Pi.single}_j(1))_i$, where $\text{Pi.single}_j(1)$ is the vector with $1$ in the $j$-th position and $0$ elsewhere. This equivalence preserves the multiplicative identity and matrix multiplication, i.e., $\text{toMatrixAlgEquiv'}(1) = 1$ and $\text{toMatrixAlgEquiv'}(f \circ g) = \text{toMatrixAlgEquiv'}(f) \cdot \text{toMatrixAlgEquiv'}(g)$.

Matrix.toLinAlgEquiv' definition

: Matrix n n R ≃ₐ[R] (n → R) →ₗ[R] n → R

Full source

/-- A `Matrix n n R` is algebra equivalent to a linear map `(n → R) →ₗ[R] (n → R)`. -/
def Matrix.toLinAlgEquiv' : MatrixMatrix n n R ≃ₐ[R] (n → R) →ₗ[R] n → R :=
  LinearMap.toMatrixAlgEquiv'.symm

Algebra equivalence from square matrices to linear endomorphisms

Informal description

The algebra equivalence between the space of $n \times n$ matrices over a commutative ring $R$ and the space of linear endomorphisms on $(n \to R)$. Specifically, it maps a matrix $M$ to the linear map $f \colon (n \to R) \to (n \to R)$ defined by $f(v) = M \cdot v$, where $\cdot$ denotes matrix-vector multiplication. This equivalence preserves the multiplicative identity and matrix multiplication, i.e., $\text{toLinAlgEquiv'}(I_n) = \text{id}$ and $\text{toLinAlgEquiv'}(M \cdot N) = \text{toLinAlgEquiv'}(M) \circ \text{toLinAlgEquiv'}(N)$.

LinearMap.toMatrixAlgEquiv'_symm theorem

: (LinearMap.toMatrixAlgEquiv'.symm : Matrix n n R ≃ₐ[R] _) = Matrix.toLinAlgEquiv'

Full source

@[simp]
theorem LinearMap.toMatrixAlgEquiv'_symm :
    (LinearMap.toMatrixAlgEquiv'.symm : MatrixMatrix n n R ≃ₐ[R] _) = Matrix.toLinAlgEquiv' :=
  rfl

Inverse of Linear-to-Matrix Equivalence Equals Matrix-to-Linear Equivalence

Informal description

The inverse of the algebra equivalence `LinearMap.toMatrixAlgEquiv'` from linear endomorphisms to matrices is equal to the algebra equivalence `Matrix.toLinAlgEquiv'` from matrices to linear endomorphisms. That is, for any commutative ring $R$ and finite type $n$, we have: \[ (\text{LinearMap.toMatrixAlgEquiv'})^{-1} = \text{Matrix.toLinAlgEquiv'} \]

Matrix.toLinAlgEquiv'_symm theorem

: (Matrix.toLinAlgEquiv'.symm : ((n → R) →ₗ[R] n → R) ≃ₐ[R] _) = LinearMap.toMatrixAlgEquiv'

Full source

@[simp]
theorem Matrix.toLinAlgEquiv'_symm :
    (Matrix.toLinAlgEquiv'.symm : ((n → R) →ₗ[R] n → R) ≃ₐ[R] _) = LinearMap.toMatrixAlgEquiv' :=
  rfl

Inverse of Matrix-to-Linear-Map Equivalence is Linear-Map-to-Matrix Equivalence

Informal description

The inverse of the algebra equivalence `Matrix.toLinAlgEquiv'` from square matrices to linear endomorphisms is equal to the algebra equivalence `LinearMap.toMatrixAlgEquiv'` from linear endomorphisms to square matrices. That is, the following diagram commutes: \[ \begin{tikzcd} \text{Matrix } n \times n R \arrow[r, "\text{Matrix.toLinAlgEquiv'}"] & (n \to R) \to_{R} (n \to R) \\ \text{Matrix } n \times n R \arrow[u, "\text{id}"] \arrow[r, "\text{LinearMap.toMatrixAlgEquiv'}"] & (n \to R) \to_{R} (n \to R) \arrow[u, "\text{id}"] \end{tikzcd} \] where both paths from $\text{Matrix } n \times n R$ to $(n \to R) \to_{R} (n \to R)$ are equal.

LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv' theorem

(M : Matrix n n R) : LinearMap.toMatrixAlgEquiv' (Matrix.toLinAlgEquiv' M) = M

Full source

@[simp]
theorem LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv' (M : Matrix n n R) :
    LinearMap.toMatrixAlgEquiv' (Matrix.toLinAlgEquiv' M) = M :=
  LinearMap.toMatrixAlgEquiv'.apply_symm_apply M

Matrix Recovery via Linear Endomorphism Algebra Equivalence

Informal description

For any $n \times n$ matrix $M$ over a commutative ring $R$, the composition of the algebra equivalences `Matrix.toLinAlgEquiv'` and `LinearMap.toMatrixAlgEquiv'` applied to $M$ returns $M$ itself. In other words, converting a matrix to a linear endomorphism and then back to a matrix yields the original matrix.

Matrix.toLinAlgEquiv'_toMatrixAlgEquiv' theorem

(f : (n → R) →ₗ[R] n → R) : Matrix.toLinAlgEquiv' (LinearMap.toMatrixAlgEquiv' f) = f

Full source

@[simp]
theorem Matrix.toLinAlgEquiv'_toMatrixAlgEquiv' (f : (n → R) →ₗ[R] n → R) :
    Matrix.toLinAlgEquiv' (LinearMap.toMatrixAlgEquiv' f) = f :=
  Matrix.toLinAlgEquiv'.apply_symm_apply f

Matrix-Linear Map Equivalence: $\text{toLinAlgEquiv'} \circ \text{toMatrixAlgEquiv'} = \text{id}$

Informal description

For any linear endomorphism $f \colon (n \to R) \to (n \to R)$ over a commutative ring $R$, the composition of the algebra equivalences `Matrix.toLinAlgEquiv'` and `LinearMap.toMatrixAlgEquiv'` applied to $f$ yields $f$ itself. That is, the linear map obtained by first converting $f$ to a matrix and then converting that matrix back to a linear map is identical to the original $f$.

LinearMap.toMatrixAlgEquiv'_apply theorem

(f : (n → R) →ₗ[R] n → R) (i j) : LinearMap.toMatrixAlgEquiv' f i j = f (fun j' ↦ if j' = j then 1 else 0) i

Full source

@[simp]
theorem LinearMap.toMatrixAlgEquiv'_apply (f : (n → R) →ₗ[R] n → R) (i j) :
    LinearMap.toMatrixAlgEquiv' f i j = f (fun j' ↦ if j' = j then 1 else 0) i := by
  simp [LinearMap.toMatrixAlgEquiv']

Matrix Entry Formula for Linear Endomorphisms via Standard Basis

Informal description

For any linear endomorphism $f \colon (n \to R) \to (n \to R)$ over a commutative ring $R$, and for any indices $i$ and $j$, the $(i,j)$-th entry of the matrix associated to $f$ via the algebra equivalence `LinearMap.toMatrixAlgEquiv'` is given by $f(e_j)_i$, where $e_j$ is the standard basis vector with $1$ in the $j$-th position and $0$ elsewhere. That is, $\text{toMatrixAlgEquiv'}(f)_{i,j} = f(\delta_j)_i$, where $\delta_j(k) = 1$ if $k = j$ and $0$ otherwise.

Matrix.toLinAlgEquiv'_apply theorem

(M : Matrix n n R) (v : n → R) : Matrix.toLinAlgEquiv' M v = M *ᵥ v

Full source

@[simp]
theorem Matrix.toLinAlgEquiv'_apply (M : Matrix n n R) (v : n → R) :
    Matrix.toLinAlgEquiv' M v = M *ᵥ v :=
  rfl

Matrix-to-Linear-Map Action via Matrix-Vector Multiplication

Informal description

For any $n \times n$ matrix $M$ over a commutative ring $R$ and any vector $v \in R^n$, the linear endomorphism $\text{toLinAlgEquiv'}(M)$ applied to $v$ equals the matrix-vector product $M \cdot v$.

Matrix.toLinAlgEquiv'_one theorem

: Matrix.toLinAlgEquiv' (1 : Matrix n n R) = LinearMap.id

Full source

theorem Matrix.toLinAlgEquiv'_one : Matrix.toLinAlgEquiv' (1 : Matrix n n R) = LinearMap.id :=
  Matrix.toLin'_one

Identity Matrix Maps to Identity Linear Map under Algebra Equivalence

Informal description

The algebra equivalence `Matrix.toLinAlgEquiv'` maps the identity matrix $1 \in \text{Matrix}_{n \times n}(R)$ to the identity linear map $\text{id} \colon (n \to R) \to (n \to R)$.

LinearMap.toMatrixAlgEquiv'_id theorem

: LinearMap.toMatrixAlgEquiv' (LinearMap.id : (n → R) →ₗ[R] n → R) = 1

Full source

@[simp]
theorem LinearMap.toMatrixAlgEquiv'_id :
    LinearMap.toMatrixAlgEquiv' (LinearMap.id : (n → R) →ₗ[R] n → R) = 1 :=
  LinearMap.toMatrix'_id

Identity Linear Map Maps to Identity Matrix under Algebra Equivalence

Informal description

The algebra equivalence `LinearMap.toMatrixAlgEquiv'` maps the identity linear map $\text{id} \colon (n \to R) \to (n \to R)$ to the identity matrix $1 \in \text{Matrix } n n R$.

LinearMap.toMatrixAlgEquiv'_comp theorem

 (f g : (n → R) →ₗ[R] n → R) :
  LinearMap.toMatrixAlgEquiv' (f.comp g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g

Full source

theorem LinearMap.toMatrixAlgEquiv'_comp (f g : (n → R) →ₗ[R] n → R) :
    LinearMap.toMatrixAlgEquiv' (f.comp g) =
      LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g :=
  LinearMap.toMatrix'_comp _ _

Matrix Representation of Composition of Linear Endomorphisms: $\text{toMatrixAlgEquiv'}(f \circ g) = \text{toMatrixAlgEquiv'}(f) \cdot \text{toMatrixAlgEquiv'}(g)$

Informal description

Let $R$ be a commutative ring and $n$ be a finite type. For any linear endomorphisms $f, g \colon (n \to R) \to (n \to R)$, the matrix representation of the composition $f \circ g$ under the algebra equivalence $\text{toMatrixAlgEquiv'}$ is equal to the product of the matrix representations of $f$ and $g$, i.e., \[ \text{toMatrixAlgEquiv'}(f \circ g) = \text{toMatrixAlgEquiv'}(f) \cdot \text{toMatrixAlgEquiv'}(g). \]

LinearMap.toMatrixAlgEquiv'_mul theorem

 (f g : (n → R) →ₗ[R] n → R) :
  LinearMap.toMatrixAlgEquiv' (f * g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g

Full source

theorem LinearMap.toMatrixAlgEquiv'_mul (f g : (n → R) →ₗ[R] n → R) :
    LinearMap.toMatrixAlgEquiv' (f * g) =
      LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g :=
  LinearMap.toMatrixAlgEquiv'_comp f g

Matrix Representation of Product of Linear Endomorphisms: $\text{toMatrixAlgEquiv'}(f * g) = \text{toMatrixAlgEquiv'}(f) \cdot \text{toMatrixAlgEquiv'}(g)$

Informal description

For any linear endomorphisms $f, g \colon (n \to R) \to (n \to R)$ over a commutative ring $R$, the matrix representation of the product $f * g$ under the algebra equivalence $\text{toMatrixAlgEquiv'}$ is equal to the product of the matrix representations of $f$ and $g$, i.e., \[ \text{toMatrixAlgEquiv'}(f * g) = \text{toMatrixAlgEquiv'}(f) \cdot \text{toMatrixAlgEquiv'}(g). \]

LinearMap.toMatrix definition

: (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R

Full source

/-- 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. -/
def LinearMap.toMatrix : (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R :=
  LinearEquiv.trans (LinearEquiv.arrowCongr v₁.equivFun v₂.equivFun) LinearMap.toMatrix'

Linear map to matrix representation equivalence

Informal description

Given a commutative ring $R$ and two $R$-modules $M₁$ and $M₂$ with bases $v₁ : ι → M₁$ and $v₂ : κ → M₂$, the linear equivalence $\text{LinearMap.toMatrix } v₁ v₂$ maps a linear map $f : M₁ →ₗ[R] M₂$ to its matrix representation with respect to the bases $v₁$ and $v₂$. The matrix is constructed by first converting $f$ to a linear map between coordinate spaces using the basis isomorphisms, then applying the standard linear map to matrix equivalence.

LinearMap.toMatrix_eq_toMatrix' theorem

: LinearMap.toMatrix (Pi.basisFun R n) (Pi.basisFun R n) = LinearMap.toMatrix'

Full source

/-- `LinearMap.toMatrix'` is a particular case of `LinearMap.toMatrix`, for the standard basis
`Pi.basisFun R n`. -/
theorem LinearMap.toMatrix_eq_toMatrix' :
    LinearMap.toMatrix (Pi.basisFun R n) (Pi.basisFun R n) = LinearMap.toMatrix' :=
  rfl

Equality of Linear Map to Matrix Representations with Standard Basis

Informal description

Given a commutative ring $R$ and the standard basis $\text{Pi.basisFun } R n$ on the function space $n \to R$, the linear equivalence $\text{LinearMap.toMatrix}$ with respect to this basis (used for both domain and codomain) is equal to the standard linear map to matrix equivalence $\text{LinearMap.toMatrix'}$.

Matrix.toLin definition

: Matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂

Full source

/-- 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₂`. -/
def Matrix.toLin : MatrixMatrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂ :=
  (LinearMap.toMatrix v₁ v₂).symm

Matrix to linear map equivalence

Informal description

Given a commutative ring $R$ and two $R$-modules $M₁$ and $M₂$ with bases $v₁ : ι → M₁$ and $v₂ : κ → M₂$, the linear equivalence $\text{Matrix.toLin } v₁ v₂$ maps a matrix $A \in \text{Matrix } \kappa \iota R$ to its corresponding linear map $M₁ →ₗ[R] M₂$ with respect to the bases $v₁$ and $v₂$. This is the inverse of the equivalence $\text{LinearMap.toMatrix } v₁ v₂$.

Matrix.toLin_eq_toLin' theorem

: Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin'

Full source

/-- `Matrix.toLin'` is a particular case of `Matrix.toLin`, for the standard basis
`Pi.basisFun R n`. -/
theorem Matrix.toLin_eq_toLin' : Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin' :=
  rfl

Equality of Matrix to Linear Map Representations with Standard Basis

Informal description

Given a commutative ring $R$ and the standard bases $\text{Pi.basisFun } R n$ and $\text{Pi.basisFun } R m$ on the function spaces $n \to R$ and $m \to R$ respectively, the linear equivalence $\text{Matrix.toLin}$ with respect to these bases is equal to the standard matrix to linear map equivalence $\text{Matrix.toLin'}$.

LinearMap.toMatrix_symm theorem

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

Full source

@[simp]
theorem LinearMap.toMatrix_symm : (LinearMap.toMatrix v₁ v₂).symm = Matrix.toLin v₁ v₂ :=
  rfl

Inverse of Linear Map to Matrix Equivalence is Matrix to Linear Map Equivalence

Informal description

Given a commutative ring $R$ and two $R$-modules $M₁$ and $M₂$ with bases $v₁ : ι → M₁$ and $v₂ : κ → M₂$, the inverse of the linear equivalence $\text{LinearMap.toMatrix } v₁ v₂$ is equal to the linear equivalence $\text{Matrix.toLin } v₁ v₂$.

Matrix.toLin_symm theorem

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

Full source

@[simp]
theorem Matrix.toLin_symm : (Matrix.toLin v₁ v₂).symm = LinearMap.toMatrix v₁ v₂ :=
  rfl

Inverse of Matrix-to-Linear-Map Equivalence is Linear-Map-to-Matrix Equivalence

Informal description

Given a commutative ring $R$ and two $R$-modules $M₁$ and $M₂$ with bases $v₁ : ι → M₁$ and $v₂ : κ → M₂$, the inverse of the linear equivalence $\text{Matrix.toLin } v₁ v₂$ is equal to $\text{LinearMap.toMatrix } v₁ v₂$. In other words, the matrix-to-linear-map equivalence and the linear-map-to-matrix equivalence are inverses of each other.

Matrix.toLin_toMatrix theorem

(f : M₁ →ₗ[R] M₂) : Matrix.toLin v₁ v₂ (LinearMap.toMatrix v₁ v₂ f) = f

Full source

@[simp]
theorem Matrix.toLin_toMatrix (f : M₁ →ₗ[R] M₂) :
    Matrix.toLin v₁ v₂ (LinearMap.toMatrix v₁ v₂ f) = f := by
  rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_apply]

Matrix-to-Linear-Map Composition with Linear-Map-to-Matrix is Identity

Informal description

Let $R$ be a commutative ring, and let $M₁$ and $M₂$ be $R$-modules with bases $v₁ : ι → M₁$ and $v₂ : κ → M₂$ respectively. For any linear map $f : M₁ →ₗ[R] M₂$, the composition of the linear equivalences $\text{Matrix.toLin } v₁ v₂$ and $\text{LinearMap.toMatrix } v₁ v₂$ applied to $f$ returns $f$ itself, i.e., \[ \text{Matrix.toLin } v₁ v₂ (\text{LinearMap.toMatrix } v₁ v₂ f) = f. \]

LinearMap.toMatrix_toLin theorem

(M : Matrix m n R) : LinearMap.toMatrix v₁ v₂ (Matrix.toLin v₁ v₂ M) = M

Full source

@[simp]
theorem LinearMap.toMatrix_toLin (M : Matrix m n R) :
    LinearMap.toMatrix v₁ v₂ (Matrix.toLin v₁ v₂ M) = M := by
  rw [← Matrix.toLin_symm, LinearEquiv.symm_apply_apply]

Linear-Map-to-Matrix Composition with Matrix-to-Linear-Map is Identity

Informal description

Let $R$ be a commutative ring, and let $M₁$ and $M₂$ be $R$-modules with bases $v₁ : \iota \to M₁$ and $v₂ : \kappa \to M₂$ respectively. For any matrix $M \in \text{Matrix}_{\kappa \iota}(R)$, the composition of the linear equivalences $\text{LinearMap.toMatrix } v₁ v₂$ and $\text{Matrix.toLin } v₁ v₂$ applied to $M$ returns $M$ itself, i.e., \[ \text{LinearMap.toMatrix } v₁ v₂ (\text{Matrix.toLin } v₁ v₂ M) = M. \]

LinearMap.toMatrix_apply theorem

(f : M₁ →ₗ[R] M₂) (i : m) (j : n) : LinearMap.toMatrix v₁ v₂ f i j = v₂.repr (f (v₁ j)) i

Full source

theorem LinearMap.toMatrix_apply (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
    LinearMap.toMatrix v₁ v₂ f i j = v₂.repr (f (v₁ j)) i := by
  rw [LinearMap.toMatrix, LinearEquiv.trans_apply, LinearMap.toMatrix'_apply,
    LinearEquiv.arrowCongr_apply, Basis.equivFun_symm_apply, Finset.sum_eq_single j, if_pos rfl,
    one_smul, Basis.equivFun_apply]
  · intro j' _ hj'
    rw [if_neg hj', zero_smul]
  · intro hj
    have := Finset.mem_univ j
    contradiction

Matrix Entry Formula for Linear Maps in Given Bases

Informal description

Let $R$ be a commutative ring, $M₁$ and $M₂$ be $R$-modules with bases $v₁ : \iota \to M₁$ and $v₂ : \kappa \to M₂$ respectively, and $f : M₁ \to M₂$ be a linear map. For any indices $i \in \kappa$ and $j \in \iota$, the $(i,j)$-th entry of the matrix representation of $f$ with respect to these bases is given by the $i$-th coordinate of $f(v₁(j))$ in the basis $v₂$, i.e., \[ (\text{LinearMap.toMatrix } v₁ v₂ f)_{i,j} = v₂.\text{repr}(f(v₁(j)))_i. \]

LinearMap.toMatrix_transpose_apply theorem

(f : M₁ →ₗ[R] M₂) (j : n) : (LinearMap.toMatrix v₁ v₂ f)ᵀ j = v₂.repr (f (v₁ j))

Full source

theorem LinearMap.toMatrix_transpose_apply (f : M₁ →ₗ[R] M₂) (j : n) :
    (LinearMap.toMatrix v₁ v₂ f)ᵀ j = v₂.repr (f (v₁ j)) :=
  funext fun i ↦ f.toMatrix_apply _ _ i j

Transpose of Matrix Representation of Linear Map Equals Coordinate Representation of Basis Image

Informal description

Let $R$ be a commutative ring, and let $M₁$ and $M₂$ be $R$-modules with bases $v₁ : \iota \to M₁$ and $v₂ : \kappa \to M₂$ respectively. For any linear map $f : M₁ \to M₂$ and any index $j \in \iota$, the $j$-th column of the transpose of the matrix representation of $f$ with respect to these bases is equal to the coordinate representation of $f(v₁(j))$ in the basis $v₂$, i.e., \[ (\text{LinearMap.toMatrix } v₁ v₂ f)^\top_j = v₂.\text{repr}(f(v₁(j))). \]

LinearMap.toMatrix_apply' theorem

(f : M₁ →ₗ[R] M₂) (i : m) (j : n) : LinearMap.toMatrix v₁ v₂ f i j = v₂.repr (f (v₁ j)) i

Full source

theorem LinearMap.toMatrix_apply' (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
    LinearMap.toMatrix v₁ v₂ f i j = v₂.repr (f (v₁ j)) i :=
  LinearMap.toMatrix_apply v₁ v₂ f i j

Matrix Entry Formula for Linear Maps in Given Bases

Informal description

Let $R$ be a commutative ring, $M_1$ and $M_2$ be $R$-modules with bases $v_1 : \iota \to M_1$ and $v_2 : \kappa \to M_2$ respectively, and $f : M_1 \to M_2$ be a linear map. For any indices $i \in \kappa$ and $j \in \iota$, the $(i,j)$-th entry of the matrix representation of $f$ with respect to these bases is given by the $i$-th coordinate of $f(v_1(j))$ in the basis $v_2$, i.e., \[ (\text{LinearMap.toMatrix } v_1 v_2 f)_{i,j} = v_2.\text{repr}(f(v_1(j)))_i. \]

LinearMap.toMatrix_transpose_apply' theorem

(f : M₁ →ₗ[R] M₂) (j : n) : (LinearMap.toMatrix v₁ v₂ f)ᵀ j = v₂.repr (f (v₁ j))

Full source

theorem LinearMap.toMatrix_transpose_apply' (f : M₁ →ₗ[R] M₂) (j : n) :
    (LinearMap.toMatrix v₁ v₂ f)ᵀ j = v₂.repr (f (v₁ j)) :=
  LinearMap.toMatrix_transpose_apply v₁ v₂ f j

Transpose of Matrix Representation Equals Coordinate Representation of Basis Image

Informal description

Let $R$ be a commutative ring, and let $M_1$ and $M_2$ be $R$-modules with bases $v_1 : \iota \to M_1$ and $v_2 : \kappa \to M_2$ respectively. For any linear map $f : M_1 \to M_2$ and any index $j \in \iota$, the $j$-th column of the transpose of the matrix representation of $f$ with respect to these bases equals the coordinate representation of $f(v_1(j))$ in the basis $v_2$, i.e., $$(\text{LinearMap.toMatrix } v_1 v_2 f)^\top_j = v_2.\text{repr}(f(v_1(j))).$$

LinearMap.toMatrix_id theorem

: LinearMap.toMatrix v₁ v₁ id = 1

Full source

/-- This will be a special case of `LinearMap.toMatrix_id_eq_basis_toMatrix`. -/
theorem LinearMap.toMatrix_id : LinearMap.toMatrix v₁ v₁ id = 1 := by
  ext i j
  simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Matrix Representation of Identity Map is Identity Matrix

Informal description

Given a commutative ring $R$ and an $R$-module $M$ with a basis $v_1 : \iota \to M$, the matrix representation of the identity linear map $\text{id} : M \to M$ with respect to the basis $v_1$ is the identity matrix. In other words, if we represent the identity map in the basis $v_1$, we get the identity matrix: $$\text{LinearMap.toMatrix}(v_1, v_1)(\text{id}) = I$$ where $I$ is the identity matrix of appropriate size.

LinearMap.toMatrix_one theorem

: LinearMap.toMatrix v₁ v₁ 1 = 1

Full source

@[simp]
theorem LinearMap.toMatrix_one : LinearMap.toMatrix v₁ v₁ 1 = 1 :=
  LinearMap.toMatrix_id v₁

Matrix representation of identity endomorphism is identity matrix

Informal description

Given a commutative ring $R$ and an $R$-module $M$ with a basis $v_1 : \iota \to M$, the matrix representation of the identity linear map $1 : M \to M$ with respect to the basis $v_1$ is the identity matrix. That is, $$\text{LinearMap.toMatrix}(v_1, v_1)(1) = I$$ where $I$ denotes the identity matrix of appropriate size.

LinearMap.toMatrix_singleton theorem

{ι : Type*} [Unique ι] (f : R →ₗ[R] R) (i j : ι) : f.toMatrix (.singleton ι R) (.singleton ι R) i j = f 1

Full source

@[simp]
lemma LinearMap.toMatrix_singleton {ι : Type*} [Unique ι] (f : R →ₗ[R] R) (i j : ι) :
    f.toMatrix (.singleton ι R) (.singleton ι R) i j = f 1 := by
  simp [toMatrix, Subsingleton.elim j default]

Matrix Representation of Linear Endomorphism on Singleton Basis Evaluates to $f(1)$

Informal description

Let $\iota$ be a type with a unique element, $R$ a commutative ring, and $f \colon R \to R$ a linear map. For the singleton basis $\text{Basis.singleton } \iota R$ and any indices $i, j \in \iota$, the $(i,j)$-th entry of the matrix representation of $f$ with respect to this basis is equal to $f(1)$. That is, $\text{LinearMap.toMatrix}(\text{Basis.singleton } \iota R, \text{Basis.singleton } \iota R)(f)_{i,j} = f(1)$.

Matrix.toLin_one theorem

: Matrix.toLin v₁ v₁ 1 = LinearMap.id

Full source

@[simp]
theorem Matrix.toLin_one : Matrix.toLin v₁ v₁ 1 = LinearMap.id := by
  rw [← LinearMap.toMatrix_id v₁, Matrix.toLin_toMatrix]

Identity Matrix Represents Identity Linear Map

Informal description

Given a commutative ring $R$ and an $R$-module $M$ with a basis $v_1 : \iota \to M$, the linear map corresponding to the identity matrix under the equivalence $\text{Matrix.toLin } v_1 v_1$ is the identity linear map $\text{id} : M \to M$. In other words, we have: $$\text{Matrix.toLin}(v_1, v_1)(I) = \text{id}$$ where $I$ is the identity matrix of appropriate size.

LinearMap.toMatrix_reindexRange theorem

 [DecidableEq M₁] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
  LinearMap.toMatrix v₁.reindexRange v₂.reindexRange f ⟨v₂ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ =
    LinearMap.toMatrix v₁ v₂ f k i

Full source

theorem LinearMap.toMatrix_reindexRange [DecidableEq M₁] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
    LinearMap.toMatrix v₁.reindexRange v₂.reindexRange f ⟨v₂ k, Set.mem_range_self k⟩
        ⟨v₁ i, Set.mem_range_self i⟩ =
      LinearMap.toMatrix v₁ v₂ f k i := by
  simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]

Matrix Representation Invariance under Basis Reindexing by Range

Informal description

Let $R$ be a commutative ring, $M₁$ and $M₂$ be $R$-modules with bases $v₁ : n \to M₁$ and $v₂ : m \to M₂$ respectively, and $f : M₁ \to M₂$ a linear map. For any indices $k \in m$ and $i \in n$, the $(k,i)$-th entry of the matrix representation of $f$ with respect to the reindexed bases $v₁.\text{reindexRange}$ and $v₂.\text{reindexRange}$ is equal to the $(k,i)$-th entry of the matrix representation of $f$ with respect to the original bases $v₁$ and $v₂$. In other words, reindexing the bases by their ranges does not change the matrix entries: \[ (\text{LinearMap.toMatrix } v₁.\text{reindexRange} v₂.\text{reindexRange} f)_{\langle v₂ k, \text{mem\_range\_self } k \rangle, \langle v₁ i, \text{mem\_range\_self } i \rangle} = (\text{LinearMap.toMatrix } v₁ v₂ f)_{k,i}. \]

LinearMap.toMatrix_algebraMap theorem

(x : R) : LinearMap.toMatrix v₁ v₁ (algebraMap R (Module.End R M₁) x) = scalar n x

Full source

@[simp]
theorem LinearMap.toMatrix_algebraMap (x : R) :
    LinearMap.toMatrix v₁ v₁ (algebraMap R (Module.End R M₁) x) = scalar n x := by
  simp [Module.algebraMap_end_eq_smul_id, LinearMap.toMatrix_id, smul_eq_diagonal_mul]

Matrix Representation of Scalar Multiplication is Scalar Matrix

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a basis $v₁ : n \to M₁$. For any element $x \in R$, the matrix representation of the scalar multiplication map $x \cdot \text{id}_{M₁}$ (where $\text{id}_{M₁}$ is the identity endomorphism on $M₁$) with respect to the basis $v₁$ is the scalar matrix $x I_n$, where $I_n$ is the identity matrix of size $n \times n$. In other words, the matrix of the linear map $y \mapsto x \cdot y$ in the basis $v₁$ is the diagonal matrix with $x$ on all diagonal entries: $$\text{LinearMap.toMatrix}(v₁, v₁)(x \cdot \text{id}_{M₁}) = x I_n$$

LinearMap.toMatrix_mulVec_repr theorem

(f : M₁ →ₗ[R] M₂) (x : M₁) : LinearMap.toMatrix v₁ v₂ f *ᵥ v₁.repr x = v₂.repr (f x)

Full source

theorem LinearMap.toMatrix_mulVec_repr (f : M₁ →ₗ[R] M₂) (x : M₁) :
    LinearMap.toMatrixLinearMap.toMatrix v₁ v₂ f *ᵥ v₁.repr x = v₂.repr (f x) := by
  ext i
  rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
    LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]
  congr
  exact v₁.equivFun.symm_apply_apply x

Matrix Representation of Linear Map Acts on Coordinates via Matrix-Vector Multiplication

Informal description

Let $R$ be a commutative ring, and let $M₁$ and $M₂$ be $R$-modules with bases $v₁ : ι → M₁$ and $v₂ : κ → M₂$, respectively. For any linear map $f : M₁ →ₗ[R] M₂$ and any element $x ∈ M₁$, the matrix-vector product of the matrix representation of $f$ (with respect to the bases $v₁$ and $v₂$) and the coordinate vector of $x$ (with respect to $v₁$) equals the coordinate vector of $f(x)$ (with respect to $v₂$). That is, if $A$ is the matrix of $f$ and $[x]$ is the coordinate vector of $x$, then $A \cdot [x] = [f(x)]$.

LinearMap.toMatrix_basis_equiv theorem

 [Fintype l] [DecidableEq l] (b : Basis l R M₁) (b' : Basis l R M₂) :
  LinearMap.toMatrix b' b (b'.equiv b (Equiv.refl l) : M₂ →ₗ[R] M₁) = 1

Full source

@[simp]
theorem LinearMap.toMatrix_basis_equiv [Fintype l] [DecidableEq l] (b : Basis l R M₁)
    (b' : Basis l R M₂) :
    LinearMap.toMatrix b' b (b'.equiv b (Equiv.refl l) : M₂ →ₗ[R] M₁) = 1 := by
  ext i j
  simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Matrix Representation of Basis Identity Equivalence is Identity Matrix

Informal description

Let $R$ be a commutative ring, and let $M₁$ and $M₂$ be $R$-modules with bases $b : l \to M₁$ and $b' : l \to M₂$ indexed by a finite type $l$. The matrix representation of the linear equivalence $b'.\text{equiv}\, b\, \text{id}_l : M₂ \to M₁$ (where $\text{id}_l$ is the identity equivalence on $l$) with respect to the bases $b'$ and $b$ is the identity matrix $1$.

LinearMap.toMatrix_smulBasis_left theorem

 {G} [Group G] [DistribMulAction G M₁] [SMulCommClass G R M₁] (g : G) (f : M₁ →ₗ[R] M₂) :
  LinearMap.toMatrix (g • v₁) v₂ f = LinearMap.toMatrix v₁ v₂ (f ∘ₗ DistribMulAction.toLinearMap _ _ g)

Full source

theorem LinearMap.toMatrix_smulBasis_left {G} [Group G] [DistribMulAction G M₁]
    [SMulCommClass G R M₁] (g : G) (f : M₁ →ₗ[R] M₂) :
    LinearMap.toMatrix (g • v₁) v₂ f =
      LinearMap.toMatrix v₁ v₂ (f ∘ₗ DistribMulAction.toLinearMap _ _ g) := by
  ext
  rw [LinearMap.toMatrix_apply, LinearMap.toMatrix_apply]
  dsimp

Matrix Representation under Left Basis Scaling: $\text{toMatrix}(g \cdot v₁, v₂)(f) = \text{toMatrix}(v₁, v₂)(f \circ g)$

Informal description

Let $R$ be a commutative ring, $M₁$ and $M₂$ be $R$-modules with bases $v₁ : ι \to M₁$ and $v₂ : κ \to M₂$, and let $G$ be a group acting distributively on $M₁$ such that the action commutes with scalar multiplication by $R$. For any $g \in G$ and any linear map $f : M₁ \to M₂$, the matrix representation of $f$ with respect to the scaled basis $g \cdot v₁$ and $v₂$ is equal to the matrix representation of $f \circ g$ with respect to the original bases $v₁$ and $v₂$. That is, \[ \text{toMatrix}(g \cdot v₁, v₂)(f) = \text{toMatrix}(v₁, v₂)(f \circ g). \]

LinearMap.toMatrix_smulBasis_right theorem

 {G} [Group G] [DistribMulAction G M₂] [SMulCommClass G R M₂] (g : G) (f : M₁ →ₗ[R] M₂) :
  LinearMap.toMatrix v₁ (g • v₂) f = LinearMap.toMatrix v₁ v₂ (DistribMulAction.toLinearMap _ _ g⁻¹ ∘ₗ f)

Full source

theorem LinearMap.toMatrix_smulBasis_right {G} [Group G] [DistribMulAction G M₂]
    [SMulCommClass G R M₂] (g : G) (f : M₁ →ₗ[R] M₂) :
    LinearMap.toMatrix v₁ (g • v₂) f =
      LinearMap.toMatrix v₁ v₂ (DistribMulAction.toLinearMapDistribMulAction.toLinearMap _ _ g⁻¹ ∘ₗ f) := by
  ext
  rw [LinearMap.toMatrix_apply, LinearMap.toMatrix_apply]
  dsimp

Matrix Representation under Right Basis Scaling: $\text{toMatrix}(v₁, g \cdot v₂)(f) = \text{toMatrix}(v₁, v₂)(g^{-1} \circ f)$

Informal description

Let $R$ be a commutative ring, $M₁$ and $M₂$ be $R$-modules with bases $v₁ : \iota \to M₁$ and $v₂ : \kappa \to M₂$ respectively, and let $G$ be a group acting on $M₂$ such that the action commutes with scalar multiplication by $R$. For any $g \in G$ and any linear map $f : M₁ \to M₂$, the matrix representation of $f$ with respect to the bases $v₁$ and $g \cdot v₂$ is equal to the matrix representation of the linear map $g^{-1} \circ f$ with respect to the original bases $v₁$ and $v₂$. In other words, we have: \[ \text{LinearMap.toMatrix } v₁ (g \cdot v₂) f = \text{LinearMap.toMatrix } v₁ v₂ (g^{-1} \circ f). \]

Matrix.toLin_apply theorem

(M : Matrix m n R) (v : M₁) : Matrix.toLin v₁ v₂ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₂ j

Full source

theorem Matrix.toLin_apply (M : Matrix m n R) (v : M₁) :
    Matrix.toLin v₁ v₂ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₂ j :=
  show v₂.equivFun.symm (Matrix.toLin' M (v₁.repr v)) = _ by
    rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]

Action of Matrix-to-Linear-Map via Basis Coordinates: $\text{toLin}(M)(v) = \sum_j (M \cdot \text{repr}(v))_j v_2(j)$

Informal description

Let $R$ be a commutative ring, and let $M_1$ and $M_2$ be $R$-modules with finite bases $v_1 : \iota \to M_1$ and $v_2 : \kappa \to M_2$. For any matrix $M \in \text{Matrix}_{\kappa \iota}(R)$ and any vector $v \in M_1$, the linear map $\text{Matrix.toLin}(v_1, v_2)(M)$ applied to $v$ is given by: \[ \text{Matrix.toLin}(v_1, v_2)(M)(v) = \sum_{j \in \kappa} (M \cdot \text{repr}_{v_1}(v))_j \cdot v_2(j), \] where $\text{repr}_{v_1}(v) \in \iota \to R$ is the coordinate representation of $v$ with respect to the basis $v_1$, and $M \cdot \text{repr}_{v_1}(v)$ denotes matrix-vector multiplication.

Matrix.toLin_self theorem

(M : Matrix m n R) (i : n) : Matrix.toLin v₁ v₂ M (v₁ i) = ∑ j, M j i • v₂ j

Full source

@[simp]
theorem Matrix.toLin_self (M : Matrix m n R) (i : n) :
    Matrix.toLin v₁ v₂ M (v₁ i) = ∑ j, M j i • v₂ j := by
  rw [Matrix.toLin_apply, Finset.sum_congr rfl fun j _hj ↦ ?_]
  rw [Basis.repr_self, Matrix.mulVec, dotProduct, Finset.sum_eq_single i, Finsupp.single_eq_same,
    mul_one]
  · intro i' _ i'_ne
    rw [Finsupp.single_eq_of_ne i'_ne.symm, mul_zero]
  · intros
    have := Finset.mem_univ i
    contradiction

Action of Matrix-to-Linear-Map on Basis Vectors: $\text{toLin}(M)(v_1(i)) = \sum_j M_{j,i} v_2(j)$

Informal description

Let $R$ be a commutative ring, and let $M_1$ and $M_2$ be $R$-modules with finite bases $v_1 : \iota \to M_1$ and $v_2 : \kappa \to M_2$. For any matrix $M \in \text{Matrix}_{\kappa \iota}(R)$ and any basis vector $v_1(i) \in M_1$, the linear map $\text{Matrix.toLin}(v_1, v_2)(M)$ applied to $v_1(i)$ is given by: \[ \text{Matrix.toLin}(v_1, v_2)(M)(v_1(i)) = \sum_{j \in \kappa} M_{j,i} \cdot v_2(j), \] where $M_{j,i}$ denotes the entry of $M$ at row $j$ and column $i$.

LinearMap.toMatrix_comp theorem

 [Finite l] [DecidableEq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
  LinearMap.toMatrix v₁ v₃ (f.comp g) = LinearMap.toMatrix v₂ v₃ f * LinearMap.toMatrix v₁ v₂ g

Full source

theorem LinearMap.toMatrix_comp [Finite l] [DecidableEq m] (f : M₂ →ₗ[R] M₃) (g : M₁ →ₗ[R] M₂) :
    LinearMap.toMatrix v₁ v₃ (f.comp g) =
    LinearMap.toMatrix v₂ v₃ f * LinearMap.toMatrix v₁ v₂ g := by
  simp_rw [LinearMap.toMatrix, LinearEquiv.trans_apply, LinearEquiv.arrowCongr_comp _ v₂.equivFun,
    LinearMap.toMatrix'_comp]

Matrix Representation of Linear Map Composition: $\text{toMatrix}(f \circ g) = \text{toMatrix}(f) \cdot \text{toMatrix}(g)$

Informal description

Let $R$ be a commutative ring, and let $M₁$, $M₂$, $M₃$ be $R$-modules with finite bases $v₁ : ι → M₁$, $v₂ : κ → M₂$, and $v₃ : l → M₃$. For any linear maps $f : M₂ →ₗ[R] M₃$ and $g : M₁ →ₗ[R] M₂$, the matrix representation of the composition $f \circ g$ with respect to the bases $v₁$ and $v₃$ is equal to the product of the matrix representations of $f$ (with respect to $v₂$ and $v₃$) and $g$ (with respect to $v₁$ and $v₂$), i.e., \[ \text{toMatrix}_{v₁ v₃}(f \circ g) = \text{toMatrix}_{v₂ v₃}(f) \cdot \text{toMatrix}_{v₁ v₂}(g). \]

LinearMap.toMatrix_mul theorem

 (f g : M₁ →ₗ[R] M₁) : LinearMap.toMatrix v₁ v₁ (f * g) = LinearMap.toMatrix v₁ v₁ f * LinearMap.toMatrix v₁ v₁ g

Full source

theorem LinearMap.toMatrix_mul (f g : M₁ →ₗ[R] M₁) :
    LinearMap.toMatrix v₁ v₁ (f * g) = LinearMap.toMatrix v₁ v₁ f * LinearMap.toMatrix v₁ v₁ g := by
  rw [Module.End.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

Matrix Representation of Linear Map Composition: $\text{toMatrix}(f \circ g) = \text{toMatrix}(f) \cdot \text{toMatrix}(g)$

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : ι → M₁$. For any two linear endomorphisms $f, g : M₁ →ₗ[R] M₁$, the matrix representation of their composition $f \circ g$ with respect to the basis $v₁$ is equal to the product of their individual matrix representations, i.e., \[ \text{toMatrix}_{v₁ v₁}(f \circ g) = \text{toMatrix}_{v₁ v₁}(f) \cdot \text{toMatrix}_{v₁ v₁}(g). \]

LinearMap.toMatrix_pow theorem

(f : M₁ →ₗ[R] M₁) (k : ℕ) : (toMatrix v₁ v₁ f) ^ k = toMatrix v₁ v₁ (f ^ k)

Full source

lemma LinearMap.toMatrix_pow (f : M₁ →ₗ[R] M₁) (k : ℕ) :
    (toMatrix v₁ v₁ f) ^ k = toMatrix v₁ v₁ (f ^ k) := by
  induction k with
  | zero => simp
  | succ k ih => rw [pow_succ, pow_succ, ih, ← toMatrix_mul]

Matrix Representation of Iterated Linear Map Equals Matrix Power

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : ι → M₁$. For any linear endomorphism $f : M₁ →ₗ[R] M₁$ and any natural number $k$, the matrix representation of the $k$-th iterate $f^k$ with respect to the basis $v₁$ is equal to the $k$-th power of the matrix representation of $f$, i.e., \[ \text{toMatrix}_{v₁ v₁}(f^k) = (\text{toMatrix}_{v₁ v₁} f)^k. \]

Matrix.toLin_mul theorem

 [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).comp (Matrix.toLin v₁ v₂ B)

Full source

theorem Matrix.toLin_mul [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).comp (Matrix.toLin v₁ v₂ B) := by
  apply (LinearMap.toMatrix v₁ v₃).injective
  haveI : DecidableEq l := fun _ _ ↦ Classical.propDecidable _
  rw [LinearMap.toMatrix_comp v₁ v₂ v₃]
  repeat' rw [LinearMap.toMatrix_toLin]

Matrix Product to Linear Map Composition: $\text{toLin}(AB) = \text{toLin}(A) \circ \text{toLin}(B)$

Informal description

Let $R$ be a commutative ring, and let $M₁$, $M₂$, $M₃$ be $R$-modules with finite bases $v₁ : n \to M₁$, $v₂ : m \to M₂$, and $v₃ : l \to M₃$. For any matrices $A \in \text{Matrix}_{l m}(R)$ and $B \in \text{Matrix}_{m n}(R)$, the linear map corresponding to the matrix product $AB$ via $\text{Matrix.toLin}$ is equal to the composition of the linear maps corresponding to $A$ and $B$ respectively, i.e., \[ \text{Matrix.toLin}_{v₁ v₃}(AB) = (\text{Matrix.toLin}_{v₂ v₃} A) \circ (\text{Matrix.toLin}_{v₁ v₂} B). \]

Matrix.toLin_mul_apply theorem

 [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) (x) :
  Matrix.toLin v₁ v₃ (A * B) x = (Matrix.toLin v₂ v₃ A) (Matrix.toLin v₁ v₂ B x)

Full source

/-- Shortcut lemma for `Matrix.toLin_mul` and `LinearMap.comp_apply`. -/
theorem Matrix.toLin_mul_apply [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R)
    (x) : Matrix.toLin v₁ v₃ (A * B) x = (Matrix.toLin v₂ v₃ A) (Matrix.toLin v₁ v₂ B x) := by
  rw [Matrix.toLin_mul v₁ v₂, LinearMap.comp_apply]

Matrix-to-Linear-Map Composition Formula: $\text{toLin}(AB)(x) = \text{toLin}(A)(\text{toLin}(B)(x))$

Informal description

Let $R$ be a commutative ring, and let $M₁$, $M₂$, $M₃$ be $R$-modules with finite bases $v₁ : n \to M₁$, $v₂ : m \to M₂$, and $v₃ : l \to M₃$. For any matrices $A \in \text{Matrix}_{l \times m}(R)$ and $B \in \text{Matrix}_{m \times n}(R)$, and for any $x \in M₁$, the following equality holds: \[ \text{Matrix.toLin}_{v₁ v₃}(A B)(x) = (\text{Matrix.toLin}_{v₂ v₃} A)(\text{Matrix.toLin}_{v₁ v₂} B (x)). \]

Matrix.toLinOfInv definition

[DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : M₁ ≃ₗ[R] M₂

Full source

/-- If `M` and `M` are each other's inverse matrices, `Matrix.toLin M` and `Matrix.toLin M'`
form a linear equivalence. -/
@[simps]
def Matrix.toLinOfInv [DecidableEq m] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1)
    (hM'M : M' * M = 1) : M₁ ≃ₗ[R] M₂ :=
  { Matrix.toLin v₁ v₂ M with
    toFun := Matrix.toLin v₁ v₂ M
    invFun := Matrix.toLin v₂ v₁ M'
    left_inv := fun x ↦ by rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]
    right_inv := fun x ↦ by
      rw [← Matrix.toLin_mul_apply, hMM', Matrix.toLin_one, id_apply] }

Linear equivalence from matrix inverse pair

Informal description

Given a commutative ring $R$ and two $R$-modules $M₁$ and $M₂$ with bases $v₁ : m \to M₁$ and $v₂ : n \to M₂$, if $M$ is an $m \times n$ matrix and $M'$ is an $n \times m$ matrix such that $M * M' = 1$ and $M' * M = 1$, then the linear map $\text{Matrix.toLin } v₁ v₂ M$ and its inverse $\text{Matrix.toLin } v₂ v₁ M'$ form a linear equivalence between $M₁$ and $M₂$.

LinearMap.toMatrixAlgEquiv definition

: (M₁ →ₗ[R] M₁) ≃ₐ[R] Matrix n n R

Full source

/-- 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. -/
def LinearMap.toMatrixAlgEquiv : (M₁ →ₗ[R] M₁) ≃ₐ[R] Matrix n n R :=
  AlgEquiv.ofLinearEquiv
    (LinearMap.toMatrix v₁ v₁) (LinearMap.toMatrix_one v₁) (LinearMap.toMatrix_mul v₁)

Algebra equivalence between linear endomorphisms and square matrices

Informal description

Given a commutative ring $R$ and an $R$-module $M₁$ with a finite basis $v₁ : n \to M₁$, the algebra equivalence $\text{LinearMap.toMatrixAlgEquiv } v₁$ maps a linear endomorphism $f : M₁ \to M₁$ to its matrix representation with respect to the basis $v₁$. This equivalence preserves the multiplicative identity and composition of linear maps, meaning: 1. The identity linear map is sent to the identity matrix. 2. The composition of two linear maps is sent to the product of their respective matrices.

Matrix.toLinAlgEquiv definition

: Matrix n n R ≃ₐ[R] M₁ →ₗ[R] M₁

Full source

/-- 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₁`. -/
def Matrix.toLinAlgEquiv : MatrixMatrix n n R ≃ₐ[R] M₁ →ₗ[R] M₁ :=
  (LinearMap.toMatrixAlgEquiv v₁).symm

Algebra equivalence from square matrices to linear endomorphisms

Informal description

Given a commutative ring $R$ and an $R$-module $M₁$ with a finite basis $v₁ : n \to M₁$, the algebra equivalence $\text{Matrix.toLinAlgEquiv } v₁$ maps a square matrix $A$ over $R$ indexed by $n$ to the linear endomorphism of $M₁$ whose matrix representation with respect to the basis $v₁$ is $A$. This equivalence is the inverse of $\text{LinearMap.toMatrixAlgEquiv } v₁$, and it preserves the multiplicative identity and composition of linear maps, meaning: 1. The identity matrix is sent to the identity linear map. 2. The product of two matrices is sent to the composition of their respective linear maps.

LinearMap.toMatrixAlgEquiv_symm theorem

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

Full source

@[simp]
theorem LinearMap.toMatrixAlgEquiv_symm :
    (LinearMap.toMatrixAlgEquiv v₁).symm = Matrix.toLinAlgEquiv v₁ :=
  rfl

Inverse of Linear-to-Matrix Algebra Equivalence Equals Matrix-to-Linear Equivalence

Informal description

The inverse of the algebra equivalence $\text{LinearMap.toMatrixAlgEquiv } v₁$ is equal to the algebra equivalence $\text{Matrix.toLinAlgEquiv } v₁$. In other words, the map that converts matrices back to linear endomorphisms is precisely the inverse of the map that converts linear endomorphisms to matrices, with respect to the basis $v₁$.

Matrix.toLinAlgEquiv_symm theorem

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

Full source

@[simp]
theorem Matrix.toLinAlgEquiv_symm :
    (Matrix.toLinAlgEquiv v₁).symm = LinearMap.toMatrixAlgEquiv v₁ :=
  rfl

Inverse of Matrix-to-Linear-Map Equivalence is Linear-Map-to-Matrix Equivalence

Informal description

Given a commutative ring $R$ and an $R$-module $M₁$ with a finite basis $v₁ : n \to M₁$, the inverse of the algebra equivalence $\text{Matrix.toLinAlgEquiv } v₁$ is equal to the algebra equivalence $\text{LinearMap.toMatrixAlgEquiv } v₁$. In other words, the map that converts linear endomorphisms of $M₁$ to their matrix representations with respect to the basis $v₁$ is precisely the inverse of the map that converts matrices to linear endomorphisms.

Matrix.toLinAlgEquiv_toMatrixAlgEquiv theorem

(f : M₁ →ₗ[R] M₁) : Matrix.toLinAlgEquiv v₁ (LinearMap.toMatrixAlgEquiv v₁ f) = f

Full source

@[simp]
theorem Matrix.toLinAlgEquiv_toMatrixAlgEquiv (f : M₁ →ₗ[R] M₁) :
    Matrix.toLinAlgEquiv v₁ (LinearMap.toMatrixAlgEquiv v₁ f) = f := by
  rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.apply_symm_apply]

Matrix-to-Linear-Map Composition Recovers Original Linear Endomorphism

Informal description

Given a commutative ring $R$, an $R$-module $M₁$ with a finite basis $v₁ : n \to M₁$, and a linear endomorphism $f : M₁ \to M₁$, the composition of the matrix representation map $\text{LinearMap.toMatrixAlgEquiv } v₁$ followed by the linear map representation $\text{Matrix.toLinAlgEquiv } v₁$ recovers the original linear endomorphism $f$. In other words, converting $f$ to its matrix representation and then back to a linear map yields $f$ again.

LinearMap.toMatrixAlgEquiv_toLinAlgEquiv theorem

(M : Matrix n n R) : LinearMap.toMatrixAlgEquiv v₁ (Matrix.toLinAlgEquiv v₁ M) = M

Full source

@[simp]
theorem LinearMap.toMatrixAlgEquiv_toLinAlgEquiv (M : Matrix n n R) :
    LinearMap.toMatrixAlgEquiv v₁ (Matrix.toLinAlgEquiv v₁ M) = M := by
  rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.symm_apply_apply]

Matrix Representation of Linear Map from Matrix Equals Original Matrix

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$. For any square matrix $M$ over $R$ indexed by $n$, the matrix representation of the linear endomorphism $\text{Matrix.toLinAlgEquiv } v₁ M$ with respect to the basis $v₁$ is equal to $M$ itself. In other words, the composition of the matrix-to-linear-map equivalence followed by the linear-map-to-matrix equivalence is the identity on matrices.

LinearMap.toMatrixAlgEquiv_apply theorem

(f : M₁ →ₗ[R] M₁) (i j : n) : LinearMap.toMatrixAlgEquiv v₁ f i j = v₁.repr (f (v₁ j)) i

Full source

theorem LinearMap.toMatrixAlgEquiv_apply (f : M₁ →ₗ[R] M₁) (i j : n) :
    LinearMap.toMatrixAlgEquiv v₁ f i j = v₁.repr (f (v₁ j)) i := by
  simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_apply]

Matrix Entry Formula for Linear Endomorphisms in Given Basis

Informal description

Let $R$ be a commutative ring, $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$, and $f : M₁ \to M₁$ be a linear endomorphism. For any indices $i, j \in n$, the $(i,j)$-th entry of the matrix representation of $f$ with respect to the basis $v₁$ is given by the $i$-th coordinate of $f(v₁(j))$ in the basis $v₁$, i.e., \[ (\text{LinearMap.toMatrixAlgEquiv } v₁ f)_{i,j} = v₁.\text{repr}(f(v₁(j)))_i. \]

LinearMap.toMatrixAlgEquiv_transpose_apply theorem

(f : M₁ →ₗ[R] M₁) (j : n) : (LinearMap.toMatrixAlgEquiv v₁ f)ᵀ j = v₁.repr (f (v₁ j))

Full source

theorem LinearMap.toMatrixAlgEquiv_transpose_apply (f : M₁ →ₗ[R] M₁) (j : n) :
    (LinearMap.toMatrixAlgEquiv v₁ f)ᵀ j = v₁.repr (f (v₁ j)) :=
  funext fun i ↦ f.toMatrix_apply _ _ i j

Transpose of Matrix Representation of Linear Endomorphism in Basis

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$. For any linear endomorphism $f : M₁ \to M₁$ and any index $j \in n$, the $j$-th column of the transpose of the matrix representation of $f$ with respect to the basis $v₁$ is equal to the coordinates of $f(v₁(j))$ in the basis $v₁$, i.e., \[ (\text{LinearMap.toMatrixAlgEquiv } v₁ f)^\top_j = v₁.\text{repr}(f(v₁(j))). \]

LinearMap.toMatrixAlgEquiv_apply' theorem

(f : M₁ →ₗ[R] M₁) (i j : n) : LinearMap.toMatrixAlgEquiv v₁ f i j = v₁.repr (f (v₁ j)) i

Full source

theorem LinearMap.toMatrixAlgEquiv_apply' (f : M₁ →ₗ[R] M₁) (i j : n) :
    LinearMap.toMatrixAlgEquiv v₁ f i j = v₁.repr (f (v₁ j)) i :=
  LinearMap.toMatrixAlgEquiv_apply v₁ f i j

Matrix Entry Formula for Linear Endomorphisms in Given Basis (variant)

Informal description

Let $R$ be a commutative ring, $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$, and $f : M₁ \to M₁$ be a linear endomorphism. For any indices $i, j \in n$, the $(i,j)$-th entry of the matrix representation of $f$ with respect to the basis $v₁$ is given by the $i$-th coordinate of $f(v₁(j))$ in the basis $v₁$, i.e., \[ (\text{LinearMap.toMatrixAlgEquiv } v₁ f)_{i,j} = v₁.\text{repr}(f(v₁(j)))_i. \]

LinearMap.toMatrixAlgEquiv_transpose_apply' theorem

(f : M₁ →ₗ[R] M₁) (j : n) : (LinearMap.toMatrixAlgEquiv v₁ f)ᵀ j = v₁.repr (f (v₁ j))

Full source

theorem LinearMap.toMatrixAlgEquiv_transpose_apply' (f : M₁ →ₗ[R] M₁) (j : n) :
    (LinearMap.toMatrixAlgEquiv v₁ f)ᵀ j = v₁.repr (f (v₁ j)) :=
  LinearMap.toMatrixAlgEquiv_transpose_apply v₁ f j

Transpose of Matrix Representation of Linear Endomorphism in Basis

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$. For any linear endomorphism $f : M₁ \to M₁$ and any index $j \in n$, the $j$-th column of the transpose of the matrix representation of $f$ with respect to the basis $v₁$ is equal to the coordinates of $f(v₁(j))$ in the basis $v₁$, i.e., \[ (\text{toMatrixAlgEquiv } v₁ f)^\top_j = v₁.\text{repr}(f(v₁(j))). \]

Matrix.toLinAlgEquiv_apply theorem

(M : Matrix n n R) (v : M₁) : Matrix.toLinAlgEquiv v₁ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₁ j

Full source

theorem Matrix.toLinAlgEquiv_apply (M : Matrix n n R) (v : M₁) :
    Matrix.toLinAlgEquiv v₁ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₁ j :=
  show v₁.equivFun.symm (Matrix.toLinAlgEquiv' M (v₁.repr v)) = _ by
    rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]

Matrix-to-Linear-Map Action via Basis Coordinates and Linear Combination

Informal description

Let $R$ be a commutative ring, $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$, and $M$ be an $n \times n$ matrix over $R$. For any vector $v \in M₁$, the linear endomorphism $\text{Matrix.toLinAlgEquiv}(v₁)(M)$ applied to $v$ is given by the linear combination: \[ \sum_{j} (M \cdot \text{repr}_{v₁}(v))_j \cdot v₁(j), \] where $\text{repr}_{v₁}(v)$ denotes the coordinate representation of $v$ in the basis $v₁$, and $M \cdot \text{repr}_{v₁}(v)$ is the matrix-vector product.

Matrix.toLinAlgEquiv_self theorem

(M : Matrix n n R) (i : n) : Matrix.toLinAlgEquiv v₁ M (v₁ i) = ∑ j, M j i • v₁ j

Full source

@[simp]
theorem Matrix.toLinAlgEquiv_self (M : Matrix n n R) (i : n) :
    Matrix.toLinAlgEquiv v₁ M (v₁ i) = ∑ j, M j i • v₁ j :=
  Matrix.toLin_self _ _ _ _

Action of Matrix-to-Endomorphism on Basis Vectors: $\text{toLinAlgEquiv}(M)(v₁(i)) = \sum_j M_{j,i} v₁(j)$

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$. For any square matrix $M \in \text{Matrix}_{n n}(R)$ and any basis vector $v₁(i) \in M₁$, the linear endomorphism $\text{Matrix.toLinAlgEquiv}(v₁)(M)$ acts on $v₁(i)$ as: \[ \text{Matrix.toLinAlgEquiv}(v₁)(M)(v₁(i)) = \sum_{j \in n} M_{j,i} \cdot v₁(j), \] where $M_{j,i}$ denotes the entry of $M$ at row $j$ and column $i$.

LinearMap.toMatrixAlgEquiv_id theorem

: LinearMap.toMatrixAlgEquiv v₁ id = 1

Full source

theorem LinearMap.toMatrixAlgEquiv_id : LinearMap.toMatrixAlgEquiv v₁ id = 1 := by
  simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]

Matrix Representation of Identity Map is Identity Matrix

Informal description

Given a commutative ring $R$ and an $R$-module $M$ with a finite basis $v_1 : n \to M$, the matrix representation of the identity linear map $\text{id} : M \to M$ with respect to the basis $v_1$ is the identity matrix. That is, \[ \text{toMatrixAlgEquiv}_{v_1}(\text{id}) = I, \] where $I$ denotes the identity matrix of size $n \times n$.

Matrix.toLinAlgEquiv_one theorem

: Matrix.toLinAlgEquiv v₁ 1 = LinearMap.id

Full source

theorem Matrix.toLinAlgEquiv_one : Matrix.toLinAlgEquiv v₁ 1 = LinearMap.id := by
  rw [← LinearMap.toMatrixAlgEquiv_id v₁, Matrix.toLinAlgEquiv_toMatrixAlgEquiv]

Identity Matrix Maps to Identity Endomorphism under Matrix-to-Linear-Map Equivalence

Informal description

Given a commutative ring $R$ and an $R$-module $M₁$ with a finite basis $v₁ : n \to M₁$, the linear endomorphism corresponding to the identity matrix $1$ under the algebra equivalence $\text{Matrix.toLinAlgEquiv } v₁$ is the identity linear map $\text{id} : M₁ \to M₁$. That is, \[ \text{Matrix.toLinAlgEquiv}_{v₁}(1) = \text{id}. \]

LinearMap.toMatrixAlgEquiv_reindexRange theorem

 [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) :
  LinearMap.toMatrixAlgEquiv v₁.reindexRange f ⟨v₁ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ =
    LinearMap.toMatrixAlgEquiv v₁ f k i

Full source

theorem LinearMap.toMatrixAlgEquiv_reindexRange [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) :
    LinearMap.toMatrixAlgEquiv v₁.reindexRange f
        ⟨v₁ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ =
      LinearMap.toMatrixAlgEquiv v₁ f k i := by
  simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr]

Matrix Entry Invariance under Basis Reindexing by Range: $(\text{toMatrixAlgEquiv } v₁.\text{reindexRange } f)_{\langle v₁ k, \cdot \rangle, \langle v₁ i, \cdot \rangle} = (\text{toMatrixAlgEquiv } v₁ f)_{k,i}$

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$. For any linear endomorphism $f : M₁ \to M₁$ and indices $k, i \in n$, the matrix entry of $f$ with respect to the reindexed basis $v₁.\text{reindexRange}$ at positions $\langle v₁ k, \text{Set.mem_range_self } k \rangle$ and $\langle v₁ i, \text{Set.mem_range_self } i \rangle$ is equal to the $(k,i)$-th entry of the matrix representation of $f$ with respect to the original basis $v₁$. That is, \[ (\text{toMatrixAlgEquiv } v₁.\text{reindexRange } f)_{\langle v₁ k, \cdot \rangle, \langle v₁ i, \cdot \rangle} = (\text{toMatrixAlgEquiv } v₁ f)_{k,i}. \]

LinearMap.toMatrixAlgEquiv_comp theorem

 (f g : M₁ →ₗ[R] M₁) :
  LinearMap.toMatrixAlgEquiv v₁ (f.comp g) = LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g

Full source

theorem LinearMap.toMatrixAlgEquiv_comp (f g : M₁ →ₗ[R] M₁) :
    LinearMap.toMatrixAlgEquiv v₁ (f.comp g) =
      LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g := by
  simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

Matrix Representation of Composition of Linear Endomorphisms: $\text{toMatrixAlgEquiv}(f \circ g) = \text{toMatrixAlgEquiv}(f) \cdot \text{toMatrixAlgEquiv}(g)$

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$. For any two linear endomorphisms $f, g : M₁ \to M₁$, the matrix representation of the composition $f \circ g$ with respect to the basis $v₁$ is equal to the product of the matrix representations of $f$ and $g$ with respect to $v₁$, i.e., \[ \text{toMatrixAlgEquiv}_{v₁}(f \circ g) = \text{toMatrixAlgEquiv}_{v₁}(f) \cdot \text{toMatrixAlgEquiv}_{v₁}(g). \]

LinearMap.toMatrixAlgEquiv_mul theorem

 (f g : M₁ →ₗ[R] M₁) :
  LinearMap.toMatrixAlgEquiv v₁ (f * g) = LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g

Full source

theorem LinearMap.toMatrixAlgEquiv_mul (f g : M₁ →ₗ[R] M₁) :
    LinearMap.toMatrixAlgEquiv v₁ (f * g) =
      LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g := by
  rw [Module.End.mul_eq_comp, LinearMap.toMatrixAlgEquiv_comp v₁ f g]

Matrix Representation of Product of Linear Endomorphisms: $\text{toMatrixAlgEquiv}(f * g) = \text{toMatrixAlgEquiv}(f) \cdot \text{toMatrixAlgEquiv}(g)$

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$. For any two linear endomorphisms $f, g : M₁ \to M₁$, the matrix representation of the product $f * g$ with respect to the basis $v₁$ is equal to the product of the matrix representations of $f$ and $g$ with respect to $v₁$, i.e., \[ \text{toMatrixAlgEquiv}_{v₁}(f * g) = \text{toMatrixAlgEquiv}_{v₁}(f) \cdot \text{toMatrixAlgEquiv}_{v₁}(g). \]

Matrix.toLinAlgEquiv_mul theorem

 (A B : Matrix n n R) : Matrix.toLinAlgEquiv v₁ (A * B) = (Matrix.toLinAlgEquiv v₁ A).comp (Matrix.toLinAlgEquiv v₁ B)

Full source

theorem Matrix.toLinAlgEquiv_mul (A B : Matrix n n R) :
    Matrix.toLinAlgEquiv v₁ (A * B) =
      (Matrix.toLinAlgEquiv v₁ A).comp (Matrix.toLinAlgEquiv v₁ B) := by
  convert Matrix.toLin_mul v₁ v₁ v₁ A B

Matrix Product to Linear Map Composition via Algebra Equivalence: $\text{toLinAlgEquiv}(AB) = \text{toLinAlgEquiv}(A) \circ \text{toLinAlgEquiv}(B)$

Informal description

Let $R$ be a commutative ring and $M₁$ be an $R$-module with a finite basis $v₁ : n \to M₁$. For any two square matrices $A, B \in \text{Matrix}_{n n}(R)$, the linear endomorphism corresponding to the matrix product $AB$ via $\text{Matrix.toLinAlgEquiv}_{v₁}$ is equal to the composition of the linear endomorphisms corresponding to $A$ and $B$ respectively, i.e., \[ \text{Matrix.toLinAlgEquiv}_{v₁}(AB) = (\text{Matrix.toLinAlgEquiv}_{v₁} A) \circ (\text{Matrix.toLinAlgEquiv}_{v₁} B). \]

Matrix.toLin_finTwoProd_apply theorem

 (a b c d : R) (x : R × R) :
  Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R) !![a, b; c, d] x =
    (a * x.fst + b * x.snd, c * x.fst + d * x.snd)

Full source

@[simp]
theorem Matrix.toLin_finTwoProd_apply (a b c d : R) (x : R × R) :
    Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R) !![a, b; c, d] x =
      (a * x.fst + b * x.snd, c * x.fst + d * x.snd) := by
  simp [Matrix.toLin_apply, Matrix.mulVec, dotProduct]

Action of $2 \times 2$ Matrix on $R \times R$ via Standard Basis

Informal description

For any elements $a, b, c, d \in R$ and any vector $x = (x_1, x_2) \in R \times R$, the linear map corresponding to the matrix $\begin{pmatrix} a & b \\ c & d \end{pmatrix}$ under the standard basis `Basis.finTwoProd R` evaluates at $x$ as: \[ \text{Matrix.toLin}(B_{\text{std}}, B_{\text{std}})\begin{pmatrix} a & b \\ c & d \end{pmatrix}(x) = (a x_1 + b x_2, c x_1 + d x_2), \] where $B_{\text{std}}$ denotes the standard basis of $R \times R$ consisting of $(1, 0)$ and $(0, 1)$.

Matrix.toLin_finTwoProd theorem

 (a b c d : R) :
  Matrix.toLin (Basis.finTwoProd R) (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)

Full source

theorem Matrix.toLin_finTwoProd (a b c d : R) :
    Matrix.toLin (Basis.finTwoProd R) (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) :=
  LinearMap.ext <| Matrix.toLin_finTwoProd_apply _ _ _ _

Matrix-to-Linear-Map Decomposition for $2 \times 2$ Matrices under Standard Basis

Informal description

For any elements $a, b, c, d$ in a commutative ring $R$, the linear map corresponding to the $2 \times 2$ matrix $\begin{pmatrix} a & b \\ c & d \end{pmatrix}$ under the standard basis of $R \times R$ is equal to the product of the linear maps $(a \cdot \pi_1 + b \cdot \pi_2)$ and $(c \cdot \pi_1 + d \cdot \pi_2)$, where $\pi_1$ and $\pi_2$ are the first and second projection maps from $R \times R$ to $R$.

toMatrix_distrib_mul_action_toLinearMap theorem

(x : R) : LinearMap.toMatrix v₁ v₁ (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun _ ↦ x

Full source

@[simp]
theorem toMatrix_distrib_mul_action_toLinearMap (x : R) :
    LinearMap.toMatrix v₁ v₁ (DistribMulAction.toLinearMap R M₁ x) =
    Matrix.diagonal fun _ ↦ x := by
  ext
  rw [LinearMap.toMatrix_apply, DistribMulAction.toLinearMap_apply, LinearEquiv.map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]

Matrix Representation of Scalar Multiplication is Diagonal Matrix with Constant Entries

Informal description

Let $R$ be a commutative ring and $M_1$ be an $R$-module with a finite basis $v_1$. For any element $x \in R$, the matrix representation of the scalar multiplication map $M_1 \to M_1$ (given by $m \mapsto x \cdot m$) with respect to the basis $v_1$ is the diagonal matrix with all diagonal entries equal to $x$. In other words, if we denote the scalar multiplication map by $\varphi_x$, then: \[ \text{LinearMap.toMatrix } v_1 v_1 \varphi_x = \text{diagonal}(\lambda \_. x) \] where $\text{diagonal}(\lambda \_. x)$ denotes the diagonal matrix with all diagonal entries equal to $x$.

LinearMap.toMatrix_prodMap theorem

 [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₂ φ₂)

Full source

lemma LinearMap.toMatrix_prodMap [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₂ φ₂) := by
  ext (i|i) (j|j) <;> simp [toMatrix]

Matrix Representation of Product Map as Block Diagonal Matrix

Informal description

Let $R$ be a commutative ring, and let $M_1$ and $M_2$ be $R$-modules with finite bases $v_1$ and $v_2$ indexed by types $n$ and $m$ respectively. For any endomorphisms $\varphi_1 \colon M_1 \to M_1$ and $\varphi_2 \colon M_2 \to M_2$, the matrix representation of the product map $\varphi_1 \times \varphi_2 \colon M_1 \times M_2 \to M_1 \times M_2$ with respect to the product basis $v_1 \times v_2$ is given by the block diagonal matrix \[ \begin{pmatrix} A & 0 \\ 0 & B \end{pmatrix}, \] where $A$ is the matrix representation of $\varphi_1$ with respect to $v_1$ and $B$ is the matrix representation of $\varphi_2$ with respect to $v_2$.

Algebra.toMatrix_lmul' theorem

(x : S) (i j) : LinearMap.toMatrix b b (lmul R S x) i j = b.repr (x * b j) i

Full source

theorem toMatrix_lmul' (x : S) (i j) :
    LinearMap.toMatrix b b (lmul R S x) i j = b.repr (x * b j) i := by
  simp only [LinearMap.toMatrix_apply', coe_lmul_eq_mul, LinearMap.mul_apply']

Matrix Entry Formula for Left Multiplication in Algebra Basis

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with a finite basis $b$ indexed by a finite type, and $x \in S$. For any indices $i$ and $j$, the $(i,j)$-th entry of the matrix representation of the left multiplication map $y \mapsto x \cdot y$ with respect to the basis $b$ is equal to the $i$-th coordinate of $x \cdot b(j)$ in the basis $b$, i.e., \[ (\text{LinearMap.toMatrix } b b (\text{lmul } R S x))_{i,j} = b.\text{repr}(x \cdot b(j))_i. \]

Algebra.toMatrix_lsmul theorem

(x : R) : LinearMap.toMatrix b b (Algebra.lsmul R R S x) = Matrix.diagonal fun _ ↦ x

Full source

@[simp]
theorem toMatrix_lsmul (x : R) :
    LinearMap.toMatrix b b (Algebra.lsmul R R S x) = Matrix.diagonal fun _ ↦ x :=
  toMatrix_distrib_mul_action_toLinearMap b x

Matrix representation of scalar multiplication is diagonal with constant entries

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra, and $b$ a basis for $S$ as an $R$-module indexed by a finite type. For any $x \in R$, the matrix representation of the left scalar multiplication map $y \mapsto x \cdot y$ (where $y \in S$) with respect to the basis $b$ is the diagonal matrix with all diagonal entries equal to $x$. In other words, if we denote the left scalar multiplication map by $\varphi_x$, then: \[ \text{LinearMap.toMatrix}_b^b(\varphi_x) = \text{diagonal}(\lambda \_. x) \] where $\text{diagonal}(\lambda \_. x)$ denotes the diagonal matrix with all diagonal entries equal to $x$.

Algebra.leftMulMatrix definition

: S →ₐ[R] Matrix m m R

Full source

/-- `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.
-/
noncomputable def leftMulMatrix : S →ₐ[R] Matrix m m R where
  toFun x := LinearMap.toMatrix b b (Algebra.lmul R S x)
  map_zero' := by
    rw [map_zero, LinearEquiv.map_zero]
  map_one' := by
    rw [map_one, LinearMap.toMatrix_one]
  map_add' x y := by
    rw [map_add, LinearEquiv.map_add]
  map_mul' x y := by
    rw [map_mul, LinearMap.toMatrix_mul]
  commutes' r := by
    ext
    rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.id.map_eq_self]

Matrix representation of left multiplication in an algebra

Informal description

Given a commutative ring $R$, an $R$-algebra $S$, and a basis $b$ for $S$ as an $R$-module indexed by a finite type $m$, the function $\text{leftMulMatrix } b$ maps an element $x \in S$ to the matrix representation of the left multiplication map $y \mapsto x \cdot y$ with respect to the basis $b$. This defines an $R$-algebra homomorphism from $S$ to the algebra of $m \times m$ matrices over $R$.

Algebra.leftMulMatrix_apply theorem

(x : S) : leftMulMatrix b x = LinearMap.toMatrix b b (lmul R S x)

Full source

theorem leftMulMatrix_apply (x : S) : leftMulMatrix b x = LinearMap.toMatrix b b (lmul R S x) :=
  rfl

Matrix Representation of Left Multiplication Equals Linear Map Matrix Representation

Informal description

Given a commutative ring $R$, an $R$-algebra $S$, a finite type $m$, and a basis $b$ for $S$ as an $R$-module indexed by $m$, for any element $x \in S$, the matrix representation of the left multiplication map $y \mapsto x \cdot y$ with respect to the basis $b$ is equal to the matrix representation of the linear map $\text{lmul}_R(S)(x)$ with respect to the basis $b$ on both the domain and codomain. In other words, the matrix $\text{leftMulMatrix}_b(x)$ satisfies $\text{leftMulMatrix}_b(x) = \text{LinearMap.toMatrix}_b^b(\text{lmul}_R(S)(x))$.

Algebra.leftMulMatrix_eq_repr_mul theorem

(x : S) (i j) : leftMulMatrix b x i j = b.repr (x * b j) i

Full source

theorem leftMulMatrix_eq_repr_mul (x : S) (i j) : leftMulMatrix b x i j = b.repr (x * b j) i := by
  -- This is defeq to just `toMatrix_lmul' b x i j`,
  -- but the unfolding goes a lot faster with this explicit `rw`.
  rw [leftMulMatrix_apply, toMatrix_lmul' b x i j]

Matrix Entry Formula for Left Multiplication: $(\text{leftMulMatrix}_b(x))_{i,j} = b.\text{repr}(x \cdot b(j))_i$

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with a basis $b$ indexed by a finite type, and $x \in S$. For any indices $i$ and $j$, the $(i,j)$-th entry of the left multiplication matrix of $x$ with respect to the basis $b$ equals the $i$-th coordinate of $x \cdot b(j)$ in the basis $b$. That is, \[ (\text{leftMulMatrix}_b(x))_{i,j} = b.\text{repr}(x \cdot b(j))_i. \]

Algebra.leftMulMatrix_mulVec_repr theorem

(x y : S) : leftMulMatrix b x *ᵥ b.repr y = b.repr (x * y)

Full source

theorem leftMulMatrix_mulVec_repr (x y : S) :
    leftMulMatrixleftMulMatrix b x *ᵥ b.repr y = b.repr (x * y) :=
  (LinearMap.mulLeft R x).toMatrix_mulVec_repr b b y

Matrix representation of left multiplication preserves product via matrix-vector multiplication

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with a basis $b$ indexed by a finite type, and $x, y \in S$. Then the matrix-vector product of the left multiplication matrix of $x$ (with respect to $b$) and the coordinate vector of $y$ (with respect to $b$) equals the coordinate vector of $x \cdot y$ (with respect to $b$). In symbols: $$\text{leftMulMatrix}_b(x) \cdot \text{repr}_b(y) = \text{repr}_b(x \cdot y)$$

Algebra.toMatrix_lmul_eq theorem

(x : S) : LinearMap.toMatrix b b (LinearMap.mulLeft R x) = leftMulMatrix b x

Full source

@[simp]
theorem toMatrix_lmul_eq (x : S) :
    LinearMap.toMatrix b b (LinearMap.mulLeft R x) = leftMulMatrix b x :=
  rfl

Matrix Representation of Left Multiplication Equals Left Multiplication Matrix

Informal description

For any element $x$ in an $R$-algebra $S$ with a basis $b$, the matrix representation of the left multiplication map $y \mapsto x \cdot y$ with respect to the basis $b$ is equal to the left multiplication matrix of $x$ in the basis $b$. That is, $\text{LinearMap.toMatrix } b b (\text{LinearMap.mulLeft } R x) = \text{leftMulMatrix } b x$.

Algebra.leftMulMatrix_injective theorem

: Function.Injective (leftMulMatrix b)

Full source

theorem leftMulMatrix_injective : Function.Injective (leftMulMatrix b) := fun x x' h ↦
  calc
    x = Algebra.lmul R S x 1 := (mul_one x).symm
    _ = Algebra.lmul R S x' 1 := by rw [(LinearMap.toMatrix b b).injective h]
    _ = x' := mul_one x'

Injectivity of Left Multiplication Matrix Representation

Informal description

The map sending an element $x$ of an $R$-algebra $S$ to the matrix representation of left multiplication by $x$ with respect to a basis $b$ is injective. In other words, if two elements $x, y \in S$ have the same left multiplication matrix representation, then $x = y$.

Algebra.smul_leftMulMatrix theorem

 {G} [Group G] [DistribMulAction G S] [SMulCommClass G R S] [SMulCommClass G S S] (g : G) (x) :
  leftMulMatrix (g • b) x = leftMulMatrix b x

Full source

@[simp]
theorem smul_leftMulMatrix {G} [Group G] [DistribMulAction G S]
    [SMulCommClass G R S] [SMulCommClass G S S] (g : G) (x) :
    leftMulMatrix (g • b) x = leftMulMatrix b x := by
  ext
  simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply',
    Basis.repr_smul, Basis.smul_apply, LinearEquiv.trans_apply,
    DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]

Invariance of Left Multiplication Matrix under Basis Scaling by Group Action

Informal description

Let $G$ be a group acting distributively on an $R$-algebra $S$, with actions commuting with both the $R$-action and the $S$-action on itself. For any $g \in G$ and $x \in S$, the left multiplication matrix representation of $x$ with respect to the scaled basis $g \cdot b$ is equal to its left multiplication matrix representation with respect to the original basis $b$. That is, \[ \text{leftMulMatrix}(g \cdot b)(x) = \text{leftMulMatrix}(b)(x). \]

LinearMap.restrictScalars_toMatrix theorem

 (f : M →ₗ[A] M) :
  (f.restrictScalars R).toMatrix (bA.smulTower' bM) (bA.smulTower' bM) =
    ((f.toMatrix bM bM).map (leftMulMatrix bA)).comp _ _ _ _ _

Full source

lemma _root_.LinearMap.restrictScalars_toMatrix (f : M →ₗ[A] M) :
    (f.restrictScalars R).toMatrix (bA.smulTower' bM) (bA.smulTower' bM) =
      ((f.toMatrix bM bM).map (leftMulMatrix bA)).comp _ _ _ _ _ := by
  ext; simp [toMatrix, Basis.repr, Algebra.leftMulMatrix_apply,
    Basis.smulTower'_repr, Basis.smulTower'_apply, mul_comm]

Matrix Representation of Scalar-Restricted Linear Map via Tensor Product Basis

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $A$-module with a basis $b_M$. Let $b_A$ be a basis for $A$ as an $R$-module. For any $A$-linear map $f : M \to M$, the matrix representation of $f$ restricted to $R$ with respect to the basis $b_A \otimes b_M$ is equal to the block matrix obtained by applying the left multiplication matrix representation (with respect to $b_A$) to each entry of the matrix representation of $f$ (with respect to $b_M$), followed by a flattening operation.

Algebra.smulTower_leftMulMatrix theorem

(x) (ik jk) : leftMulMatrix (b.smulTower c) x ik jk = leftMulMatrix b (leftMulMatrix c x ik.2 jk.2) ik.1 jk.1

Full source

theorem smulTower_leftMulMatrix (x) (ik jk) :
    leftMulMatrix (b.smulTower c) x ik jk =
      leftMulMatrix b (leftMulMatrix c x ik.2 jk.2) ik.1 jk.1 := by
  simp only [leftMulMatrix_apply, LinearMap.toMatrix_apply, mul_comm, Basis.smulTower_apply,
    Basis.smulTower_repr, Finsupp.smul_apply, id.smul_eq_mul, LinearEquiv.map_smul, mul_smul_comm,
    coe_lmul_eq_mul, LinearMap.mul_apply']

Matrix Decomposition of Left Multiplication in Tensor Product Algebra

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with basis $b$ indexed by $m$, and $A$ another $R$-algebra with basis $c$ indexed by $n$. For any $x \in S$ and indices $(i,k), (j,k) \in m \times n$, the $(i,k),(j,k)$-entry of the left multiplication matrix of $x$ with respect to the tensor product basis $b \otimes c$ equals the $(i,j)$-entry of the left multiplication matrix of $x$ with respect to $b$ multiplied by the $(k,k)$-entry of the left multiplication matrix of $x$ with respect to $c$. In other words, \[ \text{leftMulMatrix}(b \otimes c)(x)_{(i,k),(j,k)} = \text{leftMulMatrix}(b)(x)_{i,j} \cdot \text{leftMulMatrix}(c)(x)_{k,k}. \]

Algebra.smulTower_leftMulMatrix_algebraMap theorem

(x : S) : leftMulMatrix (b.smulTower c) (algebraMap _ _ x) = blockDiagonal fun _ ↦ leftMulMatrix b x

Full source

theorem smulTower_leftMulMatrix_algebraMap (x : S) :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) = blockDiagonal fun _ ↦ leftMulMatrix b x := by
  ext ⟨i, k⟩ ⟨j, k'⟩
  rw [smulTower_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]
  split_ifs with h <;> simp only at h <;> simp [h]

Block Diagonal Matrix Representation of Left Multiplication in Tensor Product Algebra via Algebra Map

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with basis $b$ indexed by a finite type $m$, and $A$ another $R$-algebra with basis $c$ indexed by a finite type $n$. For any $x \in S$, the matrix representation of the left multiplication by $\text{algebraMap } S (S \otimes_R A) x$ with respect to the tensor product basis $b \otimes c$ is equal to the block diagonal matrix where each diagonal block is the matrix representation of left multiplication by $x$ with respect to the basis $b$. In other words, \[ \text{leftMulMatrix}(b \otimes c)(\text{algebraMap } S (S \otimes_R A) x) = \text{blockDiagonal } (\lambda \_ \mapsto \text{leftMulMatrix } b x). \]

Algebra.smulTower_leftMulMatrix_algebraMap_eq theorem

(x : S) (i j k) : leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k) = leftMulMatrix b x i j

Full source

theorem smulTower_leftMulMatrix_algebraMap_eq (x : S) (i j k) :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k) = leftMulMatrix b x i j := by
  rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_eq]

Equality of Diagonal Block Entries in Left Multiplication Matrix under Algebra Map

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with basis $b$ indexed by a finite type $m$, and $A$ another $R$-algebra with basis $c$ indexed by a finite type $n$. For any $x \in S$ and indices $i, j \in m$, $k \in n$, the $(i,k),(j,k)$-entry of the left multiplication matrix of $\text{algebraMap } S (S \otimes_R A) x$ with respect to the tensor product basis $b \otimes c$ equals the $(i,j)$-entry of the left multiplication matrix of $x$ with respect to the basis $b$. In other words, \[ \text{leftMulMatrix}(b \otimes c)(\text{algebraMap } S (S \otimes_R A) x)_{(i,k),(j,k)} = \text{leftMulMatrix}(b)(x)_{i,j}. \]

Algebra.smulTower_leftMulMatrix_algebraMap_ne theorem

(x : S) (i j) {k k'} (h : k ≠ k') : leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k') = 0

Full source

theorem smulTower_leftMulMatrix_algebraMap_ne (x : S) (i j) {k k'} (h : k ≠ k') :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k') = 0 := by
  rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_ne _ _ _ h]

Vanishing of Off-Diagonal Block Entries in Left Multiplication Matrix under Algebra Map

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra with basis $b$ indexed by a finite type $m$, and $A$ another $R$-algebra with basis $c$ indexed by a finite type $n$. For any $x \in S$, indices $i, j \in m$, and distinct indices $k \neq k' \in n$, the $(i,k),(j,k')$-entry of the left multiplication matrix of $\text{algebraMap } S (S \otimes_R A) x$ with respect to the tensor product basis $b \otimes c$ is zero. In other words, \[ \text{leftMulMatrix}(b \otimes c)(\text{algebraMap } S (S \otimes_R A) x)_{(i,k),(j,k')} = 0. \]

algEquivMatrix' definition

[Fintype n] : Module.End R (n → R) ≃ₐ[R] Matrix n n R

Full source

/-- The natural equivalence between linear endomorphisms of finite free modules and square matrices
is compatible with the algebra structures. -/
def algEquivMatrix' [Fintype n] : Module.EndModule.End R (n → R) ≃ₐ[R] Matrix n n R :=
  { LinearMap.toMatrix' with
    map_mul' := LinearMap.toMatrix'_comp
    commutes' := LinearMap.toMatrix'_algebraMap }

Algebra equivalence between endomorphisms and square matrices

Informal description

The algebra equivalence between the endomorphism algebra of the free module $n \to R$ and the algebra of $n \times n$ matrices over a commutative ring $R$. This equivalence maps a linear endomorphism $f$ to its matrix representation with respect to the standard basis, and preserves both the multiplicative and additive structures, as well as the action of scalars.

LinearEquiv.algConj definition

(e : M₁ ≃ₗ[S] M₂) : Module.End S M₁ ≃ₐ[R] Module.End S M₂

Full source

/-- A linear equivalence of two modules induces an equivalence of algebras of their
endomorphisms. -/
@[simps!] def LinearEquiv.algConj (e : M₁ ≃ₗ[S] M₂) : Module.EndModule.End S M₁ ≃ₐ[R] Module.End S M₂ where
  __ := e.conjRingEquiv
  commutes' := fun _ ↦ by ext; show e.restrictScalars R _ = _; simp

Conjugation of endomorphism algebras by a linear equivalence

Informal description

Given a linear equivalence $e : M_1 \simeq_{S} M_2$ between $S$-modules $M_1$ and $M_2$, the map $\text{algConj}(e)$ is an $R$-algebra equivalence between the endomorphism algebras $\text{End}_S(M_1)$ and $\text{End}_S(M_2)$. This equivalence is induced by conjugation with $e$, i.e., for any endomorphism $f \in \text{End}_S(M_1)$, the corresponding endomorphism in $\text{End}_S(M_2)$ is given by $e \circ f \circ e^{-1}$.

algEquivMatrix definition

[Fintype n] (h : Basis n R M) : Module.End R M ≃ₐ[R] Matrix n n R

Full source

/-- A basis of a module induces an equivalence of algebras from the endomorphisms of the module to
square matrices. -/
def algEquivMatrix [Fintype n] (h : Basis n R M) : Module.EndModule.End R M ≃ₐ[R] Matrix n n R :=
  (h.equivFun.algConj R).trans algEquivMatrix'

Algebra equivalence between endomorphisms and matrices via a basis

Informal description

Given a commutative ring $R$, a finite type $n$, and a basis $h : \text{Basis } n R M$ for an $R$-module $M$, the algebra equivalence $\text{algEquivMatrix } h$ maps an $R$-linear endomorphism of $M$ to its matrix representation with respect to the basis $h$. This equivalence preserves the algebra structure, including addition, multiplication, and scalar multiplication.

Basis.linearMap definition

(b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) : Basis (ι₂ × ι₁) R (M₁ →ₗ[R] M₂)

Full source

/-- 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`. -/
@[simps! -isSimp repr_apply repr_symm_apply]
noncomputable
def linearMap (b₁ : Basis ι₁ R M₁) (b₂ : Basis ι₂ R M₂) :
    Basis (ι₂ × ι₁) R (M₁ →ₗ[R] M₂) :=
  (Matrix.stdBasis R ι₂ ι₁).map (LinearMap.toMatrix b₁ b₂).symm

Basis of linear maps between modules

Informal description

Given a commutative ring $R$ and two $R$-modules $M₁$ and $M₂$ with bases $b₁ : ι₁ → M₁$ and $b₂ : ι₂ → M₂$ respectively, the function $\text{Basis.linearMap } b₁ b₂$ constructs a basis for the space of linear maps $M₁ →ₗ[R] M₂$ indexed by $ι₂ × ι₁$. For each pair $(i,j) ∈ ι₂ × ι₁$, the corresponding basis vector is the linear map that sends $b₁(j)$ to $b₂(i)$ and all other basis vectors of $b₁$ to $0$. This basis is obtained by transforming the standard basis of matrices via the linear equivalence $\text{LinearMap.toMatrix } b₁ b₂$.

Basis.linearMap_apply theorem

(ij : ι₂ × ι₁) : (b₁.linearMap b₂ ij) = (Matrix.toLin b₁ b₂) (Matrix.stdBasis R ι₂ ι₁ ij)

Full source

lemma linearMap_apply (ij : ι₂ × ι₁) :
    (b₁.linearMap b₂ ij) = (Matrix.toLin b₁ b₂) (Matrix.stdBasis R ι₂ ι₁ ij) := by
  simp [linearMap]

Basis Vector of Linear Maps as Matrix-to-Linear-Map Transformation

Informal description

Given a commutative ring $R$, two $R$-modules $M_1$ and $M_2$ with bases $b_1 : \iota_1 \to M_1$ and $b_2 : \iota_2 \to M_2$ respectively, and an index pair $(i,j) \in \iota_2 \times \iota_1$, the basis vector $(b_1.\text{linearMap } b_2)(i,j)$ of the space of linear maps $M_1 \to M_2$ is equal to the linear map obtained by applying the matrix-to-linear-map equivalence $\text{Matrix.toLin } b_1 b_2$ to the standard basis matrix $\text{Matrix.stdBasis } R \iota_2 \iota_1 (i,j)$.

Basis.linearMap_apply_apply theorem

(ij : ι₂ × ι₁) (k : ι₁) : (b₁.linearMap b₂ ij) (b₁ k) = if ij.2 = k then b₂ ij.1 else 0

Full source

lemma linearMap_apply_apply (ij : ι₂ × ι₁) (k : ι₁) :
    (b₁.linearMap b₂ ij) (b₁ k) = if ij.2 = k then b₂ ij.1 else 0 := by
  have := Classical.decEq ι₂
  rw [linearMap_apply, Matrix.stdBasis_eq_stdBasisMatrix, Matrix.toLin_self]
  dsimp only [Matrix.stdBasisMatrix, of_apply]
  simp_rw [ite_smul, one_smul, zero_smul, ite_and, Finset.sum_ite_eq, Finset.mem_univ, if_true]

Action of Basis Linear Map on Basis Vectors: $(b_1.\text{linearMap } b_2)(i,j)(b_1(k)) = \delta_{j,k} b_2(i)$

Informal description

Let $R$ be a commutative ring, and let $M_1$ and $M_2$ be $R$-modules with bases $b_1 : \iota_1 \to M_1$ and $b_2 : \iota_2 \to M_2$ respectively. For any pair of indices $(i,j) \in \iota_2 \times \iota_1$ and any basis vector $b_1(k) \in M_1$, the action of the basis linear map $(b_1.\text{linearMap } b_2)(i,j)$ on $b_1(k)$ is given by: \[ (b_1.\text{linearMap } b_2)(i,j)(b_1(k)) = \begin{cases} b_2(i) & \text{if } j = k, \\ 0 & \text{otherwise.} \end{cases} \]

Basis.end abbrev

(b : Basis ι R M) : Basis (ι × ι) R (Module.End R M)

Full source

/-- 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`. -/
@[simps! -isSimp repr_apply repr_symm_apply]
noncomputable
abbrev _root_.Basis.end (b : Basis ι R M) : Basis (ι × ι) R (Module.End R M) :=
  b.linearMap b

Standard Basis for Endomorphism Algebra via Module Basis

Informal description

Given a commutative ring $R$ and an $R$-module $M$ with a basis $b : \iota \to M$, the function $\text{Basis.end } b$ constructs a basis for the endomorphism algebra $\text{End}_R(M)$ indexed by $\iota \times \iota$. For each pair $(i,j) \in \iota \times \iota$, the corresponding basis vector is the linear map that sends $b(j)$ to $b(i)$ and all other basis vectors to $0$.

Basis.end_apply theorem

(ij : ι × ι) : (b.end ij) = (Matrix.toLin b b) (Matrix.stdBasis R ι ι ij)

Full source

lemma end_apply (ij : ι × ι) : (b.end ij) = (Matrix.toLin b b) (Matrix.stdBasis R ι ι ij) :=
  linearMap_apply b b ij

Endomorphism Basis Vector as Matrix-to-Linear-Map Transformation

Informal description

Given a commutative ring $R$, an $R$-module $M$ with basis $b : \iota \to M$, and any pair of indices $(i,j) \in \iota \times \iota$, the basis vector $(b.\text{end})(i,j)$ of the endomorphism algebra $\text{End}_R(M)$ is equal to the linear map obtained by applying the matrix-to-linear-map equivalence $\text{Matrix.toLin } b b$ to the standard basis matrix $\text{Matrix.stdBasis } R \iota \iota (i,j)$.

Basis.end_apply_apply theorem

(ij : ι × ι) (k : ι) : (b.end ij) (b k) = if ij.2 = k then b ij.1 else 0

Full source

lemma end_apply_apply (ij : ι × ι) (k : ι) : (b.end ij) (b k) = if ij.2 = k then b ij.1 else 0 :=
  linearMap_apply_apply b b ij k

Action of Endomorphism Basis Vector on Module Basis: $(b.\text{end})(i,j)(b(k)) = \delta_{j,k} b(i)$

Informal description

Let $R$ be a commutative ring and $M$ an $R$-module with basis $b : \iota \to M$. For any pair of indices $(i,j) \in \iota \times \iota$ and any basis vector $b(k) \in M$, the action of the endomorphism basis vector $(b.\text{end})(i,j)$ on $b(k)$ is given by: \[ (b.\text{end})(i,j)(b(k)) = \begin{cases} b(i) & \text{if } j = k, \\ 0 & \text{otherwise.} \end{cases} \]

endVecRingEquivMatrixEnd definition

: Module.End A (ι → M) ≃+* Matrix ι ι (Module.End A M)

Full source

/--
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'`
-/
@[simp]
def endVecRingEquivMatrixEnd :
    Module.EndModule.End A (ι → M) ≃+* Matrix ι ι (Module.End A M) where
  toFun f i j :=
  { toFun := fun x ↦ f (Pi.single j x) i
    map_add' := fun x y ↦ by simp [Pi.single_add]
    map_smul' := fun x y ↦ by simp [Pi.single_smul] }
  invFun m :=
  { toFun := fun x i ↦ ∑ j, m i j (x j)
    map_add' := by intros; ext; simp [Finset.sum_add_distrib]
    map_smul' := by intros; ext; simp [Finset.smul_sum] }
  left_inv f := by
    ext i x j
    simp only [LinearMap.coe_mk, AddHom.coe_mk, coe_comp, coe_single, Function.comp_apply]
    rw [← Fintype.sum_apply, ← map_sum]
    exact congr_arg₂ _ (by aesop) rfl
  right_inv m := by ext; simp [Pi.single_apply, apply_ite]
  map_mul' f g := by
    ext
    simp only [Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, Matrix.mul_apply, coeFn_sum,
      Finset.sum_apply]
    rw [← Fintype.sum_apply, ← map_sum]
    exact congr_arg₂ _ (by aesop) rfl
  map_add' f g := by ext; simp

Ring isomorphism between endomorphisms of $M^n$ and matrices of endomorphisms of $M$

Informal description

Given a commutative ring $A$ and an $A$-module $M$, there is a ring isomorphism between the endomorphism ring of the module $M^n$ (where $n$ is the cardinality of a finite index set $\iota$) and the ring of $\iota \times \iota$ matrices with entries in the endomorphism ring of $M$. The isomorphism is defined by: - For an endomorphism $f$ of $M^n$, the corresponding matrix has entries $(i,j) \mapsto (x \mapsto f(0, \ldots, x \text{ at position } j, \ldots, 0)_i)$. - For a matrix $m$ of endomorphisms, the corresponding endomorphism of $M^n$ maps a vector $v$ to the vector whose $i$-th component is $\sum_j m_{i j}(v_j)$.

endVecAlgEquivMatrixEnd definition

: Module.End A (ι → M) ≃ₐ[R] Matrix ι ι (Module.End A M)

Full source

/--
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'`
-/
@[simps!]
def endVecAlgEquivMatrixEnd :
    Module.EndModule.End A (ι → M) ≃ₐ[R] Matrix ι ι (Module.End A M) where
  __ := endVecRingEquivMatrixEnd ι A M
  commutes' r := by
    ext
    simp only [endVecRingEquivMatrixEnd, RingEquiv.toEquiv_eq_coe, Module.algebraMap_end_eq_smul_id,
      Equiv.toFun_as_coe, EquivLike.coe_coe, RingEquiv.coe_mk, Equiv.coe_fn_mk,
      LinearMap.smul_apply, id_coe, id_eq, Pi.smul_apply, Pi.single_apply, smul_ite, smul_zero,
      LinearMap.coe_mk, AddHom.coe_mk, algebraMap_matrix_apply]
    split_ifs <;> rfl

Algebra isomorphism between endomorphisms of $M^n$ and matrices of endomorphisms of $M$

Informal description

Given a commutative ring $R$, a commutative $R$-algebra $A$, and an $A$-module $M$, there is an $R$-algebra isomorphism between the endomorphism algebra of the module $M^n$ (where $n$ is the cardinality of a finite index set $\iota$) and the algebra of $\iota \times \iota$ matrices with entries in the endomorphism algebra of $M$. The isomorphism is defined by: - For an endomorphism $f$ of $M^n$, the corresponding matrix has entries $(i,j) \mapsto (x \mapsto f(0, \ldots, x \text{ at position } j, \ldots, 0)_i)$. - For a matrix $m$ of endomorphisms, the corresponding endomorphism of $M^n$ maps a vector $v$ to the vector whose $i$-th component is $\sum_j m_{i j}(v_j)$.

Mathlib.LinearAlgebra.Matrix.ToLin

Main definitions

Issues

Tags