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

The short-root type-F₄ carrier over 𝔽₂ is generated by eight numbered root subgroups and its rank-four weight torus. After extending their coordinate maps to a commutative 𝔽₂-algebra k, their common kernel defines a closed subgroup of GL₂₆ over k. Because generation commutes with scalar extension along free algebras, this generated subgroup is the scalar extension of the prime-field carrier. Recognizing the carrier as the pinned simply connected group scheme of type F₄ is a separate question.

Main declarations

In the namespace TauCeti.F4ShortRoot.PrimeField:

• generatedDefiningIdeal and generatedCoordinateHopfAlgebra: the common kernel of the scalar-extended generator coordinate maps, and the resulting quotient of O(GL₂₆/k).
• baseChangeDefiningIdeal_eq_generatedDefiningIdeal: the scalar extension of the prime-field carrier's defining ideal is the generated defining ideal.
• coordinateHopfAlgebraGeneratedIso: the resulting isomorphism between the coordinate Hopf algebra of the scalar-extended carrier and that of the generated subgroup, characterized by baseChangeMap_mkQuotient_comp_coordinateHopfAlgebraGeneratedIso_hom.

References

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

The construction follows the type-G₂ short-root carrier construction in TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Generated.Basic.

@[reducible, inline]

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

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

Equations

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

noncomputable def TauCeti.F4ShortRoot.PrimeField.baseChangeGenerator (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra k 26 ⟶ 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.F4ShortRoot.PrimeField.baseChangeGenerator_def (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) : baseChangeGenerator k j = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 2) k 26).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₂₆.

theorem TauCeti.F4ShortRoot.PrimeField.baseChangeGenerator_apply (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) (x : ↑(GeneralLinear.coordinateHopfAlgebra k 26)) : (↑(CommHopfAlgCat.Hom.hom (baseChangeGenerator k j))).toRingHom x = (↑(CommHopfAlgCat.Hom.hom (CommHopfAlgCat.baseChangeMap (generator j)))).toRingHom ((CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 2) k 26).inv) x)

Evaluation of a scalar-extended generator factors through the coordinate-algebra identification and the base-changed prime-field generator.

noncomputable def TauCeti.F4ShortRoot.PrimeField.generatedDefiningIdeal (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k 26)

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

Equations

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

@[simp]

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

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

noncomputable def TauCeti.F4ShortRoot.PrimeField.generatedCoordinateHopfAlgebra (k : Type u) [CommRing k] [Algebra (ZMod 2) 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.F4ShortRoot.PrimeField.generatedCoordinateHopfAlgebra_def (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : generatedCoordinateHopfAlgebra k = CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra k 26) (generatedDefiningIdeal k)

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

theorem TauCeti.F4ShortRoot.PrimeField.le_generatedDefiningIdeal_iff (k : Type u) [CommRing k] [Algebra (ZMod 2) k] (J : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k 26)) : J ≤ generatedDefiningIdeal k ↔ ∀ (j : (Fin 4 ⊕ Fin 4) ⊕ 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.F4ShortRoot.PrimeField.baseChangeDefiningIdeal (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : HopfIdeal k ↑(GeneralLinear.coordinateHopfAlgebra k 26)

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.F4ShortRoot.PrimeField.baseChangeDefiningIdeal_def (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : baseChangeDefiningIdeal k = (CommHopfAlgCat.baseChangeHopfIdeal definingIdeal).comapOfSurjective (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 2) k 26).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₂₆.

@[simp]

theorem TauCeti.F4ShortRoot.PrimeField.mem_baseChangeDefiningIdeal_iff (k : Type u) [CommRing k] [Algebra (ZMod 2) k] {x : ↑(GeneralLinear.coordinateHopfAlgebra k 26)} : x ∈ baseChangeDefiningIdeal k ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 2) k 26).inv) x ∈ CommHopfAlgCat.baseChangeHopfIdeal definingIdeal

Membership in the transported defining ideal is membership of the corresponding element in the scalar extension of the prime-field defining ideal.

theorem TauCeti.F4ShortRoot.PrimeField.baseChangeDefiningIdeal_le_generatedDefiningIdeal (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : baseChangeDefiningIdeal k ≤ generatedDefiningIdeal k

The scalar extension of the prime-field carrier contains the subgroup generated by the scalar-extended root subgroups and torus.

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

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

noncomputable def TauCeti.F4ShortRoot.PrimeField.coordinateHopfAlgebraGeneratedIso (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : coordinateHopfAlgebra k ≅ 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.F4ShortRoot.PrimeField.baseChangeMap_mkQuotient_comp_coordinateHopfAlgebraGeneratedIso_hom (k : Type u) [CommRing k] [Algebra (ZMod 2) k] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) definingIdeal)) (coordinateHopfAlgebraGeneratedIso k).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso (ZMod 2) k 26).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra k 26) (generatedDefiningIdeal k)) (CategoryTheory.eqToHom ⋯))

The generated-carrier isomorphism identifies the carrier coordinate morphism with the quotient morphism by the generated defining ideal.