Documentation

TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.Lie

Linear terms of symplectic root subgroups #

Each standard symplectic root subgroup has the form 1 + c X, with X a single matrix unit for a long root and a signed pair of matrix units for a short root. RootSubgroupIndex.tangentMatrix records this linear term in paired coordinates. Its parameter can be recovered from a matrix entry over any commutative ring, including in characteristic two. These formulas identify the normalized Lie vectors of the represented root subgroups.

The matrix conventions are those of GLSymplecticFin.RootSubgroupIndex.hom.

References #

source
def TauCeti.GLSymplecticFin.RootSubgroupIndex.tangentMatrix {m : ℕ} {R : Type u_1} [CommRing R] (root : RootSubgroupIndex m) :
R →ₗ[R] Matrix (Fin m ⊕ Fin m) (Fin m ⊕ Fin m) R

The linear term of a standard symplectic root subgroup in paired coordinates. The difference roots have opposite signs in the two diagonal blocks; the sum roots have symmetric entries in an off-diagonal block.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.tangentMatrix_positiveLong {m : ℕ} {R : Type u_1} [CommRing R] (i : Fin m) (c : R) :
    (positiveLong i).tangentMatrix c = Matrix.single (Sum.inl i) (Sum.inr i) c

    The linear term of a positive long root.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.tangentMatrix_negativeLong {m : ℕ} {R : Type u_1} [CommRing R] (i : Fin m) (c : R) :
    (negativeLong i).tangentMatrix c = Matrix.single (Sum.inr i) (Sum.inl i) c

    The linear term of a negative long root.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.tangentMatrix_difference {m : ℕ} {R : Type u_1} [CommRing R] (i j : Fin m) (hij : i ≠ j) (c : R) :
    (difference i j hij).tangentMatrix c = Matrix.single (Sum.inl i) (Sum.inl j) c - Matrix.single (Sum.inr j) (Sum.inr i) c

    The linear term of a difference root.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.tangentMatrix_positiveSum {m : ℕ} {R : Type u_1} [CommRing R] (i j : Fin m) (hij : i < j) (c : R) :
    (positiveSum i j hij).tangentMatrix c = Matrix.single (Sum.inl i) (Sum.inr j) c + Matrix.single (Sum.inl j) (Sum.inr i) c

    The linear term of a positive sum root.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.tangentMatrix_negativeSum {m : ℕ} {R : Type u_1} [CommRing R] (i j : Fin m) (hij : i < j) (c : R) :
    (negativeSum i j hij).tangentMatrix c = Matrix.single (Sum.inr i) (Sum.inl j) c + Matrix.single (Sum.inr j) (Sum.inl i) c

    The linear term of a negative sum root.

    source
    @[simp]
    theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.map_tangentMatrix {m : ℕ} {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (root : RootSubgroupIndex m) (f : R →+ S) (c : R) :
    (root.tangentMatrix c).map ⇑f = root.tangentMatrix (f c)

    Entrywise application of an additive homomorphism preserves the linear term. This applies to derivatives of coordinate functions as well as to changes of coefficients.

    source
    theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.tangentMatrix_injective {m : ℕ} {R : Type u_1} [CommRing R] (root : RootSubgroupIndex m) :
    Function.Injective ⇑root.tangentMatrix

    The parameter of the linear term is recoverable from one of its entries.

    source
    theorem TauCeti.GLSymplecticFin.RootSubgroupIndex.hom_apply_matrix {m : ℕ} {R : Type u_1} [CommRing R] (root : RootSubgroupIndex m) (c : Multiplicative R) :
    (↑↑(root.hom c)).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv = 1 + root.tangentMatrix (Multiplicative.toAdd c)

    The root one-parameter subgroup is the identity plus its linear term. This includes all long and short roots, over every commutative ring.