Documentation

TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.LeftMulMatrix

The unit group of an algebra inside a general linear group #

Let S be an algebra over a commutative semiring R, free with basis b : Module.Basis ι R S. Multiplication by x : S is an R-linear endomorphism of S, and its matrix in the basis b is Mathlib's Algebra.leftMulMatrix b x. When x is a unit that matrix is invertible, so the regular representation restricts to a group homomorphism

TauCeti.unitsLeftMulMatrix b : Sˣ →* GL ι R.

It is injective, it sends a unit of the base ring to the corresponding scalar matrix, and it converts the two standard invariants of an element of S into the two standard invariants of a matrix: its determinant is the algebra norm and its trace is the algebra trace. Only these last two ask for a ring, the level Algebra.norm and Algebra.trace are stated at; the embedding itself lives over a semiring.

The motivating instance is a degree-2 field extension E/F, where this embeds Eˣ in GL (Fin 2) F as the non-split torus; see TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/NonSplitTorus.lean. Compare TauCeti.diagGL, which embeds the split torus.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.unitsLeftMulMatrix {R : Type u_1} {S : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [CommSemiring R] [Semiring S] [Algebra R S] (b : Module.Basis ι R S) :
Sˣ →* GL ι R

The units of S, embedded in GL ι R by left multiplication read in the basis b.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.coe_unitsLeftMulMatrix {R : Type u_1} {S : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [CommSemiring R] [Semiring S] [Algebra R S] (b : Module.Basis ι R S) (x : Sˣ) :
    ↑((unitsLeftMulMatrix b) x) = (Algebra.leftMulMatrix b) ↑x

    The matrix underlying unitsLeftMulMatrix b x is Algebra.leftMulMatrix b x.

    source
    theorem TauCeti.unitsLeftMulMatrix_apply {R : Type u_1} {S : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [CommSemiring R] [Semiring S] [Algebra R S] (b : Module.Basis ι R S) (x : Sˣ) (i j : ι) :
    ↑((unitsLeftMulMatrix b) x) i j = (b.repr (↑x * b j)) i

    The entries of unitsLeftMulMatrix b x are the coordinates of x * b j in the basis b.

    source
    theorem TauCeti.unitsLeftMulMatrix_injective {R : Type u_1} {S : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [CommSemiring R] [Semiring S] [Algebra R S] (b : Module.Basis ι R S) :
    Function.Injective ⇑(unitsLeftMulMatrix b)

    Left multiplication by a unit determines the unit.

    source
    theorem TauCeti.leftMulMatrix_algebraMap {R : Type u_1} {S : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [CommSemiring R] [Semiring S] [Algebra R S] (b : Module.Basis ι R S) (r : R) :
    (Algebra.leftMulMatrix b) ((algebraMap R S) r) = (Matrix.scalar ι) r

    Left multiplication by an element of the base ring is the corresponding scalar matrix.

    source
    @[simp]
    theorem TauCeti.unitsLeftMulMatrix_map_algebraMap {R : Type u_1} {S : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [CommSemiring R] [Semiring S] [Algebra R S] (b : Module.Basis ι R S) (r : Rˣ) :
    (unitsLeftMulMatrix b) ((Units.map ↑(algebraMap R S)) r) = (Matrix.GeneralLinearGroup.scalar ι) r

    A unit of the base ring is sent to the corresponding scalar matrix.

    source
    theorem TauCeti.val_det_unitsLeftMulMatrix {R : Type u_1} {S : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [Ring S] [Algebra R S] (b : Module.Basis ι R S) (x : Sˣ) :
    ↑(Matrix.GeneralLinearGroup.det ((unitsLeftMulMatrix b) x)) = (Algebra.norm R) ↑x

    The determinant of the matrix of left multiplication by x is the algebra norm of x.

    source
    theorem TauCeti.trace_unitsLeftMulMatrix {R : Type u_1} {S : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] [CommRing S] [Algebra R S] (b : Module.Basis ι R S) (x : Sˣ) :
    (↑((unitsLeftMulMatrix b) x)).trace = (Algebra.trace R S) ↑x

    The trace of the matrix of left multiplication by x is the algebra trace of x.