Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.ReeG2.Index

The index of the Ree family of type G₂ #

TauCeti.LieTypeIndex names the Ree family of type G₂ by its constructor reeG2 m, whose field order is 3 ^ (2m+1). This file selects that constructor and validates it, giving the restricted index domain TauCeti.ReeG2LieIndex on which the family's carrier, Steinberg endomorphism and candidate group are built, together with the numerical facts a consumer of that domain needs: its diagram is G₂, its rank is two, and its characteristic is three.

The selector is a constructor test, not a mathematical property of a group. Nothing here asserts that a named group is finite or simple.

Main definitions #

Main results #

References #

The family name, its parameter convention and the exclusion of ²G₂(3) follow Gorenstein--Lyons--Solomon, The Classification of the Finite Simple Groups, Number 1, §2.2, and Conway et al., Atlas of Finite Groups. The diagram numbering is the Bourbaki one of TauCeti.DynkinType.

source
def TauCeti.LieTypeIndex.IsReeG2 (d : LieTypeIndex) :
Prop

Whether a Lie-type index names the Ree family of type G₂, ²G₂(3^(2m+1)).

This is a constructor selector, not a mathematical property of a group. The exclusion of ²G₂(3) comes from the enclosing TauCeti.ValidLieTypeIndex; no finiteness or simplicity is asserted here.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.LieTypeIndex.isReeG2_iff_exists (d : LieTypeIndex) :
    d.IsReeG2 ↔ ∃ (m : ℕ), d = reeG2 m

    The selector names the Ree type-G₂ constructor: an index satisfies it exactly when it is reeG2 m for a parameter m, which is the form a consumer holding an abstract index needs.

    source
    @[instance_reducible]
    instance TauCeti.LieTypeIndex.instDecidablePredIsReeG2 :
    DecidablePred IsReeG2
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem TauCeti.LieTypeIndex.usesHalfFrobenius_of_isReeG2 {d : LieTypeIndex} (h : d.IsReeG2) :
    d.UsesHalfFrobenius

    The Ree family of type G₂ uses a half-Frobenius, so it carries no diagram automorphism.

    source
    @[reducible, inline]
    abbrev TauCeti.ReeG2LieIndex :
    Type

    A validated index in the Ree family of type G₂, ²G₂(3^(2m+1)).

    The outer subtype is important: ²G₂(3), the parameter m = 0, is excluded from the classification list; its derived subgroup has index three and is isomorphic to a group already named in another family, so the derived-subgroup recipe does not produce a new simple group there, and ²G₂(3) is not a ReeG2LieIndex. The Suzuki--Ree relatives ²B₂, ²F₄ and the Tits group are excluded too; they are the other three constructors of TauCeti.SuzukiReeIndex.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev TauCeti.ReeG2LieIndex.of (m : ℕ) (hvalid : (LieTypeIndex.reeG2 m).Valid) :
      ReeG2LieIndex

      Introduce a valid Ree index of type G₂, ²G₂(3^(2m+1)). Validity forces 1 ≤ m.

      Equations
      Instances For
        source
        theorem TauCeti.ReeG2LieIndex.exists_eq_of (d : ReeG2LieIndex) :
        ∃ (m : ℕ) (hvalid : (LieTypeIndex.reeG2 m).Valid), d = of m hvalid

        Every Ree index of type G₂ is of the introduction form. This is the eliminator matching of, so a consumer never repeats the case split over the other constructors.

        source
        @[simp]
        theorem TauCeti.ReeG2LieIndex.dynkinType_eq (d : ReeG2LieIndex) :
        (↑d).dynkinType = DynkinType.G2

        The Ree family of type G₂ is built on the rank-two diagram G₂.

        source
        @[simp]
        theorem TauCeti.ReeG2LieIndex.rank_eq_two (d : ReeG2LieIndex) :
        (↑d).rank = 2

        The Ree family of type G₂ has rank two, that being the rank of G₂.

        source
        @[simp]
        theorem TauCeti.ReeG2LieIndex.characteristic_eq_three (d : ReeG2LieIndex) :
        (↑d).characteristic = 3

        The Ree family of type G₂ lives in characteristic three.

        source
        theorem TauCeti.ReeG2LieIndex.fieldOrder_eq_three_pow (d : ReeG2LieIndex) :
        (↑d).fieldOrder = 3 ^ (↑d).fieldExponent

        The field order of a Ree index of type G₂ is the recorded power of three. This is the characteristic-three reading of TauCeti.ValidLieTypeIndex.fieldOrder_eq_characteristic_pow. It is the form a construction on a carrier defined over 𝔽₃ needs.

        source
        @[reducible, inline]
        abbrev TauCeti.ReeG2LieIndex.toSuzukiReeIndex (d : ReeG2LieIndex) :
        SuzukiReeIndex

        A Ree index of type G₂ is a Suzuki--Ree index: its Steinberg map is an odd power of a half-Frobenius.

        Equations
        Instances For