The subgroup generated by the scalar-extended short-root type-G2 generators

The short-root type-G₂ carrier over 𝔽₃ is generated by four numbered root subgroups and its rank-two weight torus. After extending their coordinate maps to a commutative 𝔽₃-algebra k, their common kernel defines a closed subgroup of GL₇ over k. The scalar extension of the prime-field carrier equals this generated subgroup: formation of the common-kernel Hopf ideal commutes with free scalar extension, and every 𝔽₃-algebra is free over 𝔽₃. The coordinate isomorphism is characterized by its compatibility with the ambient quotient maps.

Recognition as the pinned simply connected group scheme of type G₂ requires a further identification.

The coordinate Hopf algebra here is the common target of the smoothness, connectedness and standard-representation results for the generated subgroup.

Main declarations

In the namespace TauCeti.G2ShortRoot.PrimeField:

• generatedDefiningIdeal and generatedCoordinateHopfAlgebra: the common kernel of the scalar-extended generator coordinate maps, and the resulting quotient of O(GL₇/k).
• generatedCoordinateMap: the quotient coordinate morphism, with kernel generatedDefiningIdeal (generatedCoordinateMap_ker).
• generatedCoordinateDesc: the factorization through the generated subgroup of any coordinate morphism killing its defining ideal, unique by generatedCoordinateDesc_unique.
• baseChangeGeneratorLift: each scalar-extended generator factored through the generated subgroup, as TauCeti.CommHopfAlgCat.commonKernelLift; unique by baseChangeGeneratorLift_unique.
• baseChangeDefiningIdeal_eq_generatedDefiningIdeal: generation commutes with scalar extension.
• coordinateHopfAlgebraGeneratedIso: the scalar-extended carrier identified with the generated subgroup, compatibly with the ambient quotient maps.
• finiteTypeGeneratedCoordinateHopfAlgebra: the generated subgroup as a finite-type commutative Hopf algebra, using the Algebra.FiniteType instance on generatedCoordinateHopfAlgebra.

References

• J. E. Humphreys, Linear Algebraic Groups, §§26–27.
• J. S. Milne, Algebraic Groups (2017), §2.h.

The interface follows the generated-subgroup construction for the type-E₇ minuscule carrier in TauCeti.Algebra.Lie.E7.Minuscule.Generated.Basic.

@[reducible, inline]

noncomputable abbrev TauCeti.G2ShortRoot.PrimeField.baseChangeGeneratorCodomain (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : (Fin 2 ⊕ Fin 2) ⊕ Unit → CommHopfAlgCat k

The scalar extensions of the coordinate Hopf algebras of the numbered root subgroups and weight torus.

Equations

• TauCeti.G2ShortRoot.PrimeField.baseChangeGeneratorCodomain k j = TauCeti.CommHopfAlgCat.baseChange (TauCeti.G2ShortRoot.PrimeField.generatorCodomain j)

noncomputable def TauCeti.G2ShortRoot.PrimeField.baseChangeGenerator (k : Type u) [CommRing k] [Algebra (ZMod 3) k] (j : (Fin 2 ⊕ Fin 2) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra k 7 ⟶ baseChangeGeneratorCodomain k j

The root-subgroup and torus coordinate maps after scalar extension to k, with the ambient coordinate algebra identified with O(GL₇/k).

Equations

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

theorem TauCeti.G2ShortRoot.PrimeField.baseChangeGenerator_def (k : Type u) [CommRing k] [Algebra (ZMod 3) k] (j : (Fin 2 ⊕ Fin 2) ⊕ Unit) : baseChangeGenerator k j = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 3) k 7).inv (CommHopfAlgCat.baseChangeMap (generator j))

A scalar-extended generator is the base change of the corresponding prime-field coordinate map, transported across the canonical coordinate-algebra identification for GL₇.

noncomputable def TauCeti.G2ShortRoot.PrimeField.generatedDefiningIdeal (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k 7)

The defining ideal of the subgroup generated by the scalar-extended numbered root subgroups and weight torus.

Equations

• TauCeti.G2ShortRoot.PrimeField.generatedDefiningIdeal k = TauCeti.CommHopfAlgCat.commonKernelHopfIdeal (TauCeti.G2ShortRoot.PrimeField.baseChangeGenerator k)

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedDefiningIdeal_def (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : generatedDefiningIdeal k = CommHopfAlgCat.commonKernelHopfIdeal (baseChangeGenerator k)

The generated subgroup is defined by the common kernel of the scalar-extended generator maps.

theorem TauCeti.G2ShortRoot.PrimeField.le_generatedDefiningIdeal_iff (k : Type u) [CommRing k] [Algebra (ZMod 3) k] (J : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k 7)) : J ≤ generatedDefiningIdeal k ↔ ∀ (j : (Fin 2 ⊕ Fin 2) ⊕ Unit), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (baseChangeGenerator k j))).toRingHom

A Hopf ideal lies below the generated subgroup's defining ideal exactly when every scalar-extended generator coordinate map kills it.

noncomputable def TauCeti.G2ShortRoot.PrimeField.baseChangeDefiningIdeal (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k 7)

The defining ideal of the prime-field carrier, transported into O(GL₇/k).

Equations

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

theorem TauCeti.G2ShortRoot.PrimeField.baseChangeDefiningIdeal_def (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : baseChangeDefiningIdeal k = (CommHopfAlgCat.baseChangeHopfIdeal definingIdeal).comapOfSurjective (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 3) k 7).inv) ⋯

The transported defining ideal is the inverse image of the scalar extension of the prime-field ideal under the canonical coordinate-algebra identification for GL₇.

noncomputable def TauCeti.G2ShortRoot.PrimeField.generatedCoordinateHopfAlgebra (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : CommHopfAlgCat k

The coordinate Hopf algebra of the subgroup generated after scalar extension.

Equations

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

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateHopfAlgebra_def (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : generatedCoordinateHopfAlgebra k = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k 7) (generatedDefiningIdeal k)

The generated subgroup has the quotient coordinate Hopf algebra of its defining ideal.

noncomputable def TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : GeneralLinear.coordinateHopfAlgebra k 7 ⟶ generatedCoordinateHopfAlgebra k

The quotient coordinate morphism O(GL₇/k) ⟶ O(G), representing the closed immersion into GL₇ of the subgroup G generated by the scalar-extended root subgroups and weight torus.

Equations

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

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap_surjective (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (generatedCoordinateMap k))

The generated subgroup's coordinate morphism is surjective.

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap_ker (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : RingHom.ker (CommHopfAlgCat.Hom.hom (generatedCoordinateMap k)) = (generatedDefiningIdeal k).toIdeal

The kernel of the generated subgroup's coordinate morphism is its defining ideal.

noncomputable def TauCeti.G2ShortRoot.PrimeField.generatedCoordinateDesc (k : Type u) [CommRing k] [Algebra (ZMod 3) k] {B : CommHopfAlgCat k} (f : GeneralLinear.coordinateHopfAlgebra k 7 ⟶ B) (hf : (generatedDefiningIdeal k).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) : generatedCoordinateHopfAlgebra k ⟶ B

A coordinate morphism out of O(GL₇/k) killing the generated subgroup's defining ideal, factored through the generated subgroup. This is CommHopfAlgCat.liftQuotient, with its source identified with generatedCoordinateHopfAlgebra k; that identification is not visible outside this module.

Equations

• TauCeti.G2ShortRoot.PrimeField.generatedCoordinateDesc k f hf = TauCeti.CommHopfAlgCat.liftQuotient (TauCeti.G2ShortRoot.PrimeField.generatedDefiningIdeal k) f hf

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap_comp_generatedCoordinateDesc (k : Type u) [CommRing k] [Algebra (ZMod 3) k] {B : CommHopfAlgCat k} (f : GeneralLinear.coordinateHopfAlgebra k 7 ⟶ B) (hf : (generatedDefiningIdeal k).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap k) (generatedCoordinateDesc k f hf) = f

Composing the quotient coordinate morphism with the descent morphism of f recovers f.

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap_comp_generatedCoordinateDesc_assoc (k : Type u) [CommRing k] [Algebra (ZMod 3) k] {B : CommHopfAlgCat k} (f : GeneralLinear.coordinateHopfAlgebra k 7 ⟶ B) (hf : (generatedDefiningIdeal k).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) {Z : CommHopfAlgCat k} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap k) (CategoryTheory.CategoryStruct.comp (generatedCoordinateDesc k f hf) h) = CategoryTheory.CategoryStruct.comp f h

Composing the quotient coordinate morphism with the descent morphism of f recovers f.

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateDesc_unique (k : Type u) [CommRing k] [Algebra (ZMod 3) k] {B : CommHopfAlgCat k} (f : GeneralLinear.coordinateHopfAlgebra k 7 ⟶ B) (hf : (generatedDefiningIdeal k).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) (g : generatedCoordinateHopfAlgebra k ⟶ B) (hg : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap k) g = f) : g = generatedCoordinateDesc k f hf

The descent morphism is the unique factorization of f through the generated subgroup.

noncomputable def TauCeti.G2ShortRoot.PrimeField.baseChangeGeneratorLift (k : Type u) [CommRing k] [Algebra (ZMod 3) k] (j : (Fin 2 ⊕ Fin 2) ⊕ Unit) : generatedCoordinateHopfAlgebra k ⟶ baseChangeGeneratorCodomain k j

A scalar-extended root-subgroup or weight-torus coordinate map, factored through the generated subgroup. This is CommHopfAlgCat.commonKernelLift, with its source identified with generatedCoordinateHopfAlgebra k.

Equations

• TauCeti.G2ShortRoot.PrimeField.baseChangeGeneratorLift k j = TauCeti.CommHopfAlgCat.commonKernelLift (TauCeti.G2ShortRoot.PrimeField.baseChangeGenerator k) j

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap_comp_baseChangeGeneratorLift (k : Type u) [CommRing k] [Algebra (ZMod 3) k] (j : (Fin 2 ⊕ Fin 2) ⊕ Unit) : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap k) (baseChangeGeneratorLift k j) = baseChangeGenerator k j

Each scalar-extended generator factors through the generated subgroup.

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.generatedCoordinateMap_comp_baseChangeGeneratorLift_assoc (k : Type u) [CommRing k] [Algebra (ZMod 3) k] (j : (Fin 2 ⊕ Fin 2) ⊕ Unit) {Z : CommHopfAlgCat k} (h : baseChangeGeneratorCodomain k j ⟶ Z) : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap k) (CategoryTheory.CategoryStruct.comp (baseChangeGeneratorLift k j) h) = CategoryTheory.CategoryStruct.comp (baseChangeGenerator k j) h

Each scalar-extended generator factors through the generated subgroup.

theorem TauCeti.G2ShortRoot.PrimeField.baseChangeGeneratorLift_unique (k : Type u) [CommRing k] [Algebra (ZMod 3) k] (j : (Fin 2 ⊕ Fin 2) ⊕ Unit) (g : generatedCoordinateHopfAlgebra k ⟶ baseChangeGeneratorCodomain k j) (hg : CategoryTheory.CategoryStruct.comp (generatedCoordinateMap k) g = baseChangeGenerator k j) : g = baseChangeGeneratorLift k j

The lift is the unique factorization of a scalar-extended generator through the generated subgroup.

instance TauCeti.G2ShortRoot.PrimeField.instFiniteTypeXGeneratedCoordinateHopfAlgebra (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : Algebra.FiniteType k ↑(generatedCoordinateHopfAlgebra k)

The generated coordinate Hopf algebra is a finite-type k-algebra: it is a quotient of O(GL₇/k).

@[reducible, inline]

noncomputable abbrev TauCeti.G2ShortRoot.PrimeField.finiteTypeGeneratedCoordinateHopfAlgebra (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : FiniteTypeCommHopfAlgCat k

The generated subgroup as a finite-type commutative Hopf algebra.

Equations

• TauCeti.G2ShortRoot.PrimeField.finiteTypeGeneratedCoordinateHopfAlgebra k = { obj := TauCeti.G2ShortRoot.PrimeField.generatedCoordinateHopfAlgebra k, property := ⋯ }

theorem TauCeti.G2ShortRoot.PrimeField.baseChangeDefiningIdeal_eq_generatedDefiningIdeal (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : baseChangeDefiningIdeal k = generatedDefiningIdeal k

The scalar extension of the short-root type-G₂ carrier is the subgroup generated after scalar extension, over every commutative 𝔽₃-algebra.

noncomputable def TauCeti.G2ShortRoot.PrimeField.coordinateHopfAlgebraGeneratedIso (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : CommHopfAlgCat.baseChange carrierAlgebra ≅ generatedCoordinateHopfAlgebra k

The coordinate Hopf algebra of the scalar-extended carrier is that of the subgroup generated after scalar extension.

Equations

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

@[simp]

theorem TauCeti.G2ShortRoot.PrimeField.baseChangeMap_carrierQuotient_comp_coordinateHopfAlgebraGeneratedIso_hom (k : Type u) [CommRing k] [Algebra (ZMod 3) k] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap carrierQuotient) (coordinateHopfAlgebraGeneratedIso k).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 3) k 7).hom (generatedCoordinateMap k)

The coordinate isomorphism identifies the scalar-extended carrier quotient map with the generated subgroup quotient map, through the ambient GL₇ coordinate isomorphism.