The adjoint action on the modular F₄ short-root ideal

This file restricts the adjoint action of the full Chevalley lattice reduced modulo two to its twenty-six-dimensional short-root ideal. It expresses that representation in the canonical basis of short-root vectors and the two short simple coroots.

This restricted action ρ : L → End(I) is the input to the represented quotient ρ(L) / ρ(I) used in the construction of the characteristic-two exceptional isogeny. Only the action on the ideal is defined here; identifying that represented quotient with the quotient of the modular Chevalley algebra by its short-root ideal needs a later theorem.

Main definitions

• TauCeti.DynkinType.f4ShortRootAdjoint: the restricted adjoint representation.
• TauCeti.DynkinType.f4ShortRootAdjointMatrix: its matrix in the canonical basis f4ShortRootLieIdealBasis.
• TauCeti.DynkinType.f4ShortRootSignedSimpleAdjoint: the operators at the positive and negative simple roots.

Main results

• TauCeti.DynkinType.f4ShortRootAdjointMatrix_apply computes matrix entries as ambient bracket coordinates.
• TauCeti.DynkinType.f4ShortRootAdjoint_rootVector_of_add_eq_short, TauCeti.DynkinType.coe_f4ShortRootAdjoint_opposite, and TauCeti.DynkinType.coe_f4ShortRootAdjoint_simpleCoroot compute the action on the three forms of basis interaction used downstream.

References

• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• R. W. Carter, Simple Groups of Lie Type, §12.3.

noncomputable def TauCeti.DynkinType.f4ShortRootAdjoint : f4ModularChevalleyLieAlgebra →ₗ⁅ZMod 2⁆ Module.End (ZMod 2) ↥f4ShortRootLieIdeal

The adjoint action of the reduced Chevalley Lie algebra on its modular short-root ideal.

Equations

• TauCeti.DynkinType.f4ShortRootAdjoint = LieModule.toEnd (ZMod 2) TauCeti.DynkinType.f4ModularChevalleyLieAlgebra ↥TauCeti.DynkinType.f4ShortRootLieIdeal

@[simp]

theorem TauCeti.DynkinType.coe_f4ShortRootAdjoint_apply (x : f4ModularChevalleyLieAlgebra) (y : ↥f4ShortRootLieIdeal) : ↑((f4ShortRootAdjoint x) y) = ⁅x, ↑y⁆

The restricted adjoint action is the ambient Lie bracket after coercion from the ideal.

noncomputable def TauCeti.DynkinType.f4ShortRootAdjointMatrix (X : f4ModularChevalleyLieAlgebra) : Matrix (Fin 26) (Fin 26) (ZMod 2)

Matrix of the modular short-root adjoint action in its integral-weight basis.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.f4ShortRootAdjointMatrixBaseChange {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (X : f4ModularChevalleyLieAlgebra) : Matrix (Fin 26) (Fin 26) A

Base change of a modular short-root adjoint matrix to a value algebra.

Equations

• TauCeti.DynkinType.f4ShortRootAdjointMatrixBaseChange X = (TauCeti.DynkinType.f4ShortRootAdjointMatrix X).map ⇑(algebraMap (ZMod 2) A)

@[simp]

theorem TauCeti.DynkinType.f4ShortRootAdjointMatrixBaseChange_apply {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (X : f4ModularChevalleyLieAlgebra) (i j : Fin 26) : f4ShortRootAdjointMatrixBaseChange X i j = (algebraMap (ZMod 2) A) (f4ShortRootAdjointMatrix X i j)

Entries of the base-changed adjoint matrix are obtained by applying the structure map.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootAdjointMatrix_apply (X : f4ModularChevalleyLieAlgebra) (i j : Fin 26) : f4ShortRootAdjointMatrix X i j = (f4ModularChevalleyBasis.repr ⁅X, ↑(f4ShortRootLieIdealBasis j)⁆) (f4ShortRootBasisCoordinate i)

An entry of the adjoint matrix is the corresponding ambient bracket coordinate.

theorem TauCeti.DynkinType.f4ShortRootAdjointMatrix_eq_toMatrix (X : f4ModularChevalleyLieAlgebra) : f4ShortRootAdjointMatrix X = (LinearMap.toMatrix f4ShortRootLieIdealBasis f4ShortRootLieIdealBasis) (f4ShortRootAdjoint X)

The named adjoint matrix is the matrix of the restricted adjoint endomorphism.

noncomputable def TauCeti.DynkinType.f4ShortRootSignedSimpleAdjoint (k : Fin 4 ⊕ Fin 4) : Module.End (ZMod 2) ↥f4ShortRootLieIdeal

The signed simple-root adjoint operator restricted to the modular short-root ideal.

Equations

• TauCeti.DynkinType.f4ShortRootSignedSimpleAdjoint k = TauCeti.DynkinType.f4ShortRootAdjoint (TauCeti.DynkinType.f4ModularSignedSimpleRootVector k)

theorem TauCeti.DynkinType.coe_f4ShortRootSignedSimpleAdjoint_apply (k : Fin 4 ⊕ Fin 4) (y : ↥f4ShortRootLieIdeal) : ↑((f4ShortRootSignedSimpleAdjoint k) y) = ⁅f4ModularRootVector (f4SignedSimpleRootIndex k), ↑y⁆

The signed simple-root adjoint operator is the bracket with its signed simple root vector.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootSignedSimpleAdjoint_apply (k : Fin 4 ⊕ Fin 4) (y : ↥f4ShortRootLieIdeal) : (f4ShortRootSignedSimpleAdjoint k) y = (f4ShortRootAdjoint (f4ModularRootVector (f4SignedSimpleRootIndex k))) y

The signed simple-root operator is the restricted adjoint action of its root vector.

noncomputable def TauCeti.DynkinType.f4ShortRootSignedSimpleAdjointMatrix (k : Fin 4 ⊕ Fin 4) : Matrix (Fin 26) (Fin 26) (ZMod 2)

The matrix of the signed simple-root adjoint operator in the canonical short-root basis.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootSignedSimpleAdjointMatrix_apply (k : Fin 4 ⊕ Fin 4) (a b : Fin 26) : f4ShortRootSignedSimpleAdjointMatrix k a b = (f4ShortRootLieIdealBasis.repr ((f4ShortRootSignedSimpleAdjoint k) (f4ShortRootLieIdealBasis b))) a

Entries of a signed simple-root adjoint matrix are the corresponding ideal-basis coordinates.

theorem TauCeti.DynkinType.f4ShortRootAdjoint_rootVector_of_add_eq_short (alpha beta gamma : Fin 48) (hbeta : f4Length beta = 1) (hgamma : f4Length gamma = 1) (h : f4SimplyConnectedRootDatum.root gamma = f4SimplyConnectedRootDatum.root beta + f4SimplyConnectedRootDatum.root alpha) : (f4ShortRootAdjoint (f4ModularRootVector alpha)) (f4ShortRootLieIdealBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inl ⟨beta, hbeta⟩))) = f4ShortRootLieIdealBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inl ⟨gamma, hgamma⟩))

On a short-root basis column whose translate is again short, the restricted adjoint action is the translated short-root basis vector with coefficient one.

theorem TauCeti.DynkinType.coe_f4ShortRootAdjoint_opposite (alpha : Fin 48) (hopp : f4Length (f4OppositeRootIndex alpha) = 1) : ↑((f4ShortRootAdjoint (f4ModularRootVector alpha)) (f4ShortRootLieIdealBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inl ⟨f4OppositeRootIndex alpha, hopp⟩)))) = f4ModularCoroot alpha

On the root coordinate opposite a short root, the restricted adjoint action lands in the corresponding modular coroot.

theorem TauCeti.DynkinType.coe_f4ShortRootAdjoint_simpleCoroot (alpha : Fin 48) (i : Fin F4.rank) (hi : Fin.cast rank_F4 i = 2 ∨ Fin.cast rank_F4 i = 3) : ↑((f4ShortRootAdjoint (f4ModularRootVector alpha)) ⟨f4ModularSimpleCoroot i, ⋯⟩) = -↑(RootPairing.pairing f4SimplyConnectedRootDatum alpha (Fin.castAdd 44 (Fin.cast rank_F4 i))) • f4ModularRootVector alpha

On either short simple-coroot coordinate, the restricted adjoint action is the root vector scaled by the reduced Cartan integer (with the bracket-order sign).