Mathlib.LinearAlgebra.Matrix.Basis

Basis.toMatrix definition

(e : Basis ι R M) (v : ι' → M) : Matrix ι ι' R

Full source

/-- From a basis `e : ι → M` and a family of vectors `v : ι' → M`, make the matrix whose columns
are the vectors `v i` written in the basis `e`. -/
def Basis.toMatrix (e : Basis ι R M) (v : ι' → M) : Matrix ι ι' R := fun i j => e.repr (v j) i

Matrix of coordinates with respect to a basis

Informal description

Given a basis $ e : \iota \to M $ of a module $ M $ over a ring $ R $ and a family of vectors $ v : \iota' \to M $, the matrix $ \text{Basis.toMatrix } e \ v $ is defined such that its entry at position $ (i, j) $ is the $ i $-th coordinate of the vector $ v_j $ with respect to the basis $ e $. In other words, $ \text{Basis.toMatrix } e \ v $ represents the coordinates of the vectors $ v $ in the basis $ e $.

Basis.toMatrix_apply theorem

: e.toMatrix v i j = e.repr (v j) i

Full source

theorem toMatrix_apply : e.toMatrix v i j = e.repr (v j) i :=
  rfl

Matrix Entry Formula for Basis Coordinates

Informal description

For a basis $e$ of a module $M$ over a ring $R$, a family of vectors $v \colon \iota' \to M$, and indices $i \in \iota$, $j \in \iota'$, the $(i,j)$-th entry of the matrix $\text{Basis.toMatrix } e \ v$ is equal to the $i$-th coordinate of the vector $v_j$ with respect to the basis $e$. That is, \[ (e.\text{toMatrix } v)_{i,j} = e.\text{repr } (v_j)_i. \]

Basis.toMatrix_transpose_apply theorem

: (e.toMatrix v)ᵀ j = e.repr (v j)

Full source

theorem toMatrix_transpose_apply : (e.toMatrix v)ᵀ j = e.repr (v j) :=
  funext fun _ => rfl

Transpose of Coordinate Matrix Represents Vector Coordinates

Informal description

For a basis $e$ of a module $M$ over a ring $R$ and a family of vectors $v : \iota' \to M$, the transpose of the coordinate matrix $(e.\text{toMatrix } v)^\top$ has its $j$-th column equal to the coordinate representation $e.\text{repr } (v j)$ of the vector $v j$ with respect to the basis $e$.

Basis.toMatrix_eq_toMatrix_constr theorem

[Fintype ι] [DecidableEq ι] (v : ι → M) : e.toMatrix v = LinearMap.toMatrix e e (e.constr ℕ v)

Full source

theorem toMatrix_eq_toMatrix_constr [Fintype ι] [DecidableEq ι] (v : ι → M) :
    e.toMatrix v = LinearMap.toMatrix e e (e.constr ℕ v) := by
  ext
  rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]

Equality of Coordinate Matrix and Linear Map Matrix Representation

Informal description

Let $M$ be a module over a ring $R$ with a basis $e$ indexed by a finite type $\iota$ with decidable equality. For any family of vectors $v \colon \iota \to M$, the coordinate matrix $\text{Basis.toMatrix } e \ v$ is equal to the matrix representation of the linear map $\text{constr}_e^\mathbb{N} v$ with respect to the basis $e$ on both the domain and codomain. That is, \[ e.\text{toMatrix } v = \text{LinearMap.toMatrix } e \ e \ (e.\text{constr } \mathbb{N} \ v). \]

Basis.coePiBasisFun.toMatrix_eq_transpose theorem

[Finite ι] : ((Pi.basisFun R ι).toMatrix : Matrix ι ι R → Matrix ι ι R) = Matrix.transpose

Full source

theorem coePiBasisFun.toMatrix_eq_transpose [Finite ι] :
    ((Pi.basisFun R ι).toMatrix : Matrix ι ι R → Matrix ι ι R) = Matrix.transpose := by
  ext M i j
  rfl

Standard Basis Matrix Representation Equals Transpose

Informal description

For a finite index set $\iota$ and a ring $R$, the matrix representation of the standard basis vectors $\{e_i\}_{i \in \iota}$ (where $e_i(j) = \delta_{ij}$) with respect to themselves is equal to the transpose operation on matrices. That is, the map sending a matrix to its coordinate representation in the standard basis is equivalent to the transpose operation.

Basis.toMatrix_self theorem

[DecidableEq ι] : e.toMatrix e = 1

Full source

@[simp]
theorem toMatrix_self [DecidableEq ι] : e.toMatrix e = 1 := by
  unfold Basis.toMatrix
  ext i j
  simp [Basis.equivFun, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Identity Matrix Representation of Basis with Respect to Itself

Informal description

For any basis $e$ of a module $M$ over a ring $R$ indexed by a type $\iota$ with decidable equality, the matrix of coordinates of the basis vectors $e$ with respect to themselves is the identity matrix, i.e., $e.\text{toMatrix}(e) = 1$.

Basis.toMatrix_update theorem

[DecidableEq ι'] (x : M) : e.toMatrix (Function.update v j x) = Matrix.updateCol (e.toMatrix v) j (e.repr x)

Full source

theorem toMatrix_update [DecidableEq ι'] (x : M) :
    e.toMatrix (Function.update v j x) = Matrix.updateCol (e.toMatrix v) j (e.repr x) := by
  ext i' k
  rw [Basis.toMatrix, Matrix.updateCol_apply, e.toMatrix_apply]
  split_ifs with h
  · rw [h, update_self j x v]
  · rw [update_of_ne h]

Matrix Update Formula for Basis Coordinates under Vector Replacement

Informal description

Let $e$ be a basis for a module $M$ over a ring $R$, indexed by $\iota$, and let $v \colon \iota' \to M$ be a family of vectors in $M$. For any vector $x \in M$ and index $j \in \iota'$, the matrix of coordinates of the updated family $\text{update } v \ j \ x$ with respect to $e$ is equal to the matrix obtained by updating the $j$-th column of the coordinate matrix $e.\text{toMatrix } v$ with the coordinates of $x$ in the basis $e$. That is, \[ e.\text{toMatrix } (\text{update } v \ j \ x) = \text{updateCol } (e.\text{toMatrix } v) \ j \ (e.\text{repr } x). \]

Basis.toMatrix_unitsSMul theorem

[DecidableEq ι] (e : Basis ι R₂ M₂) (w : ι → R₂ˣ) : e.toMatrix (e.unitsSMul w) = diagonal ((↑) ∘ w)

Full source

/-- The basis constructed by `unitsSMul` has vectors given by a diagonal matrix. -/
@[simp]
theorem toMatrix_unitsSMul [DecidableEq ι] (e : Basis ι R₂ M₂) (w : ι → R₂ˣ) :
    e.toMatrix (e.unitsSMul w) = diagonal ((↑) ∘ w) := by
  ext i j
  by_cases h : i = j
  · simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]
  · simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def, Ne.symm h]

Diagonal Matrix Representation of Unit-Scaled Basis Vectors: $e.\text{toMatrix}(e.\text{unitsSMul}\, w) = \text{diagonal}(w)$

Informal description

Let $e$ be a basis for a module $M$ over a ring $R$ indexed by a type $\iota$ with decidable equality, and let $w \colon \iota \to R^\times$ be a family of units in $R$. The matrix of coordinates of the basis vectors obtained by scaling $e$ with $w$ (i.e., the basis $e.\text{unitsSMul}\, w$) with respect to the original basis $e$ is the diagonal matrix whose $(i,i)$-th entry is the unit $w_i$. In mathematical notation: $$e.\text{toMatrix}(e.\text{unitsSMul}\, w) = \text{diagonal}(w).$$

Basis.toMatrix_isUnitSMul theorem

 [DecidableEq ι] (e : Basis ι R₂ M₂) {w : ι → R₂} (hw : ∀ i, IsUnit (w i)) : e.toMatrix (e.isUnitSMul hw) = diagonal w

Full source

/-- The basis constructed by `isUnitSMul` has vectors given by a diagonal matrix. -/
@[simp]
theorem toMatrix_isUnitSMul [DecidableEq ι] (e : Basis ι R₂ M₂) {w : ι → R₂}
    (hw : ∀ i, IsUnit (w i)) : e.toMatrix (e.isUnitSMul hw) = diagonal w :=
  e.toMatrix_unitsSMul _

Diagonal Matrix Representation of Unit-Scaled Basis Vectors: $e.\text{toMatrix}(e.\text{isUnitSMul}\, hw) = \text{diagonal}(w)$

Informal description

Let $e$ be a basis for a module $M$ over a ring $R$ indexed by a finite type $\iota$ with decidable equality, and let $w \colon \iota \to R$ be a family of elements in $R$ such that each $w_i$ is a unit. Then the matrix of coordinates of the basis vectors obtained by scaling $e$ with $w$ (i.e., the basis $e.\text{isUnitSMul}\, hw$) with respect to the original basis $e$ is the diagonal matrix whose $(i,i)$-th entry is $w_i$. In mathematical notation: $$e.\text{toMatrix}(e.\text{isUnitSMul}\, hw) = \text{diagonal}(w).$$

Basis.toMatrix_smul_left theorem

{G} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) : (g • e).toMatrix v = e.toMatrix (g⁻¹ • v)

Full source

theorem toMatrix_smul_left {G} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) :
    (g • e).toMatrix v = e.toMatrix (g⁻¹ • v) := rfl

Matrix of Coordinates under Scalar Multiplication of Basis Vectors

Informal description

Let $G$ be a group acting distributively on a module $M$ over a ring $R$, with the action commuting with scalar multiplication by $R$. For any basis $e$ of $M$ indexed by $\iota$, any family of vectors $v \colon \iota' \to M$, and any group element $g \in G$, the matrix of coordinates of the vectors $v$ with respect to the scaled basis $g \cdot e$ is equal to the matrix of coordinates of the vectors $g^{-1} \cdot v$ with respect to the original basis $e$. In other words, $$(g \cdot e).\text{toMatrix}(v) = e.\text{toMatrix}(g^{-1} \cdot v).$$

Basis.sum_toMatrix_smul_self theorem

[Fintype ι] : ∑ i : ι, e.toMatrix v i j • e i = v j

Full source

@[simp]
theorem sum_toMatrix_smul_self [Fintype ι] : ∑ i : ι, e.toMatrix v i j • e i = v j := by
  simp_rw [e.toMatrix_apply, e.sum_repr]

Reconstruction of Vector from Coordinate Matrix via Basis Summation

Informal description

Let $M$ be a module over a ring $R$ with a finite basis $e$ indexed by a finite type $\iota$. For any family of vectors $v \colon \iota' \to M$ and any index $j \in \iota'$, the sum $\sum_{i \in \iota} (e.\text{toMatrix } v)_{i,j} \cdot e_i$ equals $v_j$, where $(e.\text{toMatrix } v)_{i,j}$ denotes the $(i,j)$-th entry of the coordinate matrix of $v$ with respect to the basis $e$.

Basis.toMatrix_smul theorem

 {R₁ S : Type*} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] [Fintype ι] [DecidableEq ι] (x : S) (b : Basis ι R₁ S)
  (w : ι → S) : (b.toMatrix (x • w)) = (Algebra.leftMulMatrix b x) * (b.toMatrix w)

Full source

theorem toMatrix_smul {R₁ S : Type*} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] [Fintype ι]
    [DecidableEq ι] (x : S) (b : Basis ι R₁ S) (w : ι → S) :
    (b.toMatrix (x • w)) = (Algebra.leftMulMatrix b x) * (b.toMatrix w) := by
  ext
  rw [Basis.toMatrix_apply, Pi.smul_apply, smul_eq_mul, ← Algebra.leftMulMatrix_mulVec_repr]
  rfl

Matrix of Scaled Vectors as Product of Left Multiplication Matrix and Original Coordinate Matrix

Informal description

Let $R_1$ and $S$ be commutative semirings with $S$ also being an $R_1$-algebra via the algebra map $\text{algebraMap } R_1 S$. Let $\iota$ be a finite type with decidable equality, and let $b$ be a basis of $S$ as an $R_1$-module indexed by $\iota$. For any element $x \in S$ and any family of vectors $w \colon \iota \to S$, the matrix of coordinates of the scaled vectors $x \cdot w$ with respect to the basis $b$ is equal to the product of the left multiplication matrix of $x$ with respect to $b$ and the matrix of coordinates of $w$ with respect to $b$. That is, \[ b.\text{toMatrix}(x \cdot w) = (\text{Algebra.leftMulMatrix } b x) * (b.\text{toMatrix } w). \]

Basis.toMatrix_map_vecMul theorem

 {S : Type*} [Semiring S] [Algebra R S] [Fintype ι] (b : Basis ι R S) (v : ι' → S) :
  b ᵥ* ((b.toMatrix v).map <| algebraMap R S) = v

Full source

theorem toMatrix_map_vecMul {S : Type*} [Semiring S] [Algebra R S] [Fintype ι] (b : Basis ι R S)
    (v : ι' → S) : b ᵥ* ((b.toMatrix v).map <| algebraMap R S) = v := by
  ext i
  simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
    sum_toMatrix_smul_self]

Vector Reconstruction via Algebra Map and Coordinate Matrix Multiplication

Informal description

Let $R$ be a ring and $S$ a semiring with an $R$-algebra structure given by the algebra map $R \to S$. Let $\iota$ be a finite type and $b$ a basis of $S$ as an $R$-module indexed by $\iota$. For any family of vectors $v \colon \iota' \to S$, the vector-matrix multiplication of $b$ with the matrix obtained by applying the algebra map to each entry of the coordinate matrix $b.\text{toMatrix } v$ equals $v$. That is, \[ b \cdot \left(\text{map } (\text{algebraMap } R S) (b.\text{toMatrix } v)\right) = v, \] where $\cdot$ denotes the vector-matrix multiplication operation.

Basis.toLin_toMatrix theorem

[Finite ι] [Fintype ι'] [DecidableEq ι'] (v : Basis ι' R M) : Matrix.toLin v e (e.toMatrix v) = LinearMap.id

Full source

@[simp]
theorem toLin_toMatrix [Finite ι] [Fintype ι'] [DecidableEq ι'] (v : Basis ι' R M) :
    Matrix.toLin v e (e.toMatrix v) = LinearMap.id :=
  v.ext fun i => by cases nonempty_fintype ι; rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]

Coordinate Matrix Transformation Yields Identity Linear Map

Informal description

Let $M$ be a module over a ring $R$ with a basis $e$ indexed by a finite type $\iota$, and let $v$ be another basis of $M$ indexed by a finite type $\iota'$ with decidable equality. The linear map obtained by converting the coordinate matrix of $v$ with respect to $e$ (via `Matrix.toLin`) is equal to the identity linear map on $M$. In other words, the coordinate transformation from basis $v$ to basis $e$ acts as the identity when composed with its inverse transformation.

Basis.toMatrixEquiv definition

[Fintype ι] (e : Basis ι R M) : (ι → M) ≃ₗ[R] Matrix ι ι R

Full source

/-- From a basis `e : ι → M`, build a linear equivalence between families of vectors `v : ι → M`,
and matrices, making the matrix whose columns are the vectors `v i` written in the basis `e`. -/
def toMatrixEquiv [Fintype ι] (e : Basis ι R M) : (ι → M) ≃ₗ[R] Matrix ι ι R where
  toFun := e.toMatrix
  map_add' v w := by
    ext i j
    rw [Matrix.add_apply, e.toMatrix_apply, Pi.add_apply, LinearEquiv.map_add]
    rfl
  map_smul' := by
    intro c v
    ext i j
    dsimp only []
    rw [e.toMatrix_apply, Pi.smul_apply, LinearEquiv.map_smul]
    rfl
  invFun m j := ∑ i, m i j • e i
  left_inv := by
    intro v
    ext j
    exact e.sum_toMatrix_smul_self v j
  right_inv := by
    intro m
    ext k l
    simp only [e.toMatrix_apply, ← e.equivFun_apply, ← e.equivFun_symm_apply,
      LinearEquiv.apply_symm_apply]

Linear equivalence between families of vectors and coordinate matrices

Informal description

Given a finite basis $ e : \iota \to M $ of a module $ M $ over a ring $ R $, the linear equivalence `Basis.toMatrixEquiv e` maps a family of vectors $ v : \iota \to M $ to the matrix whose $(i,j)$-th entry is the $i$-th coordinate of $v_j$ with respect to the basis $e$. The inverse operation takes a matrix and returns the family of vectors obtained by taking linear combinations of the basis vectors $e_i$ with coefficients given by the matrix columns. More precisely: - The forward map $ \text{toFun} $ is `Basis.toMatrix e`, which constructs the coordinate matrix. - The inverse map $ \text{invFun} $ reconstructs the vectors from their coordinate matrix representation by $ v_j = \sum_i m_{ij} e_i $. - The equivalence preserves addition and scalar multiplication, and satisfies $ \text{invFun} \circ \text{toFun} = \text{id} $ and $ \text{toFun} \circ \text{invFun} = \text{id} $.

Basis.restrictScalars_toMatrix theorem

 [Fintype ι] [DecidableEq ι] {S : Type*} [CommRing S] [Nontrivial S] [Algebra R₂ S] [Module S M₂]
  [IsScalarTower R₂ S M₂] [NoZeroSMulDivisors R₂ S] (b : Basis ι S M₂) (v : ι → span R₂ (Set.range b)) :
  (algebraMap R₂ S).mapMatrix ((b.restrictScalars R₂).toMatrix v) = b.toMatrix (fun i ↦ (v i : M₂))

Full source

theorem restrictScalars_toMatrix [Fintype ι] [DecidableEq ι] {S : Type*} [CommRing S] [Nontrivial S]
    [Algebra R₂ S] [Module S M₂] [IsScalarTower R₂ S M₂] [NoZeroSMulDivisors R₂ S]
    (b : Basis ι S M₂) (v : ι → span R₂ (Set.range b)) :
    (algebraMap R₂ S).mapMatrix ((b.restrictScalars R₂).toMatrix v) =
      b.toMatrix (fun i ↦ (v i : M₂)) := by
  ext
  rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
    Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]

Compatibility of Coordinate Matrices under Scalar Restriction: $\text{algebraMap} \circ \text{toMatrix}_{\text{restrict}} = \text{toMatrix}_{\text{orig}}$

Informal description

Let $R_2$ and $S$ be commutative rings with $S$ nontrivial, and let $M_2$ be an $S$-module. Suppose there is an algebra structure $R_2 \to S$ making $M_2$ an $R_2$-module via scalar restriction, and that $R_2$ has no zero divisors acting on $S$. Given a basis $b$ of $M_2$ over $S$ indexed by a finite type $\iota$, and a family of vectors $v \colon \iota \to \text{span}_{R_2}(\text{range } b)$, the matrix obtained by applying the algebra map $R_2 \to S$ to each entry of the coordinate matrix of $v$ with respect to the restricted basis $b.\text{restrictScalars}\,R_2$ equals the coordinate matrix of $v$ (viewed in $M_2$) with respect to the original basis $b$. In mathematical notation: $$\text{algebraMap}_{R_2 \to S} \left( (b.\text{restrictScalars}\,R_2).\text{toMatrix}\,v \right) = b.\text{toMatrix}\,(\lambda i, (v i : M_2)).$$

LinearMap.toMatrix_id_eq_basis_toMatrix theorem

[Fintype ι] [DecidableEq ι] [Finite ι'] : LinearMap.toMatrix b b' id = b'.toMatrix b

Full source

/-- A generalization of `LinearMap.toMatrix_id`. -/
@[simp]
theorem LinearMap.toMatrix_id_eq_basis_toMatrix [Fintype ι] [DecidableEq ι] [Finite ι'] :
    LinearMap.toMatrix b b' id = b'.toMatrix b := by
  ext i
  apply LinearMap.toMatrix_apply

Matrix of Identity Map Equals Basis Transformation Matrix

Informal description

Let $b$ and $b'$ be bases for a module $M$ over a ring $R$, indexed by finite types $\iota$ and $\iota'$ respectively. Then the matrix representation of the identity linear map with respect to the bases $b$ and $b'$ is equal to the matrix whose columns are the coordinates of the basis vectors $b$ with respect to the basis $b'$. In other words, the matrix $\text{LinearMap.toMatrix } b \ b' \ \text{id}$ equals $\text{Basis.toMatrix } b' \ b$.

basis_toMatrix_mul_linearMap_toMatrix theorem

[Finite κ] [Fintype κ'] [DecidableEq ι'] : c.toMatrix c' * LinearMap.toMatrix b' c' f = LinearMap.toMatrix b' c f

Full source

@[simp]
theorem basis_toMatrix_mul_linearMap_toMatrix [Finite κ] [Fintype κ'] [DecidableEq ι'] :
    c.toMatrix c' * LinearMap.toMatrix b' c' f = LinearMap.toMatrix b' c f :=
  (Matrix.toLin b' c).injective <| by
    haveI := Classical.decEq κ'
    rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]

Matrix Multiplication of Basis Transformation and Linear Map Representation

Informal description

Let $M$ and $N$ be modules over a ring $R$ with bases $b'$ (indexed by $\iota'$), $c$ (indexed by $\kappa$), and $c'$ (indexed by $\kappa'$), where $\kappa$ is finite and $\kappa'$ is a finite type with decidable equality. For any linear map $f \colon M \to N$, the product of the coordinate matrix transforming $c'$ to $c$ and the matrix representation of $f$ with respect to bases $b'$ and $c'$ equals the matrix representation of $f$ with respect to bases $b'$ and $c$. In mathematical notation: $$c.\text{toMatrix}\,c' \cdot \text{LinearMap.toMatrix}\,b'\,c'\,f = \text{LinearMap.toMatrix}\,b'\,c\,f.$$

basis_toMatrix_mul theorem

 [Fintype κ] [Finite ι] [DecidableEq κ] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix ι' κ R) :
  b₁.toMatrix b₂ * A = LinearMap.toMatrix b₃ b₁ (toLin b₃ b₂ A)

Full source

theorem basis_toMatrix_mul [Fintype κ] [Finite ι] [DecidableEq κ]
    (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix ι' κ R) :
    b₁.toMatrix b₂ * A = LinearMap.toMatrix b₃ b₁ (toLin b₃ b₂ A) := by
  have := basis_toMatrix_mul_linearMap_toMatrix b₃ b₁ b₂ (Matrix.toLin b₃ b₂ A)
  rwa [LinearMap.toMatrix_toLin] at this

Matrix Product of Basis Transformation and Linear Map Representation

Informal description

Let $M$ and $N$ be modules over a ring $R$ with bases $b₁$ (indexed by $\iota$), $b₂$ (indexed by $\iota'$), and $b₃$ (indexed by $\kappa$), where $\iota$ is finite and $\kappa$ is a finite type with decidable equality. For any matrix $A$ of size $\iota' \times \kappa$ over $R$, the product of the coordinate matrix transforming $b₂$ to $b₁$ and $A$ equals the matrix representation of the linear map corresponding to $A$ (via $\text{toLin}$) with respect to bases $b₃$ and $b₁$. In mathematical notation: $$b₁.\text{toMatrix}\,b₂ \cdot A = \text{LinearMap.toMatrix}\,b₃\,b₁\,(\text{toLin}\,b₃\,b₂\,A).$$

linearMap_toMatrix_mul_basis_toMatrix theorem

 [Finite κ'] [DecidableEq ι] [DecidableEq ι'] : LinearMap.toMatrix b' c' f * b'.toMatrix b = LinearMap.toMatrix b c' f

Full source

@[simp]
theorem linearMap_toMatrix_mul_basis_toMatrix [Finite κ'] [DecidableEq ι] [DecidableEq ι'] :
    LinearMap.toMatrix b' c' f * b'.toMatrix b = LinearMap.toMatrix b c' f :=
  (Matrix.toLin b c').injective <| by
    rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]

Matrix Representation of Linear Map Composed with Basis Change

Informal description

Let $M$ and $N$ be modules over a ring $R$ with bases $b$ and $b'$ indexed by finite types $\iota$ and $\iota'$ respectively (with decidable equality), and let $c'$ be another basis of $N$ indexed by a finite type $\kappa'$. For any linear map $f : M \to N$, the product of the matrix representation of $f$ with respect to bases $b'$ and $c'$ and the coordinate matrix of $b'$ with respect to $b$ equals the matrix representation of $f$ with respect to bases $b$ and $c'$. In symbols: $$\text{toMatrix}_{b',c'}(f) \cdot \text{toMatrix}_{b,b'} = \text{toMatrix}_{b,c'}(f)$$ where $\text{toMatrix}_{x,y}$ denotes the matrix representation with respect to bases $x$ and $y$.

basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix theorem

 [Fintype κ'] [DecidableEq ι] [DecidableEq ι'] :
  c.toMatrix c' * LinearMap.toMatrix b' c' f * b'.toMatrix b = LinearMap.toMatrix b c f

Full source

theorem basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix
    [Fintype κ'] [DecidableEq ι] [DecidableEq ι'] :
    c.toMatrix c' * LinearMap.toMatrix b' c' f * b'.toMatrix b = LinearMap.toMatrix b c f := by
  cases nonempty_fintype κ
  rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]

Matrix Representation of Linear Map under Basis Change: $C_{c'}^c \cdot [f]_{b'}^{c'} \cdot B_b^{b'} = [f]_b^c$

Informal description

Let $M$ and $N$ be modules over a ring $R$ with bases $b$ (indexed by $\iota$), $b'$ (indexed by $\iota'$), $c$ (indexed by $\kappa$), and $c'$ (indexed by $\kappa'$), where $\iota$, $\iota'$, and $\kappa'$ are finite types with decidable equality. For any linear map $f \colon M \to N$, the following matrix equality holds: $$c.\text{toMatrix}\,c' \cdot \text{LinearMap.toMatrix}_{b',c'}(f) \cdot b'.\text{toMatrix}\,b = \text{LinearMap.toMatrix}_{b,c}(f)$$ Here, $\text{toMatrix}_{x,y}$ denotes the coordinate matrix transforming basis $x$ to basis $y$, and $\text{LinearMap.toMatrix}_{x,y}(f)$ is the matrix representation of $f$ with respect to bases $x$ and $y$.

mul_basis_toMatrix theorem

 [DecidableEq ι] [DecidableEq ι'] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix κ ι R) :
  A * b₁.toMatrix b₂ = LinearMap.toMatrix b₂ b₃ (toLin b₁ b₃ A)

Full source

theorem mul_basis_toMatrix [DecidableEq ι] [DecidableEq ι'] (b₁ : Basis ι R M) (b₂ : Basis ι' R M)
    (b₃ : Basis κ R N) (A : Matrix κ ι R) :
    A * b₁.toMatrix b₂ = LinearMap.toMatrix b₂ b₃ (toLin b₁ b₃ A) := by
  cases nonempty_fintype κ
  have := linearMap_toMatrix_mul_basis_toMatrix b₂ b₁ b₃ (Matrix.toLin b₁ b₃ A)
  rwa [LinearMap.toMatrix_toLin] at this

Matrix Multiplication with Basis Change: $A \cdot \text{toMatrix}_{b₁ b₂} = \text{toMatrix}_{b₂ b₃}(\text{toLin}_{b₁ b₃}(A))$

Informal description

Let $M$ and $N$ be modules over a ring $R$ with bases $b₁ : \iota \to M$ and $b₂ : \iota' \to M$ respectively, and let $b₃ : \kappa \to N$ be another basis. For any matrix $A$ with entries in $R$ and dimensions $\kappa \times \iota$, the product of $A$ with the coordinate matrix of $b₂$ with respect to $b₁$ equals the matrix representation of the linear map $\text{toLin}_{b₁ b₃}(A)$ with respect to bases $b₂$ and $b₃$. In symbols: $$A \cdot \text{toMatrix}_{b₁ b₂} = \text{toMatrix}_{b₂ b₃}(\text{toLin}_{b₁ b₃}(A))$$ where $\text{toMatrix}_{x,y}$ denotes the coordinate matrix with respect to bases $x$ and $y$, and $\text{toLin}_{x,y}$ converts a matrix to a linear map with respect to bases $x$ and $y$.

basis_toMatrix_basisFun_mul theorem

(b : Basis ι R (ι → R)) (A : Matrix ι ι R) : b.toMatrix (Pi.basisFun R ι) * A = of fun i j => b.repr (Aᵀ j) i

Full source

theorem basis_toMatrix_basisFun_mul (b : Basis ι R (ι → R)) (A : Matrix ι ι R) :
    b.toMatrix (Pi.basisFun R ι) * A = of fun i j => b.repr (Aᵀ j) i := by
  classical
  simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
  ext i j
  rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]

Matrix Product of Basis Transformation and Matrix Equals Coordinate Matrix of Transposed Columns

Informal description

Let $R$ be a ring and $\iota$ a finite type. For any basis $b$ of the $R$-module $\iota \to R$ and any matrix $A$ over $R$ of size $\iota \times \iota$, the product of the coordinate matrix transforming the standard basis (Pi.basisFun) to $b$ with $A$ equals the matrix whose $(i,j)$-th entry is the $i$-th coordinate of the $j$-th column of $A^T$ with respect to basis $b$. In symbols: $$b.\text{toMatrix}\,(\text{Pi.basisFun}\,R\,\iota) \cdot A = \text{matrix}\,(i\,j \mapsto b.\text{repr}\,(A^T\,j)_i)$$

Basis.toMatrix_reindex' theorem

 [DecidableEq ι] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
  (b.reindex e).toMatrix v = Matrix.reindexAlgEquiv R R e (b.toMatrix (v ∘ e))

Full source

/-- See also `Basis.toMatrix_reindex` which gives the `simp` normal form of this result. -/
theorem Basis.toMatrix_reindex' [DecidableEq ι] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M)
    (e : ι ≃ ι') : (b.reindex e).toMatrix v =
    Matrix.reindexAlgEquiv R R e (b.toMatrix (v ∘ e)) := by
  ext
  simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.reindexAlgEquiv_apply,
    Matrix.reindex_apply, Matrix.submatrix_apply, Function.comp_apply, e.apply_symm_apply,
    Finsupp.mapDomain_equiv_apply]

Matrix Representation under Basis Reindexing: $(b.\text{reindex}\, e).\text{toMatrix}\, v = \text{reindexAlgEquiv}\, e\, (b.\text{toMatrix}\, (v \circ e))$

Informal description

Let $M$ be a module over a ring $R$ with a basis $b$ indexed by $\iota$, and let $v : \iota' \to M$ be a family of vectors in $M$. Given an equivalence $e : \iota \simeq \iota'$ between index types, the matrix of coordinates of $v$ with respect to the reindexed basis $b.\text{reindex}\, e$ is equal to the matrix obtained by applying the reindexing algebra equivalence (induced by $e$) to the matrix of coordinates of $v \circ e$ with respect to the original basis $b$. In other words, for the reindexed basis $b' = b.\text{reindex}\, e$, we have: $$ b'.\text{toMatrix}\, v = \text{reindexAlgEquiv}\, e\, (b.\text{toMatrix}\, (v \circ e)). $$

Basis.toMatrix_mulVec_repr theorem

[Finite ι'] (m : M) : b'.toMatrix b *ᵥ b.repr m = b'.repr m

Full source

@[simp]
lemma Basis.toMatrix_mulVec_repr [Finite ι'] (m : M) :
    b'.toMatrix b *ᵥ b.repr m = b'.repr m := by
  classical
  cases nonempty_fintype ι'
  simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]

Change-of-Basis Matrix Action on Coordinate Vectors

Informal description

Let $M$ be a module over a ring $R$ with two bases $b$ and $b'$ indexed by finite types $\iota$ and $\iota'$ respectively. For any element $m \in M$, the matrix-vector product of the change-of-basis matrix from $b$ to $b'$ with the coordinate vector of $m$ in the basis $b$ equals the coordinate vector of $m$ in the basis $b'$. In other words, if $A$ is the matrix representing the change from basis $b$ to basis $b'$, then $A \cdot \mathbf{v}_b = \mathbf{v}_{b'}$, where $\mathbf{v}_b$ and $\mathbf{v}_{b'}$ are the coordinate vectors of $m$ in bases $b$ and $b'$ respectively.

Basis.toMatrix_mul_toMatrix theorem

{ι'' : Type*} [Fintype ι'] (b'' : ι'' → M) : b.toMatrix b' * b'.toMatrix b'' = b.toMatrix b''

Full source

/-- A generalization of `Basis.toMatrix_self`, in the opposite direction. -/
@[simp]
theorem Basis.toMatrix_mul_toMatrix {ι'' : Type*} [Fintype ι'] (b'' : ι'' → M) :
    b.toMatrix b' * b'.toMatrix b'' = b.toMatrix b'' := by
  haveI := Classical.decEq ι
  haveI := Classical.decEq ι'
  haveI := Classical.decEq ι''
  ext i j
  simp only [Matrix.mul_apply, Basis.toMatrix_apply, Basis.sum_repr_mul_repr]

Composition of Change-of-Basis Matrices: $A_{b→b'} \cdot A_{b'→b''} = A_{b→b''}$

Informal description

Let $M$ be a module over a ring $R$ with three bases $b$, $b'$, and $b''$ indexed by types $\iota$, $\iota'$, and $\iota''$ respectively, where $\iota'$ is finite. Then the matrix product of the change-of-basis matrix from $b$ to $b'$ and the change-of-basis matrix from $b'$ to $b''$ equals the change-of-basis matrix from $b$ to $b''$. That is: \[ \text{Basis.toMatrix}\, b\, b' \cdot \text{Basis.toMatrix}\, b'\, b'' = \text{Basis.toMatrix}\, b\, b'' \]

Basis.toMatrix_mul_toMatrix_flip theorem

[DecidableEq ι] [Fintype ι'] : b.toMatrix b' * b'.toMatrix b = 1

Full source

/-- `b.toMatrix b'` and `b'.toMatrix b` are inverses. -/
theorem Basis.toMatrix_mul_toMatrix_flip [DecidableEq ι] [Fintype ι'] :
    b.toMatrix b' * b'.toMatrix b = 1 := by rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

Inverse Relationship of Change-of-Basis Matrices: $A_{b→b'} \cdot A_{b'→b} = 1$

Informal description

Let $M$ be a module over a ring $R$ with two bases $b$ and $b'$ indexed by types $\iota$ and $\iota'$ respectively, where $\iota$ has decidable equality and $\iota'$ is finite. Then the matrix product of the change-of-basis matrix from $b$ to $b'$ and the change-of-basis matrix from $b'$ to $b$ is the identity matrix, i.e., $$A_{b→b'} \cdot A_{b'→b} = 1.$$

Basis.invertibleToMatrix definition

[DecidableEq ι] [Fintype ι] (b b' : Basis ι R₂ M₂) : Invertible (b.toMatrix b')

Full source

/-- A matrix whose columns form a basis `b'`, expressed w.r.t. a basis `b`, is invertible. -/
def Basis.invertibleToMatrix [DecidableEq ι] [Fintype ι] (b b' : Basis ι R₂ M₂) :
    Invertible (b.toMatrix b') :=
  ⟨b'.toMatrix b, Basis.toMatrix_mul_toMatrix_flip _ _, Basis.toMatrix_mul_toMatrix_flip _ _⟩

Invertibility of Change of Basis Matrix

Informal description

Given two bases $ b $ and $ b' $ of a finite-dimensional module $ M $ over a ring $ R $, the matrix $ b.toMatrix \, b' $ representing the change of basis from $ b $ to $ b' $ is invertible. The inverse matrix is given by $ b'.toMatrix \, b $, and both the left and right multiplication of these matrices yield the identity matrix.

Basis.toMatrix_reindex theorem

 (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') : (b.reindex e).toMatrix v = (b.toMatrix v).submatrix e.symm _root_.id

Full source

@[simp]
theorem Basis.toMatrix_reindex (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
    (b.reindex e).toMatrix v = (b.toMatrix v).submatrix e.symm _root_.id := by
  ext
  simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.submatrix_apply, _root_.id,
    Finsupp.mapDomain_equiv_apply]

Change of Basis Matrix under Reindexing: $(b.\text{reindex}\, e).\text{toMatrix}\, v = (b.\text{toMatrix}\, v).\text{submatrix}\, e^{-1}\, \text{id}$

Informal description

Let $b$ be a basis for an $R$-module $M$ indexed by $\iota$, and let $v : \iota' \to M$ be a family of vectors in $M$. Given an equivalence $e : \iota \simeq \iota'$ between index types, the matrix of coordinates of $v$ with respect to the reindexed basis $b.\text{reindex}\, e$ is equal to the submatrix of the original coordinate matrix $b.\text{toMatrix}\, v$ obtained by applying the inverse equivalence $e^{-1}$ to the row indices and keeping the column indices unchanged. In other words, $$(b.\text{reindex}\, e).\text{toMatrix}\, v = (b.\text{toMatrix}\, v).\text{submatrix}\, e^{-1}\, \text{id}.$$

Basis.toMatrix_map theorem

(b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N) : (b.map f).toMatrix v = b.toMatrix (f.symm ∘ v)

Full source

@[simp]
theorem Basis.toMatrix_map (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N) :
    (b.map f).toMatrix v = b.toMatrix (f.symm ∘ v) := by
  ext
  simp only [Basis.toMatrix_apply, Basis.map, LinearEquiv.trans_apply, (· ∘ ·)]

Transformation of Basis Coordinates under Linear Equivalence

Informal description

Let $b$ be a basis for an $R$-module $M$ indexed by $\iota$, and let $f : M \simeq N$ be a linear equivalence to another $R$-module $N$. For any family of vectors $v : \iota \to N$, the matrix of coordinates of $v$ with respect to the transformed basis $b.map\ f$ is equal to the matrix of coordinates of $f^{-1} \circ v$ with respect to the original basis $b$. In other words, $$(b.map\ f).toMatrix\ v = b.toMatrix\ (f^{-1} \circ v).$$

Mathlib.LinearAlgebra.Matrix.Basis

Main definitions

Main results

Tags