Basis.toMatrix_reindex'
theorem Basis.toMatrix_reindex' :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : Fintype ι'] [inst_4 : Fintype ι] [inst_5 : DecidableEq ι]
[inst_6 : DecidableEq ι'] (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι'),
(b.reindex e).toMatrix v = (Matrix.reindexAlgEquiv R e) (b.toMatrix (v ∘ ⇑e))
The theorem `Basis.toMatrix_reindex'` states that for any types `ι`, `ι'`, `R` and `M`, with `R` a commutative semiring, `M` an additive commutative monoid and also a module over `R`, `ι` and `ι'` being finite types with decidable equality, given a basis `b` of `M` over `R` indexed by `ι`, a function `v` from `ι'` to `M`, and an equivalence `e` between `ι` and `ι'`, the matrix of the reindexed basis `b` with respect to `v` is equal to the matrix obtained by reindexing with `e` the matrix of `b` with respect to `v ∘ e`. This essentially captures how reindexing affects the matrix representation of the basis.
More concisely: Given a commutative semiring `R`, an additive commutative monoid and `R`-module `M` with finite index types `ι` and `ι'`, decidable equality, a basis `b` of `M` indexed by `ι`, a function `v` from `ι'` to `M`, and an equivalence `e` between `ι` and `ι'`, the matrices of the reindexed bases `b` with respect to `v` are equal up to reindexing with `e`.
|
LinearMap.toMatrix_id_eq_basis_toMatrix
theorem LinearMap.toMatrix_id_eq_basis_toMatrix :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (b : Basis ι R M) (b' : Basis ι' R M) [inst_3 : Fintype ι] [inst_4 : DecidableEq ι]
[inst_5 : Finite ι'], (LinearMap.toMatrix b b') LinearMap.id = b'.toMatrix ⇑b
The theorem `LinearMap.toMatrix_id_eq_basis_toMatrix` generalizes the identity of the transformation of a linear map to a matrix. Specifically, it states that for any types `ι`, `ι'`, `R`, and `M`, under the conditions that `R` is a commutative semiring, `M` is an additive commutative monoid, and `M` is a module over `R`, given a basis `b` for `M` over `R` indexed by `ι`, another basis `b'` for `M` over `R` indexed by `ι'`, as long as `ι` is finite and has decidable equality, and `ι'` is finite, the transformation of the identity linear map from `M` to `M` to a matrix with respect to the bases `b` and `b'` is equal to the matrix representation of `b'` with respect to the basis `b`.
More concisely: For finite index sets `ι` and `ι'`, given commutative semiring `R`, additive commutative monoid `M` with `R`-module structure, and bases `b: M ⨉ ι` and `b': M ⨉ ι'` of `M` over `R`, the matrix representation of `id_M` with respect to `b` and `b'` equals the matrix of `b'` with respect to `b`.
|
Basis.toMatrix_apply
theorem Basis.toMatrix_apply :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (e : Basis ι R M) (v : ι' → M) (i : ι) (j : ι'), e.toMatrix v i j = (e.repr (v j)) i
The theorem `Basis.toMatrix_apply` states that for all types `ι`, `ι'`, `R`, and `M`, where `R` is a commutative semiring, `M` is an additive commutative monoid, and `M` is a module over `R`, and for any basis `e` over `R` on `M`, any function `v` mapping `ι'` to `M`, and any elements `i` of `ι` and `j` of `ι'`, the value at the `(i, j)` position in the matrix obtained by expressing the vectors `v j` in the basis `e` is exactly the `i`-th coordinate of the vector `v j` in the basis `e`.
More concisely: For any commutative semiring R, additive commutative monoid and R-module M, basis e over R on M, function v mapping ι' to M, and i in ι and j in ι', the entry at position (i, j) in the matrix of vectors v j expressed in basis e equals the i-th coordinate of vector v j in basis e.
|
Basis.toMatrix_unitsSMul
theorem Basis.toMatrix_unitsSMul :
∀ {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂]
[inst_2 : Module R₂ M₂] [inst_3 : DecidableEq ι] (e : Basis ι R₂ M₂) (w : ι → R₂ˣ),
e.toMatrix ⇑(e.unitsSMul w) = Matrix.diagonal (Units.val ∘ w)
This theorem states that for any commutative ring `R₂`, additive commutative group `M₂`, and a `Module` of `M₂` over `R₂`, given a basis `e` of this `Module` and a function `w` that maps from index set `ι` to invertible elements of `R₂`, the matrix representation of the basis vectors, after they are scaled by `w` using `unitsSMul`, is a diagonal matrix. The diagonal entries of this matrix are the underlying values of the invertible elements given by function `w`.
More concisely: For any commutative ring `R₂`, additive commutative group `M₂`, and a `Module` `M` of `M₂` with basis `e` and a function `w : ι -> units R₂`, the matrix representation of `e` scaled by `w` is a diagonal matrix with `w i` as its diagonal entries.
|
Basis.toMatrix_isUnitSMul
theorem Basis.toMatrix_isUnitSMul :
∀ {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂]
[inst_2 : Module R₂ M₂] [inst_3 : DecidableEq ι] (e : Basis ι R₂ M₂) {w : ι → R₂} (hw : ∀ (i : ι), IsUnit (w i)),
e.toMatrix ⇑(e.isUnitSMul hw) = Matrix.diagonal w
This theorem states that for any basis `e` of a module `M₂` over a commutative ring `R₂`, indexed by type `ι`, and any function `w` from `ι` to `R₂` such that every `w i` is a unit (i.e., has a multiplicative inverse), the matrix representation of the basis transformed by `e.isUnitSMul hw` (which constructs a new basis where each basis vector is multiplied by the unit corresponding to its index) is a diagonal matrix with diagonal entries given by the function `w`. In other words, this basis transformation results in a diagonal matrix when represented in terms of the original basis.
More concisely: For any commutative ring R₂, module M₂ with basis e indexed by ι, and function w : ι → R₂ such that every w i is a unit, the basis transformation of e by e.isUnitSMul hw results in a diagonal matrix with diagonal entries equal to w.
|
Basis.toMatrix_mul_toMatrix
theorem Basis.toMatrix_mul_toMatrix :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (b : Basis ι R M) (b' : Basis ι' R M) {ι'' : Type u_10} [inst_3 : Fintype ι']
(b'' : ι'' → M), b.toMatrix ⇑b' * b'.toMatrix b'' = b.toMatrix b''
This theorem, `Basis.toMatrix_mul_toMatrix`, is a generalization of the `Basis.toMatrix_self` theorem, but in the opposite direction. It states that for any given types `ι`, `ι'` and `ι''`, a commutative semiring `R`, an additive commutative monoid `M` where `M` is a module over `R`, and bases `b` and `b'` of `M`, the product of the matrix representation of `b` with respect to `b'` and the matrix representation of `b'` with respect to another basis `b''` is equal to the matrix representation of `b` with respect to `b''`. This theorem holds true for any finitely typable `ι'`.
More concisely: For any commutative semiring R, additive commutative monoid M as an R-module, bases b and b' of M, and finitely typable ι', the product of the matrix representations of b with respect to b' and b' with respect to another basis b'' is equal to the matrix representation of b with respect to b''.
|
Basis.toMatrix_mul_toMatrix_flip
theorem Basis.toMatrix_mul_toMatrix_flip :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (b : Basis ι R M) (b' : Basis ι' R M) [inst_3 : DecidableEq ι] [inst_4 : Fintype ι'],
b.toMatrix ⇑b' * b'.toMatrix ⇑b = 1
The theorem `Basis.toMatrix_mul_toMatrix_flip` states that for any commutative semiring `R`, additive commutative monoid `M`, `R`-module `M`, basis `b` of type `ι`, basis `b'` of type `ι'`, given a decision procedure for equality on `ι` and that `ι'` is a finite type, the matrix representation `b.toMatrix b'` of basis `b'` in terms of basis `b` and the matrix representation `b'.toMatrix b` of basis `b` in terms of basis `b'` are inverses. In other words, multiplying these two matrix representations yields the identity matrix.
More concisely: For any commutative semiring `R`, additive commutative monoid `M`, `R`-module `M`, finite types `ι` and `ι'`, bases `b` and `b'` of `ι` and `ι'` respectively, if there exists a decision procedure for equality on `ι` and `ι'`, then `b'.toMatrix b` and `b.toMatrix b'` are inverses.
|