Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Assembly.HalfFrobenius

The half-Frobenius of every Suzuki--Ree index #

Each of the four half-Frobenius families carries an exceptional isogeny τ of its ambient group: the special isogeny of the rank-two symplectic carrier for the Suzuki groups, of the short-root G₂ carrier over 𝔽₃ for the Ree groups of type G₂, and of the short-root F₄ carrier over 𝔽₂ for the Ree groups of type F₄ and the Tits group. This file selects that isogeny for an arbitrary TauCeti.SuzukiReeIndex, as an endomorphism of the uniform ambient group TauCeti.ValidLieTypeIndex.AmbientGroup, and states its defining equations once for all four families:

τ (x_i(t)) = x_{σ i}(t ^ e_i),      τ ∘ τ = Frob_p,      steinberg = τ ^ (2m + 1),

where σ is TauCeti.SuzukiReeIndex.lengthPerm, e_i is TauCeti.SuzukiReeIndex.exponent (1 on a long simple root and p on a short one), Frob_p is the prime-field Frobenius TauCeti.ValidLieTypeIndex.primeFrobenius, and 2m + 1 is the field exponent the index records. The first equation is what identifies the selected isogeny: the opposite assignment of exponents would also square to Frob_p. The last says that the uniform Steinberg endomorphism TauCeti.ValidLieTypeIndex.steinberg of a half-Frobenius family is the odd power of this map, and not τ ∘ Frob_q.

As with the ambient group, nothing here identifies τ with the special isogeny of a pinned simply connected group scheme; that comparison transfers along an identification of the carriers.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.SuzukiReeIndex.halfFrobenius (e : SuzukiReeIndex) :
(↑e).AmbientGroup →* (↑e).AmbientGroup

The half-Frobenius of a Suzuki--Ree index: the exceptional isogeny of the carrier of its family, as an endomorphism of the uniform ambient group. On each of the four families it is the family's special isogeny, by halfFrobenius_suzuki and its siblings; its action on the simple root subgroups is halfFrobenius_simpleRootSubgroup, and its square is the prime-field Frobenius by halfFrobenius_halfFrobenius.

Instances For

    The branch equations #

    source
    theorem TauCeti.SuzukiReeIndex.halfFrobenius_suzuki {m : ℕ} (hv : (LieTypeIndex.suzuki m).Valid) :
    halfFrobenius ⟨⟨LieTypeIndex.suzuki m, hv⟩, ⋯⟩ = SuzukiLieIndex.halfFrobenius ⟨⟨LieTypeIndex.suzuki m, hv⟩, ⋯⟩

    On ²B₂(2^(2m+1)) the half-Frobenius is that of the Suzuki family, the special isogeny of the rank-two symplectic carrier.

    source
    theorem TauCeti.SuzukiReeIndex.halfFrobenius_reeG2 {m : ℕ} (hv : (LieTypeIndex.reeG2 m).Valid) :
    halfFrobenius ⟨⟨LieTypeIndex.reeG2 m, hv⟩, ⋯⟩ = (ReeG2LieIndex.of m hv).halfFrobenius

    On ²G₂(3^(2m+1)) the half-Frobenius is that of the Ree G₂ family.

    source
    theorem TauCeti.SuzukiReeIndex.halfFrobenius_reeF4 {m : ℕ} (hv : (LieTypeIndex.reeF4 m).Valid) :
    halfFrobenius ⟨⟨LieTypeIndex.reeF4 m, hv⟩, ⋯⟩ = (ReeF4LieIndex.of m hv).halfFrobenius

    On ²F₄(2^(2m+1)) the half-Frobenius is that of the Ree F₄ family.

    source
    theorem TauCeti.SuzukiReeIndex.halfFrobenius_tits (hv : LieTypeIndex.tits.Valid) :
    halfFrobenius ⟨⟨LieTypeIndex.tits, hv⟩, ⋯⟩ = TitsLieIndex.of.steinberg

    On the Tits index the half-Frobenius is the Tits Steinberg endomorphism, which is the special isogeny of the short-root F₄ carrier over 𝔽₂ by TauCeti.TitsLieIndex.steinberg_def: the Tits index records field exponent one, so its Steinberg endomorphism is the half-Frobenius itself.

    The defining equations #

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.halfFrobenius_simpleRootSubgroup (e : SuzukiReeIndex) (i : Fin (↑e).rank) (u : Multiplicative (↑e).Closure) :
    e.halfFrobenius (((↑e).simpleRootSubgroup i) u) = ((↑e).simpleRootSubgroup (e.lengthPerm i)) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ e.exponent i))

    The half-Frobenius has the pinned action on every simple root subgroup. It sends x_i(u) to x_{σ i}(u ^ e_i), for σ the length permutation of the index and e_i its exponent, 1 on a long simple root and the defining characteristic on a short one.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.halfFrobenius_halfFrobenius (e : SuzukiReeIndex) (g : (↑e).AmbientGroup) :
    e.halfFrobenius (e.halfFrobenius g) = (↑e).primeFrobenius g

    The square of the half-Frobenius is the prime-field Frobenius, τ (τ g) = Frob_p g for p the defining characteristic of the index.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.halfFrobenius_sq (e : SuzukiReeIndex) :
    e.halfFrobenius ^ 2 = (↑e).primeFrobenius

    The square relation τ ^ 2 = Frob_p as an equation in the endomorphism monoid.

    source
    theorem TauCeti.SuzukiReeIndex.steinberg_eq_halfFrobenius_pow (e : SuzukiReeIndex) :
    (↑e).steinberg = e.halfFrobenius ^ (↑e).fieldExponent

    The Steinberg endomorphism of a Suzuki--Ree index is the odd power τ ^ (2m + 1) of its half-Frobenius, for 2m + 1 the field exponent the index records.