Documentation

Mathlib.LinearAlgebra.Matrix.Basis

Bases and matrices #

This file defines the map Basis.toMatrix that sends a family of vectors to the matrix of their coordinates with respect to some basis.

Main definitions #

Main results #

Tags #

matrix, basis

def Basis.toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) :
Matrix ι ι' R

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.

Equations
Instances For
    theorem Basis.toMatrix_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) (i : ι) (j : ι') :
    Basis.toMatrix e v i j = (e.repr (v j)) i
    theorem Basis.toMatrix_transpose_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) (j : ι') :
    Matrix.transpose (Basis.toMatrix e v) j = (e.repr (v j))
    theorem Basis.toMatrix_eq_toMatrix_constr {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) [Fintype ι] [DecidableEq ι] (v : ιM) :
    theorem Basis.coePiBasisFun.toMatrix_eq_transpose {ι : Type u_1} {R : Type u_5} [CommSemiring R] [Finite ι] :
    Basis.toMatrix (Pi.basisFun R ι) = Matrix.transpose
    @[simp]
    theorem Basis.toMatrix_self {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) [DecidableEq ι] :
    Basis.toMatrix e e = 1
    theorem Basis.toMatrix_update {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) (j : ι') [DecidableEq ι'] (x : M) :
    @[simp]
    theorem Basis.toMatrix_unitsSMul {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [DecidableEq ι] (e : Basis ι R₂ M₂) (w : ιR₂ˣ) :

    The basis constructed by unitsSMul has vectors given by a diagonal matrix.

    @[simp]
    theorem Basis.toMatrix_isUnitSMul {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [DecidableEq ι] (e : Basis ι R₂ M₂) {w : ιR₂} (hw : ∀ (i : ι), IsUnit (w i)) :

    The basis constructed by isUnitSMul has vectors given by a diagonal matrix.

    @[simp]
    theorem Basis.sum_toMatrix_smul_self {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) (j : ι') [Fintype ι] :
    (Finset.sum Finset.univ fun (i : ι) => Basis.toMatrix e v i j e i) = v j
    theorem Basis.toMatrix_smul {ι : Type u_1} {R₁ : Type u_9} {S : Type u_10} [CommRing R₁] [Ring S] [Algebra R₁ S] [Fintype ι] [DecidableEq ι] (x : S) (b : Basis ι R₁ S) (w : ιS) :
    theorem Basis.toMatrix_map_vecMul {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} [CommSemiring R] {S : Type u_9} [Ring S] [Algebra R S] [Fintype ι] (b : Basis ι R S) (v : ι'S) :
    @[simp]
    theorem Basis.toLin_toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) [Fintype ι] [Fintype ι'] [DecidableEq ι'] (v : Basis ι' R M) :
    (Matrix.toLin v e) (Basis.toMatrix e v) = LinearMap.id
    def Basis.toMatrixEquiv {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (e : Basis ι R M) :
    (ιM) ≃ₗ[R] Matrix ι ι R

    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Basis.restrictScalars_toMatrix {ι : Type u_1} (R₂ : Type u_7) {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [Fintype ι] [DecidableEq ι] {S : Type u_9} [CommRing S] [Nontrivial S] [Algebra R₂ S] [Module S M₂] [IsScalarTower R₂ S M₂] [NoZeroSMulDivisors R₂ S] (b : Basis ι S M₂) (v : ι(Submodule.span R₂ (Set.range b))) :
      (RingHom.mapMatrix (algebraMap R₂ S)) (Basis.toMatrix (Basis.restrictScalars R₂ b) v) = Basis.toMatrix b fun (i : ι) => (v i)
      @[simp]
      theorem basis_toMatrix_mul_linearMap_toMatrix {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b' : Basis ι' R M) (c : Basis κ R N) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Fintype κ] [Fintype κ'] [DecidableEq ι'] :
      @[simp]
      theorem linearMap_toMatrix_mul_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b : Basis ι R M) (b' : Basis ι' R M) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Fintype κ'] [Fintype ι] [DecidableEq ι] [DecidableEq ι'] :
      theorem basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b : Basis ι R M) (b' : Basis ι' R M) (c : Basis κ R N) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Fintype κ] [Fintype κ'] [Fintype ι] [DecidableEq ι] [DecidableEq ι'] :
      theorem basis_toMatrix_mul {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] [Fintype ι'] [Fintype κ] [Fintype ι] [DecidableEq κ] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix ι' κ R) :
      Basis.toMatrix b₁ b₂ * A = (LinearMap.toMatrix b₃ b₁) ((Matrix.toLin b₃ b₂) A)
      theorem mul_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] [Fintype ι'] [Fintype κ] [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix κ ι R) :
      A * Basis.toMatrix b₁ b₂ = (LinearMap.toMatrix b₂ b₃) ((Matrix.toLin b₁ b₃) A)
      theorem basis_toMatrix_basisFun_mul {ι : Type u_1} {R : Type u_5} [CommSemiring R] [Fintype ι] (b : Basis ι R (ιR)) (A : Matrix ι ι R) :
      Basis.toMatrix b (Pi.basisFun R ι) * A = Matrix.of fun (i j : ι) => (b.repr (Matrix.transpose A j)) i
      @[simp]
      theorem LinearMap.toMatrix_id_eq_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) [Fintype ι'] [Fintype ι] [DecidableEq ι] :
      (LinearMap.toMatrix b b') LinearMap.id = Basis.toMatrix b' b

      A generalization of LinearMap.toMatrix_id.

      theorem Basis.toMatrix_reindex' {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι'] [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (b : Basis ι R M) (v : ι'M) (e : ι ι') :

      See also Basis.toMatrix_reindex which gives the simp normal form of this result.

      @[simp]
      theorem Basis.toMatrix_mul_toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) {ι'' : Type u_10} [Fintype ι'] (b'' : ι''M) :

      A generalization of Basis.toMatrix_self, in the opposite direction.

      theorem Basis.toMatrix_mul_toMatrix_flip {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) [DecidableEq ι] [Fintype ι'] :
      Basis.toMatrix b b' * Basis.toMatrix b' b = 1

      b.toMatrix b' and b'.toMatrix b are inverses.

      def Basis.invertibleToMatrix {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [DecidableEq ι] [Fintype ι] (b : Basis ι R₂ M₂) (b' : Basis ι R₂ M₂) :

      A matrix whose columns form a basis b', expressed w.r.t. a basis b, is invertible.

      Equations
      Instances For
        @[simp]
        theorem Basis.toMatrix_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι'M) (e : ι ι') :
        @[simp]
        theorem Basis.toMatrix_map {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ιN) :