Pinned coordinates on the modular F4 quotient

This file fixes the coordinate identification between the long-root quotient and the short-root ideal. It also records the elementary reversal and exponent data for the special isogeny on the eight signed simple roots. The actual first- and second-order column comparison is built on this normalization.

References

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

def TauCeti.F4ShortRoot.isogenyReverse : Fin 4 ⊕ Fin 4 → Fin 4 ⊕ Fin 4

The length-exchanging involution of the positive and negative numbered simple roots.

Equations

• TauCeti.F4ShortRoot.isogenyReverse = Sum.map ⇑Fin.revPerm ⇑Fin.revPerm

def TauCeti.F4ShortRoot.isogenyExponent : Fin 4 ⊕ Fin 4 → ℕ

The parameter exponent of a numbered simple root under the special isogeny.

Equations

• TauCeti.F4ShortRoot.isogenyExponent = Sum.elim ![1, 1, 2, 2] ![1, 1, 2, 2]

theorem TauCeti.F4ShortRoot.isogenyExponent_eq_one_or_two (k : Fin 4 ⊕ Fin 4) : isogenyExponent k = 1 ∨ isogenyExponent k = 2

Each special-isogeny parameter exponent is one or two.

@[simp]

theorem TauCeti.F4ShortRoot.isogenyReverse_isogenyReverse (k : Fin 4 ⊕ Fin 4) : isogenyReverse (isogenyReverse k) = k

Reversal of the signed simple-root labels is involutive.

theorem TauCeti.F4ShortRoot.isogenyExponent_mul_isogenyExponent_eq_two (k : Fin 4 ⊕ Fin 4) : isogenyExponent k * isogenyExponent (isogenyReverse k) = 2

The exponents on two successively reversed labels multiply to two.

noncomputable def TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv : (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace) ≃ₗ[ZMod 2] ↥f4ShortRootLieIdeal

The coordinate identification from the long-root quotient to the short-root ideal. Both sides use the same Fin 26 labels, already normalized by the special root permutation.

Equations

• TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv = TauCeti.DynkinType.f4ShortRootQuotientBasis.equiv TauCeti.DynkinType.f4ShortRootLieIdealBasis (Equiv.refl (Fin 26))

@[simp]

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_basis (a : Fin 26) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientBasis a) = f4ShortRootLieIdealBasis a

noncomputable def TauCeti.DynkinType.f4ShortRootQuotientLift (a : Fin 26) : f4ModularChevalleyLieAlgebra

The canonical ambient lift of a quotient coordinate.

Equations

• TauCeti.DynkinType.f4ShortRootQuotientLift a = TauCeti.DynkinType.f4ModularChevalleyBasis (TauCeti.DynkinType.f4LongRootBasisCoordinate a)

@[simp]

theorem TauCeti.DynkinType.f4ShortRootQuotientLift_eq_basis (a : Fin 26) : f4ShortRootQuotientLift a = f4ModularChevalleyBasis (f4LongRootBasisCoordinate a)

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_quotientLift (a : Fin 26) : f4ShortRootSubspace.mkQ (f4ShortRootQuotientLift a) = f4ShortRootQuotientBasis a

@[simp]

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_basisLift (a : Fin 26) : Submodule.Quotient.mk (f4ModularChevalleyBasis (f4LongRootBasisCoordinate a)) = f4ShortRootQuotientBasis a

The quotient projection on a canonical ambient basis lift, in simplifier normal form.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_mkQ_quotientLift (a : Fin 26) : f4ShortRootQuotientToIdealEquiv (f4ShortRootSubspace.mkQ (f4ShortRootQuotientLift a)) = f4ShortRootLieIdealBasis a

noncomputable def TauCeti.DynkinType.f4ShortRootQuotientFirstColumn (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace

The first-order quotient column of a numbered signed simple root.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4ShortRootQuotientFirstColumn_eq (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ShortRootQuotientFirstColumn k a = f4ShortRootSubspace.mkQ ⁅f4ModularRootVector (f4SignedSimpleRootIndex k), f4ShortRootQuotientLift a⁆

noncomputable def TauCeti.DynkinType.f4ShortRootQuotientDividedSquareColumn (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace

The second divided-power quotient column of a numbered signed simple root.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4ShortRootQuotientDividedSquareColumn_eq (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ShortRootQuotientDividedSquareColumn k a = f4ShortRootSubspace.mkQ ((f4ModularDividedAdjointSquare k) (f4ShortRootQuotientLift a))

noncomputable def TauCeti.DynkinType.f4ShortRootIdealFirstColumn (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : ↥f4ShortRootLieIdeal

The first-order column on the short-root ideal, in its canonical coordinates.

Equations

• TauCeti.DynkinType.f4ShortRootIdealFirstColumn k a = (TauCeti.DynkinType.f4ShortRootSignedSimpleAdjoint k) (TauCeti.DynkinType.f4ShortRootLieIdealBasis a)

@[simp]

theorem TauCeti.DynkinType.f4ShortRootIdealFirstColumn_apply (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ShortRootIdealFirstColumn k a = (f4ShortRootSignedSimpleAdjoint k) (f4ShortRootLieIdealBasis a)

theorem TauCeti.DynkinType.coe_f4ShortRootIdealFirstColumn (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : ↑(f4ShortRootIdealFirstColumn k a) = ⁅f4ModularRootVector (f4SignedSimpleRootIndex k), ↑(f4ShortRootLieIdealBasis a)⁆

noncomputable def TauCeti.DynkinType.f4ShortRootIdealDividedSquareColumn (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : ↥f4ShortRootLieIdeal

The second divided-power column on the short-root ideal, in its canonical coordinates.

Equations

• TauCeti.DynkinType.f4ShortRootIdealDividedSquareColumn k a = (TauCeti.DynkinType.f4ShortRootDividedAdjointSquare k) (TauCeti.DynkinType.f4ShortRootLieIdealBasis a)

@[simp]

theorem TauCeti.DynkinType.f4ShortRootIdealDividedSquareColumn_apply (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ShortRootIdealDividedSquareColumn k a = (f4ShortRootDividedAdjointSquare k) (f4ShortRootLieIdealBasis a)

theorem TauCeti.DynkinType.f4ShortRootIdealFirstColumn_eq (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ShortRootIdealFirstColumn k a = ↑(f4SimpleRootCoeff k a) • f4ShortRootLieIdealBasis (f4SimpleRootTarget k a)

The ideal's first-order canonical column is the corresponding sparse root-matrix column.

theorem TauCeti.DynkinType.f4ShortRootIdealDividedSquareColumn_eq (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ShortRootIdealDividedSquareColumn k a = ↑(f4DividedSquareCoeff k a) • f4ShortRootLieIdealBasis (f4DividedSquareTarget k a)

The ideal's second divided-power canonical column is the corresponding sparse matrix column.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_firstColumn_eq_zero_of_short (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 1) (a : Fin 26) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientFirstColumn k a) = 0

A short signed-simple source has zero first-order action on every quotient coordinate.

theorem TauCeti.DynkinType.f4SpecialIsogenyIndexEquiv_f4SignedSimpleRootIndex (k : Fin 4 ⊕ Fin 4) : f4SpecialIsogenyIndexEquiv (f4SignedSimpleRootIndex k) = f4SignedSimpleRootIndex (F4ShortRoot.isogenyReverse k)

The special root permutation reverses the numbered signed simple roots.

theorem TauCeti.DynkinType.f4SpecialIsogenyIndexEquiv_opposite_f4SignedSimpleRootIndex (k : Fin 4 ⊕ Fin 4) : f4SpecialIsogenyIndexEquiv (f4OppositeRootIndex (f4SignedSimpleRootIndex k)) = f4OppositeRootIndex (f4SignedSimpleRootIndex (F4ShortRoot.isogenyReverse k))

The special root permutation also reverses the opposite signed-simple indices.