The ambient group of the Ree family of type G₂

The Ree family ²G₂(3^(2m+1)) is built inside the group of algebraic-closure-valued points of the short-root type-G₂ carrier over the prime field 𝔽₃. That carrier is the closed subgroup scheme of GL₇ generated over 𝔽₃ by the reductions of the numbered simple root subgroups and the weight torus of the Kostant toral closure of the seven-dimensional module V(ϖ₁). This file attaches it to a validated Ree index, together with its numbered positive simple root subgroups and the two Frobenius endomorphisms used in the fixed-point construction.

The carrier is taken over 𝔽₃, rather than obtained by base change from its integral toral closure, because the characteristic-three exceptional isogeny is constructed on the prime-field carrier. The base change of the integral closure is only known to contain this carrier; no flatness statement identifying them is assumed here.

The two Frobenius maps

TauCeti.ReeG2LieIndex.frobenius is the q-power Frobenius, where q = 3 ^ (2m+1) is the field order of the index. The map TauCeti.ReeG2LieIndex.primeFrobenius is the 3-power Frobenius, and the former is the (2m+1)-st power of the latter.

Neither is the family's Steinberg endomorphism. That endomorphism is the odd power τ ^ (2m+1) of the exceptional isogeny τ, which exchanges the two root lengths and squares to the prime-field Frobenius. Thus the prime-field Frobenius is the map τ squares to, and the q-power Frobenius is the map the Steinberg endomorphism squares to.

The numbering is the Bourbaki numbering of the G₂ diagram carried by the index. No renumbering adapter is needed: every numbered object below is indexed by Fin d.1.rank, identified with the carrier's Fin 2 by TauCeti.ReeG2LieIndex.rank_eq_two.

The carrier is not identified with the pinned simply connected group scheme of type G₂. Constructions on it transfer to that pinned group only along such an identification, once one is proved. Nothing here asserts that the carrier is reductive, that its weight torus is maximal, or that any group below is finite, perfect, or simple.

Main definitions

• TauCeti.ReeG2LieIndex.AmbientGroup: the algebraic-closure-valued points of the carrier.
• TauCeti.ReeG2LieIndex.simpleRootSubgroup: its positive simple-root subgroup at a Bourbaki-numbered node.
• TauCeti.ReeG2LieIndex.frobenius and TauCeti.ReeG2LieIndex.primeFrobenius: the q-power and 3-power Frobenius endomorphisms of the ambient group.

Main results

• TauCeti.ReeG2LieIndex.frobenius_simpleRootSubgroup and TauCeti.ReeG2LieIndex.primeFrobenius_simpleRootSubgroup give the two Frobenius actions on the numbered root subgroups.
• TauCeti.ReeG2LieIndex.rootGeneratorWeight_eq_root_simpleIndex certifies that the carrier and index use the same Bourbaki numbering of the simple roots.
• TauCeti.ReeG2LieIndex.weightTorusPoints_conj_simpleRootSubgroup states the corresponding torus-conjugation equation on the index's numbered root subgroups.
• TauCeti.ReeG2LieIndex.frobenius_eq_primeFrobenius_pow identifies the q-power Frobenius as the recorded iterate of the prime-field one.
• TauCeti.ReeG2LieIndex.mem_fixedSubgroup_frobenius_iff characterizes the q-rational points by their matrix entries.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 14.
• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX, for the numbering of G₂.

The ambient group and its simple root subgroups

@[reducible, inline]

abbrev TauCeti.ReeG2LieIndex.AmbientGroup (d : ReeG2LieIndex) : Type

The ambient group attached to a validated Ree index of type G₂: the points, over the algebraic closure of the prime field, of the short-root type-G₂ carrier over 𝔽₃. It is a subgroup of GL₇ over that closure.

The carrier is independent of the parameter m; that parameter enters through the endomorphism whose fixed points are taken. No finiteness or simplicity assertion is part of this definition.

Equations

• d.AmbientGroup = ↥(TauCeti.G2ShortRoot.PrimeField.points (↑d).Closure)

noncomputable def TauCeti.ReeG2LieIndex.simpleRootSubgroup (d : ReeG2LieIndex) (i : Fin (↑d).rank) : Multiplicative (↑d).Closure →* d.AmbientGroup

The positive simple-root subgroup at the Bourbaki-numbered node i of the G₂ diagram.

Equations

• d.simpleRootSubgroup i = TauCeti.G2ShortRoot.PrimeField.rootSubgroupPoints (Sum.inl ((finCongr ⋯) i)) (↑d).Closure

theorem TauCeti.ReeG2LieIndex.simpleRootSubgroup_def (d : ReeG2LieIndex) (i : Fin (↑d).rank) : d.simpleRootSubgroup i = G2ShortRoot.PrimeField.rootSubgroupPoints (Sum.inl ((finCongr ⋯) i)) (↑d).Closure

The simple-root subgroup is the carrier's numbered raising subgroup at the corresponding node. This is the unfolding equation for the sealed definition.

It is deliberately not a simp lemma: the Frobenius action lemmas below are the normal forms for the public API.

theorem TauCeti.ReeG2LieIndex.rootGeneratorWeight_eq_root_simpleIndex (d : ReeG2LieIndex) (i : Fin (↑d).rank) : DynkinType.G2.rootGeneratorWeight DynkinType.valid_G2 (Sum.inl ((finCongr ⋯) i)) = (DynkinType.G2.simplyConnectedRootDatum DynkinType.valid_G2).root (DynkinType.G2.simpleIndex DynkinType.valid_G2 ((finCongr ⋯) i))

The simple-root subgroups sit at the simple roots of the G₂ root datum. The character by which the carrier's split weight torus rescales the parameter of simpleRootSubgroup i is the i-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum at G₂, in the same Bourbaki numbering. This is the sense in which the carrier serves the diagram the index names; it is not a claim that the carrier is the pinned group of that diagram, no pinning being constructed for it.

@[simp]

theorem TauCeti.ReeG2LieIndex.weightTorusPoints_conj_simpleRootSubgroup (d : ReeG2LieIndex) (i : Fin (↑d).rank) (s : Fin 2 → (↑d).Closureˣ) (u : Multiplicative (↑d).Closure) : (G2ShortRoot.PrimeField.weightTorusPoints (↑d).Closure) s * (d.simpleRootSubgroup i) u * ((G2ShortRoot.PrimeField.weightTorusPoints (↑d).Closure) s)⁻¹ = (d.simpleRootSubgroup i) (Multiplicative.ofAdd (↑(torusCharacter s ((DynkinType.G2.simplyConnectedRootDatum DynkinType.valid_G2).root (DynkinType.G2.simpleIndex DynkinType.valid_G2 ((finCongr ⋯) i)))) * Multiplicative.toAdd u))

The simple-root subgroups sit at the simple roots of the G₂ root datum. A point of the carrier's rank-two split weight torus conjugates the subgroup at node i to itself, rescaling its parameter by the value of the corresponding root of TauCeti.DynkinType.G2.simplyConnectedRootDatum.

The Frobenius endomorphisms

noncomputable def TauCeti.ReeG2LieIndex.frobenius (d : ReeG2LieIndex) : d.AmbientGroup →* d.AmbientGroup

The q-power Frobenius endomorphism of the ambient group, where q = 3 ^ d.1.fieldExponent is the field order of the Ree index.

This is not the Steinberg endomorphism; it is the map that the odd power of the exceptional isogeny squares to.

Equations

• d.frobenius = TauCeti.G2ShortRoot.PrimeField.frobenius (↑d).fieldExponent (↑d).Closure

theorem TauCeti.ReeG2LieIndex.frobenius_def (d : ReeG2LieIndex) : d.frobenius = G2ShortRoot.PrimeField.frobenius (↑d).fieldExponent (↑d).Closure

The Frobenius of a Ree index is the carrier's Frobenius at the exponent recorded by the index. This is the unfolding equation for the sealed definition.

@[simp]

theorem TauCeti.ReeG2LieIndex.coe_frobenius_apply (d : ReeG2LieIndex) (g : d.AmbientGroup) (r c : Fin 7) : ↑↑(d.frobenius g) r c = ↑↑g r c ^ (↑d).fieldOrder

The Frobenius acts on the ambient group by raising every matrix entry to the q-th power.

@[simp]

theorem TauCeti.ReeG2LieIndex.frobenius_simpleRootSubgroup (d : ReeG2LieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.frobenius ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup i) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ (↑d).fieldOrder))

The Frobenius preserves each numbered simple-root subgroup and raises its parameter to the q-th power: Frob_q (x_i(u)) = x_i(u ^ q).

theorem TauCeti.ReeG2LieIndex.mem_fixedSubgroup_frobenius_iff (d : ReeG2LieIndex) (g : d.AmbientGroup) : g ∈ fixedSubgroup d.frobenius ↔ ∀ (r c : Fin 7), ↑↑g r c ∈ (↑d).fixedField

A point is fixed by the q-power Frobenius exactly when all of its matrix entries lie in the field of definition. Writing 𝔽_q for TauCeti.ValidLieTypeIndex.fixedField, these are the points of the carrier whose entries lie in 𝔽_q.

This is not a simp lemma because membership in TauCeti.fixedSubgroup simplifies first to an equality with the Frobenius image.

noncomputable def TauCeti.ReeG2LieIndex.primeFrobenius (d : ReeG2LieIndex) : d.AmbientGroup →* d.AmbientGroup

The prime-field Frobenius endomorphism of the ambient group, cubing each matrix entry. It is the map the exceptional isogeny squares to.

Equations

• d.primeFrobenius = TauCeti.G2ShortRoot.PrimeField.frobenius 1 (↑d).Closure

theorem TauCeti.ReeG2LieIndex.primeFrobenius_def (d : ReeG2LieIndex) : d.primeFrobenius = G2ShortRoot.PrimeField.frobenius 1 (↑d).Closure

The prime-field Frobenius is the carrier's first Frobenius iterate. This is the unfolding equation for the sealed definition.

@[simp]

theorem TauCeti.ReeG2LieIndex.coe_primeFrobenius_apply (d : ReeG2LieIndex) (g : d.AmbientGroup) (r c : Fin 7) : ↑↑(d.primeFrobenius g) r c = ↑↑g r c ^ 3

The prime-field Frobenius acts by cubing every matrix entry.

@[simp]

theorem TauCeti.ReeG2LieIndex.primeFrobenius_simpleRootSubgroup (d : ReeG2LieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.primeFrobenius ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup i) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ 3))

The prime-field Frobenius preserves each numbered simple-root subgroup and cubes its parameter: Frob_3 (x_i(u)) = x_i(u ^ 3).

theorem TauCeti.ReeG2LieIndex.frobenius_eq_primeFrobenius_pow (d : ReeG2LieIndex) : d.frobenius = (have this := d.primeFrobenius; this) ^ (↑d).fieldExponent

The q-power Frobenius is the recorded power of the prime-field Frobenius. This is the relation against which the square of the odd-power Steinberg endomorphism is measured. The type annotation selects the composition monoid structure on endomorphisms used by the power.