The short-root type-F4 carrier over the prime field of characteristic two

The short-root type-F₄ carrier over ℤ is the Kostant toral closure of the twenty-six-dimensional module V(ϖ₄) inside GL₂₆: the largest Hopf ideal of O(GL₂₆/ℤ) killed by the coordinate maps of the eight numbered simple root subgroups and of the rank-four weight torus. This file forms the companion carrier over the prime field 𝔽₂: the closed subgroup scheme of GL₂₆ over 𝔽₂ generated by the reductions of those same coordinate maps.

Over 𝔽₂ the defining ideal is again maximal among Hopf ideals killed by the generators, this time by construction. That maximality is what lets a homomorphism to GL₂₆ satisfying the generator equations be restricted to an endomorphism of the carrier, and it is not available for the base change of the integral carrier, whose defining ideal is maximal over ℤ only: new equations can appear over a base that is not flat. The two carriers are compared in the honest direction only, and no flatness is asserted.

The root subgroups and weight torus are the reductions of the integral ones. Their matrix-valued points and functoriality are developed in PrimeField.PointsFunctor; Frobenius is developed in PrimeField.Frobenius.

The carrier is not identified with the pinned simply connected group scheme of type F₄, and constructions on it transfer to that group scheme only along such an identification, once one is proved.

Main definitions

• TauCeti.F4ShortRoot.PrimeField.generator: the reduced coordinate maps of the eight numbered simple root subgroups and of the weight torus.
• TauCeti.F4ShortRoot.PrimeField.groupScheme: the closed subgroup scheme of GL₂₆ over 𝔽₂ they generate, with carrierι its closed immersion into GL₂₆.
• TauCeti.F4ShortRoot.PrimeField.rootSubgroup and TauCeti.F4ShortRoot.PrimeField.weightTorus: the generators, factored through it.

Main results

• TauCeti.F4ShortRoot.PrimeField.baseChangePresentationIdeal_le_definingIdeal and TauCeti.F4ShortRoot.PrimeField.groupScheme_hom_ext: the honest one-way comparison with the integral presentation and rigidity of morphisms out of the generated carrier.

References

The construction is motivated by the Chevalley--Demazure construction on the twenty-six-dimensional module over the prime field; see R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1, and J. E. Humphreys, Linear Algebraic Groups, §26. The weight conventions follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII.

@[reducible, inline]

noncomputable abbrev TauCeti.F4ShortRoot.PrimeField.generatorCodomain : (Fin 4 ⊕ Fin 4) ⊕ Unit → CommHopfAlgCat (ZMod 2)

The coordinate Hopf algebra receiving a reduced root-subgroup or weight-torus generator: that of the additive group over 𝔽₂ at a root index, and that of the rank-four split torus over 𝔽₂ at the torus index.

Equations

• TauCeti.F4ShortRoot.PrimeField.generatorCodomain (Sum.inl val) = TauCeti.AdditiveGroup.coordinateHopfAlgebra (ZMod 2)
• TauCeti.F4ShortRoot.PrimeField.generatorCodomain (Sum.inr val) = (TauCeti.DiagonalizableGroup.coordinateRing (ZMod 2) (TauCeti.SplitTorus.characterGroup (Fin 4))).obj

noncomputable def TauCeti.F4ShortRoot.PrimeField.generator (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26 ⟶ generatorCodomain j

The generating coordinate maps of the short-root type-F₄ carrier over 𝔽₂: the reductions of the eight numbered simple root-subgroup coordinate maps and of the weight-torus coordinate map, transported into the coordinate Hopf algebras formed directly over 𝔽₂.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.F4ShortRoot.PrimeField.generator (Sum.inr val) = TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ (ZMod 2) TauCeti.DynkinType.f4ShortRootWeight

theorem TauCeti.F4ShortRoot.PrimeField.generator_inl (k : Fin 4 ⊕ Fin 4) : generator (Sum.inl k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator CartanMatrix.F₄.transpose) (serreH ℚ CartanMatrix.F₄.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis (ZMod 2) k

At a root index the generating family is the reduced root-subgroup coordinate map.

theorem TauCeti.F4ShortRoot.PrimeField.generator_inr : generator (Sum.inr ()) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ (ZMod 2) DynkinType.f4ShortRootWeight

At the torus index the generating family is the reduced weight-torus coordinate map.

noncomputable def TauCeti.F4ShortRoot.PrimeField.definingIdeal : HopfIdeal (ZMod 2) ↑(GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26)

The Hopf ideal cutting out the short-root type-F₄ carrier over 𝔽₂ inside GL₂₆: the largest Hopf ideal of O(GL₂₆/𝔽₂) killed by all the reduced generators.

Equations

• TauCeti.F4ShortRoot.PrimeField.definingIdeal = TauCeti.CommHopfAlgCat.commonKernelHopfIdeal TauCeti.F4ShortRoot.PrimeField.generator

theorem TauCeti.F4ShortRoot.PrimeField.definingIdeal_def : definingIdeal = CommHopfAlgCat.commonKernelHopfIdeal generator

The defining ideal is the common-kernel ideal of the reduced generators.

@[reducible, inline]

noncomputable abbrev TauCeti.F4ShortRoot.PrimeField.coordinateHopfAlgebra (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : CommHopfAlgCat k

The coordinate Hopf algebra of the scalar extension of the short-root prime-field carrier.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.F4ShortRoot.PrimeField.finiteTypeCoordinateHopfAlgebra : FiniteTypeCommHopfAlgCat (ZMod 2)

The coordinate Hopf algebra of the short-root type-F₄ carrier over 𝔽₂, bundled with its finite-type property. Its scalar extension to an 𝔽₂-algebra k is coordinateHopfAlgebra k.

Equations

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

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.finiteTypeCoordinateHopfAlgebra_baseChange_obj (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : finiteTypeCoordinateHopfAlgebra.baseChange.obj = coordinateHopfAlgebra k

The finite-type package base-changes to the carrier's coordinate Hopf algebra.

@[reducible, inline]

noncomputable abbrev TauCeti.F4ShortRoot.PrimeField.groupScheme : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧(ZMod 2)))

The short-root type-F₄ carrier over 𝔽₂: the closed subgroup scheme of GL₂₆ over 𝔽₂ generated by the reductions of the numbered simple root subgroups and of the weight torus.

Equations

• TauCeti.F4ShortRoot.PrimeField.groupScheme = TauCeti.GeneralLinear.generatedGroupScheme 26 TauCeti.F4ShortRoot.PrimeField.generator

theorem TauCeti.F4ShortRoot.PrimeField.groupScheme_def : groupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) definingIdeal

The quotient-spectrum presentation of the carrier over 𝔽₂.

noncomputable def TauCeti.F4ShortRoot.PrimeField.carrierι : groupScheme ⟶ GeneralLinear.groupScheme (ZMod 2) 26

The canonical inclusion of the carrier over 𝔽₂ into GL₂₆.

Equations

• TauCeti.F4ShortRoot.PrimeField.carrierι = TauCeti.GeneralLinear.generatedGroupSchemeι 26 TauCeti.F4ShortRoot.PrimeField.generator

theorem TauCeti.F4ShortRoot.PrimeField.carrierι_def : carrierι = GeneralLinear.generatedGroupSchemeι 26 generator

The ambient inclusion is the one of the generated subgroup scheme.

instance TauCeti.F4ShortRoot.PrimeField.isClosedImmersion_carrierι : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left carrierι.hom.hom)

The carrier over 𝔽₂ is a closed subgroup scheme of GL₂₆.

noncomputable def TauCeti.F4ShortRoot.PrimeField.rootSubgroup (k : Fin 4 ⊕ Fin 4) : AdditiveGroup.groupScheme (ZMod 2) ⟶ groupScheme

A positive or negative numbered simple root subgroup of the carrier over 𝔽₂.

Equations

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

theorem TauCeti.F4ShortRoot.PrimeField.rootSubgroup_def (k : Fin 4 ⊕ Fin 4) : rootSubgroup k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (GeneralLinear.generatorToGeneratedGroupScheme 26 generator (Sum.inl k))

The numbered root subgroup is the generator of the generated subgroup scheme it indexes.

noncomputable def TauCeti.F4ShortRoot.PrimeField.weightTorus : SplitTorus.groupScheme (ZMod 2) (Fin 4) ⟶ groupScheme

The rank-four split weight torus in the carrier over 𝔽₂.

Equations

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

theorem TauCeti.F4ShortRoot.PrimeField.weightTorus_def : weightTorus = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (GeneralLinear.generatorToGeneratedGroupScheme 26 generator (Sum.inr ()))

The weight torus is the generator of the generated subgroup scheme it indexes.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.rootSubgroup_comp_carrierι (k : Fin 4 ⊕ Fin 4) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) carrierι = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧(ZMod 2)).map (generator (Sum.inl k)).op) (CategoryTheory.eqToHom ⋯))

Including a numbered root subgroup into GL₂₆ recovers the reduced generating morphism.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.weightTorus_comp_carrierι : CategoryTheory.CategoryStruct.comp weightTorus carrierι = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec ↧(ZMod 2)).map (generator (Sum.inr ())).op) (CategoryTheory.eqToHom ⋯))

Including the weight torus into GL₂₆ recovers the reduced generating morphism.

theorem TauCeti.F4ShortRoot.PrimeField.groupScheme_hom_ext {Y : CommHopfAlgCat (ZMod 2)} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧(ZMod 2)).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 4 ⊕ Fin 4), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g) (htorus : CategoryTheory.CategoryStruct.comp weightTorus f = CategoryTheory.CategoryStruct.comp weightTorus g) : f = g

Two morphisms out of the prime-field carrier agree when they agree on all eight numbered root subgroups and on the weight torus.

theorem TauCeti.F4ShortRoot.PrimeField.groupScheme_hom_ext_iff {Y : CommHopfAlgCat (ZMod 2)} {f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧(ZMod 2)).obj (Opposite.op Y)} : f = g ↔ (∀ (k : Fin 4 ⊕ Fin 4), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g) ∧ CategoryTheory.CategoryStruct.comp weightTorus f = CategoryTheory.CategoryStruct.comp weightTorus g

theorem TauCeti.F4ShortRoot.PrimeField.baseChangePresentationIdeal_le_definingIdeal : UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (serreRootGenerator CartanMatrix.F₄.transpose) (serreH ℚ CartanMatrix.F₄.transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.f4ShortRootWeight (ZMod 2) ≤ definingIdeal

The carrier over 𝔽₂ is a closed subgroup scheme of the base change of the integral short-root carrier. The reverse containment is not claimed: the integral defining ideal is the largest Hopf ideal killed by the generators over ℤ only, and new equations can appear over a base that is not flat.