Divided adjoint squares on the modular F₄ short-root ideal

The second adjoint divided power is formed on the integral Chevalley lattice before reduction modulo two. This file identifies the reduced operator with the reductions of the integral divided-square matrices used in the pinned twenty-six-dimensional representation.

References

• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11, for the special isogeny in characteristic two and its divided-power formulas.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 12.3, for the divided powers of the adjoint action on a Chevalley lattice.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII, for the root coordinates and the simple-root numbering.

theorem TauCeti.DynkinType.f4IntegralDividedAdjointSquare_rootVector_opposite (k : Fin 4 ⊕ Fin 4) : (f4IntegralDividedAdjointSquare k) (f4IntegralRootVector (f4OppositeRootIndex (f4SignedSimpleRootIndex k))) = -f4IntegralRootVector (f4SignedSimpleRootIndex k)

The integral divided square has the expected exceptional opposite-root column.

theorem TauCeti.DynkinType.f4IntegralDividedAdjointSquare_rootVector_eq_zero_of_dividedPower_eq_zero (k : Fin 4 ⊕ Fin 4) (i : Fin 48) (h : Associative.dividedPower 2 ((LieAlgebra.ad ℚ ↥(F4.lieAlgebra valid_F4)) (f4ChevalleyRootVector (f4KillingRoot (f4SignedSimpleRootIndex k)))) • f4ChevalleyRootVector (f4KillingRoot i) = 0) : (f4IntegralDividedAdjointSquare k) (f4IntegralRootVector i) = 0

A rational divided-square zero column remains zero in the integral Chevalley lattice.

theorem TauCeti.DynkinType.f4IntegralDividedAdjointSquare_simpleCoroot_eq_zero (k : Fin 4 ⊕ Fin 4) (i : Fin F4.rank) : (f4IntegralDividedAdjointSquare k) (f4IntegralSimpleCoroot i) = 0

The integral divided square vanishes on each simple-coroot basis column.

noncomputable def TauCeti.DynkinType.f4ModularDividedAdjointSquare (k : Fin 4 ⊕ Fin 4) : Module.End (ZMod 2) f4ModularChevalleyLieAlgebra

The second divided adjoint power after reduction modulo two.

Equations

• TauCeti.DynkinType.f4ModularDividedAdjointSquare k = LinearMap.baseChange (ZMod 2) (TauCeti.DynkinType.f4IntegralDividedAdjointSquare k)

@[simp]

theorem TauCeti.DynkinType.f4ModularDividedAdjointSquare_tmul (k : Fin 4 ⊕ Fin 4) (y : ↥f4ChevalleyLieLattice) : (f4ModularDividedAdjointSquare k) (1 ⊗ₜ[ℤ] y) = 1 ⊗ₜ[ℤ] (f4IntegralDividedAdjointSquare k) y

Reduction modulo two commutes with the integral divided square on pure tensors.

theorem TauCeti.DynkinType.f4ModularDividedAdjointSquare_rootVector_opposite (k : Fin 4 ⊕ Fin 4) : (f4ModularDividedAdjointSquare k) (f4ModularRootVector (f4OppositeRootIndex (f4SignedSimpleRootIndex k))) = f4ModularRootVector (f4SignedSimpleRootIndex k)

Modulo two, the exceptional opposite-root column has coefficient one.

theorem TauCeti.DynkinType.f4ModularDividedAdjointSquare_rootVector_of_long_add_two_short (k : Fin 4 ⊕ Fin 4) (β γ : Fin 48) (hα : f4Length (f4SignedSimpleRootIndex k) = 1) (hβ : f4Length β = 2) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + 2 • f4SimplyConnectedRootDatum.root (f4SignedSimpleRootIndex k)) : (f4ModularDividedAdjointSquare k) (f4ModularRootVector β) = f4ModularRootVector γ

A short-source second divided power carries a long root to another long root with unit coefficient after reduction modulo two.

theorem TauCeti.DynkinType.f4ModularDividedAdjointSquare_rootVector_eq_zero_of_dividedPower_eq_zero (k : Fin 4 ⊕ Fin 4) (β : Fin 48) (h : Associative.dividedPower 2 ((LieAlgebra.ad ℚ ↥(F4.lieAlgebra valid_F4)) (f4ChevalleyRootVector (f4KillingRoot (f4SignedSimpleRootIndex k)))) • f4ChevalleyRootVector (f4KillingRoot β) = 0) : (f4ModularDividedAdjointSquare k) (f4ModularRootVector β) = 0

A rational divided-square zero column remains zero after integral reduction.

theorem TauCeti.DynkinType.f4ModularDividedAdjointSquare_rootVector_eq_zero_of_short (k : Fin 4 ⊕ Fin 4) (i : Fin 48) (hi : f4Length i = 1) (hopp : i ≠ f4OppositeRootIndex (f4SignedSimpleRootIndex k)) : (f4ModularDividedAdjointSquare k) (f4ModularRootVector i) = 0

Modulo two, every non-opposite short-root column of the divided square vanishes.

theorem TauCeti.DynkinType.f4ModularDividedAdjointSquare_rootVector_eq_zero_of_no_endpoint (k : Fin 4 ⊕ Fin 4) (β : Fin 48) (hopp : β ≠ f4OppositeRootIndex (f4SignedSimpleRootIndex k)) (hno : ∀ (γ : Fin 48), f4SimplyConnectedRootDatum.root γ ≠ f4SimplyConnectedRootDatum.root β + 2 • f4SimplyConnectedRootDatum.root (f4SignedSimpleRootIndex k)) : (f4ModularDividedAdjointSquare k) (f4ModularRootVector β) = 0

Modulo two, the divided square vanishes when the second root-string endpoint is absent.

theorem TauCeti.DynkinType.f4ModularDividedAdjointSquare_simpleCoroot_eq_zero (k : Fin 4 ⊕ Fin 4) (i : Fin F4.rank) : (f4ModularDividedAdjointSquare k) (f4ModularSimpleCoroot i) = 0

The modular divided square vanishes on every simple-coroot basis column.

def TauCeti.DynkinType.f4DividedSquareTarget : Fin 4 ⊕ Fin 4 → Fin 26 → Fin 26

The target coordinate in a divided-square matrix column.

Equations

• TauCeti.DynkinType.f4DividedSquareTarget (Sum.inl i) = TauCeti.F4ShortRoot.raisingDividedSquareTarget i
• TauCeti.DynkinType.f4DividedSquareTarget (Sum.inr i) = TauCeti.F4ShortRoot.loweringDividedSquareTarget i

@[simp]

theorem TauCeti.DynkinType.f4DividedSquareTarget_inl (i : Fin 4) (b : Fin 26) : f4DividedSquareTarget (Sum.inl i) b = F4ShortRoot.raisingDividedSquareTarget i b

@[simp]

theorem TauCeti.DynkinType.f4DividedSquareTarget_inr (i : Fin 4) (b : Fin 26) : f4DividedSquareTarget (Sum.inr i) b = F4ShortRoot.loweringDividedSquareTarget i b

def TauCeti.DynkinType.f4DividedSquareCoeff : Fin 4 ⊕ Fin 4 → Fin 26 → ℤ

The integral coefficient in a divided-square matrix column.

Equations

• TauCeti.DynkinType.f4DividedSquareCoeff (Sum.inl i) = TauCeti.F4ShortRoot.raisingDividedSquareCoeff i
• TauCeti.DynkinType.f4DividedSquareCoeff (Sum.inr i) = TauCeti.F4ShortRoot.loweringDividedSquareCoeff i

@[simp]

theorem TauCeti.DynkinType.f4DividedSquareCoeff_inl (i : Fin 4) (b : Fin 26) : f4DividedSquareCoeff (Sum.inl i) b = F4ShortRoot.raisingDividedSquareCoeff i b

@[simp]

theorem TauCeti.DynkinType.f4DividedSquareCoeff_inr (i : Fin 4) (b : Fin 26) : f4DividedSquareCoeff (Sum.inr i) b = F4ShortRoot.loweringDividedSquareCoeff i b

@[simp]

theorem TauCeti.DynkinType.rootDividedSquareMatrix_apply (k : Fin 4 ⊕ Fin 4) (a b : Fin 26) : F4ShortRoot.rootDividedSquareMatrix k a b = if a = f4DividedSquareTarget k b then f4DividedSquareCoeff k b else 0

Each sparse divided-square matrix entry is its column coefficient at the target row.

theorem TauCeti.DynkinType.f4DividedSquareCoeff_mod_two_eq_zero_iff (k : Fin 4 ⊕ Fin 4) (b : Fin 26) : ↑(f4DividedSquareCoeff k b) = 0 ↔ f4ShortRootWeight b ≠ f4Root (f4OppositeRootIndex (f4SignedSimpleRootIndex k))

The coefficient vanishes modulo two exactly off the opposite-root weight.

theorem TauCeti.DynkinType.f4DividedSquareCoeff_mod_two_eq_zero_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) (b : Fin 26) : ↑(f4DividedSquareCoeff k b) = 0

The divided-square coefficient vanishes modulo two for a long signed-simple source.

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

The divided-square matrix, viewed as an endomorphism of the canonical short-root ideal.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4ShortRootDividedAdjointSquare_toMatrix (k : Fin 4 ⊕ Fin 4) : (LinearMap.toMatrix f4ShortRootLieIdealBasis f4ShortRootLieIdealBasis) (f4ShortRootDividedAdjointSquare k) = (F4ShortRoot.rootDividedSquareMatrix k).map Int.cast

The divided-square endomorphism is realized, in the canonical short-root basis, by the reduction modulo two of the integral divided-square matrix.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootDividedAdjointSquare_basis (k : Fin 4 ⊕ Fin 4) (b : Fin 26) : (f4ShortRootDividedAdjointSquare k) (f4ShortRootLieIdealBasis b) = ↑(f4DividedSquareCoeff k b) • f4ShortRootLieIdealBasis (f4DividedSquareTarget k b)

Each basis column of the divided-square endomorphism has the advertised sparse form.

theorem TauCeti.DynkinType.f4ModularDividedAdjointSquare_basis (k : Fin 4 ⊕ Fin 4) (b : Fin 26) : (f4ModularDividedAdjointSquare k) ↑(f4ShortRootLieIdealBasis b) = ↑((f4ShortRootDividedAdjointSquare k) (f4ShortRootLieIdealBasis b))

The reduced ambient divided square and its matrix realization agree on every basis vector of the modular short-root ideal.

@[simp]

theorem TauCeti.DynkinType.coe_f4ShortRootDividedAdjointSquare_apply (k : Fin 4 ⊕ Fin 4) (y : ↥f4ShortRootLieIdeal) : ↑((f4ShortRootDividedAdjointSquare k) y) = (f4ModularDividedAdjointSquare k) ↑y

The reduced ambient divided square agrees with its matrix realization on every element of the modular short-root ideal.