Documentation

TauCeti.LinearAlgebra.Matrix.ToLin

The endomorphism algebra of a finite-dimensional vector space, as matrices of a known size #

Mathlib's algEquivMatrix turns Module.End K M into matrices indexed by the index type of a chosen basis of M. This file records the form of it that is wanted when the dimension of M is known but no particular basis is: for Module.finrank K M = n, an isomorphism

Module.End K M ≃ₐ[K] Matrix (Fin n) (Fin n) K.

In the other direction it records how a matrix unit acts on the basis it is read in, which is the computation every matrix model of a Lie algebra performs on its root vectors.

Main results #

The first is used to turn the Azumaya isomorphism of a finite-dimensional central simple algebra into a matrix algebra in TauCeti/Algebra/CentralSimple/Opposite.lean.

source
def TauCeti.matrixGeneralLinearEquiv {R : Type u_1} [CommSemiring R] {n : Type u_2} [Fintype n] [DecidableEq n] :
GL n R ≃* LinearMap.GeneralLinearGroup R (n → R)

The matrix general linear group is the group of linear automorphisms of coordinate vectors over a commutative semiring. Mathlib's Matrix.GeneralLinearGroup.toLin requires a commutative ring.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.matrixGeneralLinearEquiv_apply {R : Type u_1} [CommSemiring R] {n : Type u_2} [Fintype n] [DecidableEq n] (A : GL n R) (v : n → R) :
    ((LinearMap.GeneralLinearGroup.generalLinearEquiv R (n → R)) (matrixGeneralLinearEquiv A)) v = (↑A).mulVec v

    A general linear matrix acts on coordinate vectors by matrix-vector multiplication.

    source
    theorem TauCeti.toLinAlgEquiv_single_apply_basis {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (bas : Module.Basis n R M) (p q : n) (v : R) (c : n) :
    ((Matrix.toLinAlgEquiv bas) (Matrix.single p q v)) (bas c) = (if q = c then v else 0) • bas p

    A matrix unit acts on a basis by a single coordinate. The endomorphism attached to Matrix.single p q v sends the basis vector indexed by the column q to v • bas p, and every other basis vector to 0.

    source
    theorem TauCeti.toMatrixAlgEquiv_eq_single_of_apply_basis {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {n : Type u_3} [Fintype n] [DecidableEq n] (bas : Module.Basis n R M) (f : Module.End R M) (p q : n) (v : R) (h : ∀ (c : n), f (bas c) = (if q = c then v else 0) • bas p) :
    (LinearMap.toMatrixAlgEquiv bas) f = Matrix.single p q v

    An endomorphism with a matrix-unit action has a single-entry matrix. If an endomorphism sends the basis vector indexed by q to v • bas p and every other basis vector to zero, its matrix in bas is Matrix.single p q v.

    source
    noncomputable def TauCeti.Algebra.endAlgEquivMatrix (K : Type u_1) [Field K] (M : Type u_2) [AddCommGroup M] [Module K M] [FiniteDimensional K M] {n : ℕ} (hn : Module.finrank K M = n) :
    Module.End K M ≃ₐ[K] Matrix (Fin n) (Fin n) K

    A K-vector space M of dimension n has Module.End K M ≃ₐ[K] Matrix (Fin n) (Fin n) K, read off a chosen K-basis of M.

    This is Mathlib's algEquivMatrix at the basis Module.finBasisOfFinrankEq, named here because it is wanted wherever a finite-dimensional endomorphism algebra has to be turned into matrices of a known size -- in particular as the second half of the opposite isomorphism TauCeti.Algebra.tensorOpAlgEquivMatrix, which the roadmap asks for separately.

    The basis is a choice, and nothing downstream should depend on which one it is; there is deliberately no lemma computing the matrix entries.

    Equations
    Instances For