Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Tits.Index

The index of the Tits group #

TauCeti.LieTypeIndex.tits is the separate classification-list entry for the Tits group ²F₄(2)'. It uses the same type-F₄ diagram and characteristic-two exceptional isogeny as the Ree family ²F₄(2^(2m+1)), but its Steinberg endomorphism is the exceptional isogeny itself: the field order is two and the field exponent is one.

This file gives that constructor its own validated index type. The distinction from the reeF4 constructor is mathematical rather than cosmetic: ²F₄(2) is not simple, while its derived subgroup is the Tits group named by this index. A construction receiving a TauCeti.TitsLieIndex therefore cannot accidentally receive a positive-parameter Ree-family index, even though the two branches use the same ambient carrier and special isogeny.

The exceptional isogeny raises the parameters of the two long simple root subgroups to the first power and those of the two short simple root subgroups to the second. The theorem TauCeti.TitsLieIndex.exponent_eq derives this numbered formula from the root-length predicate on TauCeti.DynkinType.F4, rather than recording a second root-length table.

Nothing here constructs a group or asserts finiteness or simplicity.

Main definitions #

Main results #

References #

The separate Tits entry and the ²F₄ parameter convention follow D. Gorenstein, R. Lyons and R. Solomon, The Classification of the Finite Simple Groups, Number 1, §2.2, and J. H. Conway et al., Atlas of Finite Groups. The diagram numbering is Bourbaki's.

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

Whether a Lie-type index is the separate Tits constructor.

This is a constructor selector, not a mathematical property of a group. In particular, it is false on every member of the Ree family of type F₄, including at the level of raw parameters.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.LieTypeIndex.isTits_iff (d : LieTypeIndex) :
    d.IsTits ↔ d = tits

    The Tits selector holds exactly at the Tits constructor.

    source
    @[instance_reducible]
    instance TauCeti.LieTypeIndex.instDecidablePredIsTits :
    DecidablePred IsTits
    Equations
    source
    theorem TauCeti.LieTypeIndex.usesHalfFrobenius_of_isTits {d : LieTypeIndex} (h : d.IsTits) :
    d.UsesHalfFrobenius

    The Tits index uses a half-Frobenius, so it carries no diagram automorphism.

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

    The validated index of the Tits group ²F₄(2)'.

    This is a subtype of TauCeti.ValidLieTypeIndex, as required of every index passed to a carrier-valued construction. Its constructor selector excludes the uniform Ree family of type F₄, whose members use the same diagram and exceptional isogeny.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev TauCeti.TitsLieIndex.of :
      TitsLieIndex

      Introduce the Tits index.

      Equations
      Instances For
        source
        theorem TauCeti.TitsLieIndex.eq_of (d : TitsLieIndex) :
        d = of

        Every Tits index is the canonical introduction form.

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

        The Tits construction uses the rank-four diagram F₄.

        source
        @[simp]
        theorem TauCeti.TitsLieIndex.rank_eq_four (d : TitsLieIndex) :
        (↑d).rank = 4

        The Tits construction has rank four, that being the rank of F₄.

        source
        @[simp]
        theorem TauCeti.TitsLieIndex.characteristic_eq_two (d : TitsLieIndex) :
        (↑d).characteristic = 2

        The Tits construction lives in characteristic two.

        source
        @[simp]
        theorem TauCeti.TitsLieIndex.fieldOrder_eq_two (d : TitsLieIndex) :
        (↑d).fieldOrder = 2

        The field order attached to the Tits index is two.

        source
        @[simp]
        theorem TauCeti.TitsLieIndex.fieldExponent_eq_one (d : TitsLieIndex) :
        (↑d).fieldExponent = 1

        The field exponent attached to the Tits index is one, so its Steinberg map is the half-Frobenius itself.

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

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

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.TitsLieIndex.exponent_eq (d : TitsLieIndex) (i : Fin (↑d).rank) :
          d.toSuzukiReeIndex.exponent i = if ↑i < 2 then 1 else 2

          The exponents of the exceptional isogeny on the four numbered simple root subgroups: the first power at the two long simple roots, Bourbaki nodes 1 and 2, and the second power at the two short ones. This is the F₄ specialization of TauCeti.SuzukiReeIndex.exponent_of_isLongSimpleRoot.