The short-root type-G2 carrier over the prime field of characteristic three

The short-root type-G₂ carrier over ℤ is the Kostant toral closure of the seven-dimensional module V(ϖ₁) inside GL₇: the largest Hopf ideal of O(GL₇/ℤ) killed by the coordinate maps of the four numbered simple root subgroups and of the rank-two 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 the largest Hopf ideal 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 what the special isogeny of type G₂ in characteristic three needs. 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 therefore compared in one direction only, and no flatness is asserted.

The root subgroups and the weight torus are the reductions of the integral ones, so their matrices and the pinning equation between them are not re-derived.

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

Main definitions

• TauCeti.G2ShortRoot.PrimeField.generator: the reduced coordinate maps of the four numbered simple root subgroups and of the weight torus.
• TauCeti.G2ShortRoot.PrimeField.definingIdeal: the largest Hopf ideal of O(GL₇/𝔽₃) they kill.
• TauCeti.G2ShortRoot.PrimeField.carrierAlgebra and TauCeti.G2ShortRoot.PrimeField.carrierGenericMatrix: the carrier's coordinate Hopf algebra and its universal matrix-valued point.
• TauCeti.G2ShortRoot.PrimeField.groupScheme: the closed subgroup scheme of GL₇ over 𝔽₃ they generate, with TauCeti.G2ShortRoot.PrimeField.carrierι its closed immersion into GL₇.
• TauCeti.G2ShortRoot.PrimeField.rootSubgroup and TauCeti.G2ShortRoot.PrimeField.weightTorus: those generators, factored through it.

Main results

• TauCeti.G2ShortRoot.PrimeField.groupScheme_hom_ext: a morphism from the carrier to an affine group scheme presented as hopfSpec Y is determined by its restrictions to the four numbered root subgroups and to the weight torus.
• TauCeti.G2ShortRoot.PrimeField.baseChangePresentationIdeal_le_definingIdeal: the carrier is a closed subgroup scheme of the base change of the integral short-root carrier.

References

The construction is the Chevalley--Demazure construction on the seven-dimensional module, carried out over the prime field; see J. E. Humphreys, Linear Algebraic Groups, §26, and R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1. The weight conventions follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX. The reason the prime field, rather than ℤ, is the base for a carrier carrying the special isogeny is the maximality of the defining ideal explained above; see R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.

@[reducible, inline]

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

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-two split torus over 𝔽₃ at the torus index.

Equations

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

noncomputable def TauCeti.G2ShortRoot.PrimeField.generator (j : (Fin 2 ⊕ Fin 2) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra (ZMod 3) 7 ⟶ generatorCodomain j

The generating coordinate maps of the short-root type-G₂ carrier over 𝔽₃: the reductions of the four 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.G2ShortRoot.PrimeField.generator (Sum.inr val) = TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ (ZMod 3) TauCeti.G2ShortRoot.weight

theorem TauCeti.G2ShortRoot.PrimeField.generator_inl (k : Fin 2 ⊕ Fin 2) : generator (Sum.inl k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis (ZMod 3) k

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

theorem TauCeti.G2ShortRoot.PrimeField.generator_inr : generator (Sum.inr ()) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ (ZMod 3) weight

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

noncomputable def TauCeti.G2ShortRoot.PrimeField.definingIdeal : HopfIdeal (ZMod 3) ↑(GeneralLinear.coordinateHopfAlgebra (ZMod 3) 7)

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

Equations

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

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

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

@[reducible, inline]

noncomputable abbrev TauCeti.G2ShortRoot.PrimeField.carrierAlgebra : CommHopfAlgCat (ZMod 3)

The coordinate Hopf algebra of the short-root type-G₂ carrier over 𝔽₃.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.G2ShortRoot.PrimeField.carrierQuotient : GeneralLinear.coordinateHopfAlgebra (ZMod 3) 7 ⟶ carrierAlgebra

The quotient map of the coordinate Hopf algebra of GL₇ onto that of the carrier.

Equations

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

noncomputable def TauCeti.G2ShortRoot.PrimeField.carrierGenericMatrix : Matrix (Fin 7) (Fin 7) ↑carrierAlgebra

The universal point of the carrier: the generic matrix of GL₇ pushed to the carrier's coordinate Hopf algebra.

Equations

• TauCeti.G2ShortRoot.PrimeField.carrierGenericMatrix = (TauCeti.GeneralLinear.genericMatrix (ZMod 3) 7).map ⇑↑(CommHopfAlgCat.Hom.hom TauCeti.G2ShortRoot.PrimeField.carrierQuotient)

theorem TauCeti.G2ShortRoot.PrimeField.carrierGenericMatrix_def : carrierGenericMatrix = (GeneralLinear.genericMatrix (ZMod 3) 7).map ⇑↑(CommHopfAlgCat.Hom.hom carrierQuotient)

The universal point of the carrier is the generic matrix of GL₇ pushed along carrierQuotient. Consumers should unfold carrierGenericMatrix through this lemma.

noncomputable def TauCeti.G2ShortRoot.PrimeField.groupScheme : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧(ZMod 3)))

The short-root type-G₂ 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.G2ShortRoot.PrimeField.groupScheme = TauCeti.GeneralLinear.generatedGroupScheme 7 TauCeti.G2ShortRoot.PrimeField.generator

theorem TauCeti.G2ShortRoot.PrimeField.groupScheme_def : groupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra (ZMod 3) 7) definingIdeal

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

theorem TauCeti.G2ShortRoot.PrimeField.groupScheme_eq_commonKernelSpec : groupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra (ZMod 3) 7) (CommHopfAlgCat.commonKernelHopfIdeal generator)

The carrier is represented by the quotient of the ambient coordinate Hopf algebra by the common kernel of its generators.

theorem TauCeti.G2ShortRoot.PrimeField.groupScheme_eq_generatedGroupScheme : groupScheme = GeneralLinear.generatedGroupScheme 7 generator

The carrier is the subgroup scheme generated by the reduced generators.

noncomputable def TauCeti.G2ShortRoot.PrimeField.carrierι : groupScheme ⟶ GeneralLinear.groupScheme (ZMod 3) 7

The canonical inclusion of the carrier over 𝔽₃ into GL₇.

Equations

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

theorem TauCeti.G2ShortRoot.PrimeField.carrierι_def : carrierι = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom groupScheme_eq_generatedGroupScheme) (GeneralLinear.generatedGroupSchemeι 7 generator)

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

instance TauCeti.G2ShortRoot.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.G2ShortRoot.PrimeField.rootSubgroup (k : Fin 2 ⊕ Fin 2) : AdditiveGroup.groupScheme (ZMod 3) ⟶ 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.G2ShortRoot.PrimeField.rootSubgroup_def (k : Fin 2 ⊕ Fin 2) : rootSubgroup k = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GeneralLinear.generatorToGeneratedGroupScheme 7 generator (Sum.inl k)) (CategoryTheory.eqToHom ⋯))

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

noncomputable def TauCeti.G2ShortRoot.PrimeField.weightTorus : SplitTorus.groupScheme (ZMod 3) (Fin 2) ⟶ groupScheme

The rank-two split weight torus in the carrier over 𝔽₃.

Equations

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

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

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

@[simp]

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

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

@[simp]

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

Including the weight torus into GL₇ recovers the reduced generating morphism.

theorem TauCeti.G2ShortRoot.PrimeField.groupScheme_hom_ext {Y : CommHopfAlgCat (ZMod 3)} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧(ZMod 3)).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 2 ⊕ Fin 2), 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 from the carrier over 𝔽₃ to an affine group scheme presented as hopfSpec Y agree when they agree on all four numbered simple root subgroups and on the weight torus.

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

theorem TauCeti.G2ShortRoot.PrimeField.baseChangePresentationIdeal_le_definingIdeal : UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (serreRootGenerator CartanMatrix.G₂) (serreH ℚ CartanMatrix.G₂) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis weight (ZMod 3) ≤ 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.