Integral root exponentials on the modular F₄ quotient

The reduced integral Chevalley root exponential acts on the modular F4 short-root quotient by a three-term quadratic formula over every commutative ZMod 2-algebra. The formula identifies the quotient root columns used in the special-isogeny pinning.

References

• R. W. Carter, Simple Groups of Lie Type, §4.4, for Chevalley root exponentials.

theorem TauCeti.DynkinType.isogenyExponent_eq_two_of_short (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 1) : F4ShortRoot.isogenyExponent k = 2

A short signed-simple source has parameter exponent two.

theorem TauCeti.DynkinType.isogenyExponent_eq_one_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) : F4ShortRoot.isogenyExponent k = 1

A long signed-simple source has parameter exponent one.

theorem TauCeti.DynkinType.f4ShortRootIdealDividedSquareColumn_eq_zero_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) (a : Fin 26) : f4ShortRootIdealDividedSquareColumn k a = 0

A long signed-simple root has zero divided-square action on the short-root ideal.

theorem TauCeti.DynkinType.f4Length_isogenyReverse_eq_two_of_short (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 1) : f4Length (f4SignedSimpleRootIndex (F4ShortRoot.isogenyReverse k)) = 2

Reversal exchanges a short signed-simple source with a long one.

noncomputable def TauCeti.DynkinType.f4ShortRootBaseChangeQuotient {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] : TensorProduct ℤ A ↥f4ChevalleyLieLattice →ₗ[A] TensorProduct (ZMod 2) A (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace)

Reduction modulo two followed by the quotient by the modular short-root ideal, after an arbitrary scalar extension.

Equations

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

theorem TauCeti.DynkinType.f4ShortRootBaseChangeQuotient_apply {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) : f4ShortRootBaseChangeQuotient x = (LinearMap.baseChange A f4ShortRootSubspace.mkQ) ((cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice).symm x)

Evaluation of the scalar-extended quotient map through scalar-tower cancellation.

theorem TauCeti.DynkinType.f4ShortRootBaseChangeQuotient_tmul {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (a : A) (x : ↥f4ChevalleyLieLattice) : f4ShortRootBaseChangeQuotient (a ⊗ₜ[ℤ] x) = a ⊗ₜ[ZMod 2] f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] x)

The scalar-extended quotient map on a pure integral tensor.

theorem TauCeti.DynkinType.f4ShortRootBaseChangeQuotient_rootExponential_tmul {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (x : ↥f4ChevalleyLieLattice) : f4ShortRootBaseChangeQuotient ((f4RootExponential k t) (1 ⊗ₜ[ℤ] x)) = 1 ⊗ₜ[ZMod 2] f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] x) + t • 1 ⊗ₜ[ZMod 2] f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] ⁅f4IntegralRootVector (f4SignedSimpleRootIndex k), x⁆) + t ^ 2 • 1 ⊗ₜ[ZMod 2] f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] (f4IntegralDividedAdjointSquare k) x)

After passing to the quotient, the root exponential has its three-term integral divided-power polynomial on every pure tensor.

noncomputable def TauCeti.DynkinType.f4IntegralShortRootQuotientLift (a : Fin 26) : ↥f4ChevalleyLieLattice

The canonical integral lift of a quotient basis coordinate: a long root vector, or the long simple coroot h₁, h₀ at coordinates 12, 13.

Equations

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

theorem TauCeti.DynkinType.f4IntegralShortRootQuotientLift_modular (a : Fin 26) : 1 ⊗ₜ[ℤ] f4IntegralShortRootQuotientLift a = f4ShortRootQuotientLift a

Reduction modulo two of the canonical integral lift is the canonical ambient modular lift.

theorem TauCeti.DynkinType.f4IntegralShortRootQuotientLift_mkQ (a : Fin 26) : f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] f4IntegralShortRootQuotientLift a) = f4ShortRootQuotientBasis a

Reduction of the canonical integral lift represents the corresponding quotient basis coordinate.

theorem TauCeti.DynkinType.f4IntegralRootBracket_quotientLift_mkQ (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] ⁅f4IntegralRootVector (f4SignedSimpleRootIndex k), f4IntegralShortRootQuotientLift a⁆) = f4ShortRootQuotientFirstColumn k a

The bracket of an integral root vector with a canonical lift reduces to the first-order quotient column.

theorem TauCeti.DynkinType.f4IntegralDividedAdjointSquare_quotientLift_mkQ (k : Fin 4 ⊕ Fin 4) (a : Fin 26) : f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] (f4IntegralDividedAdjointSquare k) (f4IntegralShortRootQuotientLift a)) = f4ShortRootQuotientDividedSquareColumn k a

The reduced second integral divided power on a canonical lift is the named quotient divided-square column.

theorem TauCeti.DynkinType.f4ShortRootBaseChangeQuotient_rootExponential_integralShortRootQuotientLift {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (a : Fin 26) : f4ShortRootBaseChangeQuotient ((f4RootExponential k t) (1 ⊗ₜ[ℤ] f4IntegralShortRootQuotientLift a)) = 1 ⊗ₜ[ZMod 2] f4ShortRootQuotientBasis a + t • 1 ⊗ₜ[ZMod 2] f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] ⁅f4IntegralRootVector (f4SignedSimpleRootIndex k), f4IntegralShortRootQuotientLift a⁆) + t ^ 2 • 1 ⊗ₜ[ZMod 2] f4ShortRootSubspace.mkQ (1 ⊗ₜ[ℤ] (f4IntegralDividedAdjointSquare k) (f4IntegralShortRootQuotientLift a))

On every canonical quotient-basis lift, the arbitrary-scalar root exponential is the three-term integral divided-power polynomial, with constant term normalized to the quotient basis. The two remaining terms retain their integral lifts until the concrete quotient-column identification is applied.

theorem TauCeti.DynkinType.f4ShortRootBaseChangeQuotient_rootExponential_quotientColumns {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (a : Fin 26) : f4ShortRootBaseChangeQuotient ((f4RootExponential k t) (1 ⊗ₜ[ℤ] f4IntegralShortRootQuotientLift a)) = 1 ⊗ₜ[ZMod 2] f4ShortRootQuotientBasis a + t • 1 ⊗ₜ[ZMod 2] f4ShortRootQuotientFirstColumn k a + t ^ 2 • 1 ⊗ₜ[ZMod 2] f4ShortRootQuotientDividedSquareColumn k a

The quotient of the genuine integral root exponential on a canonical lift is its canonical quadratic column polynomial, over every commutative algebra of characteristic two.

noncomputable def TauCeti.DynkinType.f4ShortRootQuotientToIdealBaseChange {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] : TensorProduct (ZMod 2) A (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace) →ₗ[A] TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal

Scalar extension of the pinned coordinate equivalence from the modular quotient to the short-root ideal.

Equations

• TauCeti.DynkinType.f4ShortRootQuotientToIdealBaseChange = LinearMap.baseChange A ↑TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv

@[simp]

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealBaseChange_tmul {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (x : f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace) : f4ShortRootQuotientToIdealBaseChange (1 ⊗ₜ[ZMod 2] x) = 1 ⊗ₜ[ZMod 2] f4ShortRootQuotientToIdealEquiv x

noncomputable def TauCeti.DynkinType.f4ShortRootTransportedQuotientPolynomial {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (a : Fin 26) : TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal

The canonical quotient-column polynomial after transport to the short-root ideal.

Equations

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

theorem TauCeti.DynkinType.f4ShortRootExponential_basis_apply {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (a : Fin 26) : (f4ShortRootExponential k t) (1 ⊗ₜ[ZMod 2] f4ShortRootLieIdealBasis a) = 1 ⊗ₜ[ZMod 2] f4ShortRootLieIdealBasis a + t • 1 ⊗ₜ[ZMod 2] f4ShortRootIdealFirstColumn k a + t ^ 2 • 1 ⊗ₜ[ZMod 2] f4ShortRootIdealDividedSquareColumn k a

The target root exponential on a canonical basis vector, written using its named columns.

theorem TauCeti.DynkinType.f4ShortRootQuotientColumns_eq_exponential {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (a : Fin 26) : f4ShortRootTransportedQuotientPolynomial k t a = (f4ShortRootExponential (F4ShortRoot.isogenyReverse k) (t ^ F4ShortRoot.isogenyExponent k)) (1 ⊗ₜ[ZMod 2] f4ShortRootLieIdealBasis a)

The transported canonical quotient-column polynomial is the target short-root exponential with the special-isogeny parameter exponent.

theorem TauCeti.DynkinType.f4ShortRootQuotient_rootExponential_pinning {A : Type u_1} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (t : A) (a : Fin 26) : f4ShortRootQuotientToIdealBaseChange (f4ShortRootBaseChangeQuotient ((f4RootExponential k t) (1 ⊗ₜ[ℤ] f4IntegralShortRootQuotientLift a))) = (f4ShortRootExponential (F4ShortRoot.isogenyReverse k) (t ^ F4ShortRoot.isogenyExponent k)) (1 ⊗ₜ[ZMod 2] f4ShortRootLieIdealBasis a)

After the canonical coordinate identification, the quotient exponential is the target short-root exponential with the special-isogeny parameter exponent.