Root-subgroup stability of the represented modular F4 flag

The modular root exponentials conjugate the represented adjoint range and ideal into themselves. Transporting this matrix stability to the cotangent adjoint comodule gives block triangularity for root-subgroup generators with respect to the adapted represented flag.

noncomputable def TauCeti.DynkinType.f4ShortRootBaseChangeAdjointMatrixLinearMap {A : Type} [CommRing A] [Algebra (ZMod 2) A] : TensorProduct ℤ A ↥f4ChevalleyLieLattice →ₗ[A] Matrix (Fin 26) (Fin 26) A

The scalar-extended short-root adjoint representation in its canonical matrix basis.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4ShortRootBaseChangeAdjointMatrixLinearMap_apply {A : Type} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) : f4ShortRootBaseChangeAdjointMatrixLinearMap x = (LinearMap.toMatrix (Module.Basis.baseChange A f4ShortRootLieIdealBasis) (Module.Basis.baseChange A f4ShortRootLieIdealBasis)) (f4ShortRootBaseChangeAdjoint x)

Evaluate the scalar-extended adjoint map in matrix coordinates.

theorem TauCeti.DynkinType.f4ShortRootBaseChangeAdjointMatrixLinearMap_cancel_tmul {A : Type} [CommRing A] [Algebra (ZMod 2) A] (a : A) (X : f4ModularChevalleyLieAlgebra) : f4ShortRootBaseChangeAdjointMatrixLinearMap ((cancelBaseChange ℤ (ZMod 2) A ↥f4ChevalleyLieLattice) (a ⊗ₜ[ZMod 2] X)) = a • f4ShortRootAdjointMatrixBaseChange X

On a pure tensor, the scalar-extended adjoint matrix is the entrywise scalar extension of the modular adjoint matrix.

theorem TauCeti.DynkinType.f4ShortRootBaseChangeAdjointMatrix_mem_range {A : Type} [CommRing A] [Algebra (ZMod 2) A] (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) : f4ShortRootBaseChangeAdjointMatrixLinearMap x ∈ f4ShortRootRepresentedRangeMatrixBaseChange

Every scalar-extended represented adjoint matrix belongs to the represented range span.

theorem TauCeti.DynkinType.f4ShortRootRoot_lieConj_adjoint {A : Type} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) (x : TensorProduct ℤ A ↥f4ChevalleyLieLattice) : ((↑↑((F4ShortRoot.rootSubgroupPoints k A) u)).lieConj (Units.invertible ↑((F4ShortRoot.rootSubgroupPoints k A) u))) (f4ShortRootBaseChangeAdjointMatrixLinearMap x) = f4ShortRootBaseChangeAdjointMatrixLinearMap ((f4RootExponential k (Multiplicative.toAdd u)) x)

Root conjugation carries a represented adjoint matrix to the adjoint matrix of the integrally transformed ambient vector.

theorem TauCeti.DynkinType.f4ShortRootRootConj_mem_representedRange {A : Type} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) {X : Matrix (Fin 26) (Fin 26) A} (hX : X ∈ f4ShortRootRepresentedRangeMatrixBaseChange) : ((↑↑((F4ShortRoot.rootSubgroupPoints k A) u)).lieConj (Units.invertible ↑((F4ShortRoot.rootSubgroupPoints k A) u))) X ∈ f4ShortRootRepresentedRangeMatrixBaseChange

Carrier root-subgroup conjugation preserves the represented range matrix span.

theorem TauCeti.DynkinType.f4ShortRootBaseChangeAdjointMatrix_mem_ideal {A : Type} [CommRing A] [Algebra (ZMod 2) A] (z : TensorProduct (ZMod 2) A ↥f4ShortRootLieIdeal) : f4ShortRootBaseChangeAdjointMatrixLinearMap (f4ShortRootBaseChangeInclusion z) ∈ f4ShortRootRepresentedIdealMatrixBaseChange

The represented matrix of an element in the scalar-extended short-root ideal belongs to the represented ideal span.

theorem TauCeti.DynkinType.f4ShortRootRootConj_mem_representedIdeal {A : Type} [CommRing A] [Algebra (ZMod 2) A] (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) {X : Matrix (Fin 26) (Fin 26) A} (hX : X ∈ f4ShortRootRepresentedIdealMatrixBaseChange) : ((↑↑((F4ShortRoot.rootSubgroupPoints k A) u)).lieConj (Units.invertible ↑((F4ShortRoot.rootSubgroupPoints k A) u))) X ∈ f4ShortRootRepresentedIdealMatrixBaseChange

Carrier root-subgroup conjugation preserves the represented ideal matrix span.

theorem TauCeti.DynkinType.f4ShortRootRootSubgroup_adjoint_blockTriangular {A : Type} [CommRing A] [Algebra (ZMod 2) A] (g : ↑(HopfAlgebra.points ↧A)) (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) (hg : (GeneralLinear.pointsMulEquiv 26) g = ↑((F4ShortRoot.rootSubgroupPoints k A) u)) : ((Comodule.coefficientMatrix f4ShortRootCotangentFlagBasis).map ⇑g.ofConv).BlockTriangular (⇑OrderDual.toDual ∘ f4ShortRootCotangentFlagWeight)

Every short-root carrier root point acts block triangularly on the represented flag.