Indices for the classification of finite simple groups

This file defines the parameters and indexing types for the eventual statement of the classification of finite simple groups. The Lie-type index records the family, rank, and finite field parameter as data. Its validity predicate first imposes the conventional rank and small-field ranges and then removes the six remaining duplicate representatives. A Lie-type index also determines its underlying untwisted Dynkin diagram, characteristic, and Frobenius parameter.

The twenty-six sporadic names and the four-way TauCeti.CFSGIndex complete the indexing layer. No definition here asserts that a named group is finite or simple; the groups themselves are built from these indices elsewhere, the Lie-type entries as TauCeti.ValidLieTypeIndex.Group.

The twisted families use the Gorenstein--Lyons--Solomon and ATLAS small-field convention. Thus twistedA 2 q denotes ²A₂(q), with a matrix realization over the field of q² elements, while q itself is the Frobenius parameter. The Suzuki--Ree families instead record m in the field order p ^ (2 * m + 1).

Main definitions

• TauCeti.PrimePower: a prime and positive exponent, retaining the data needed for a finite field.
• TauCeti.LieTypeIndex and TauCeti.LieTypeIndex.Valid: the Lie families and their preferred parameter range.
• TauCeti.ValidLieTypeIndex, TauCeti.SuzukiReeIndex, TauCeti.GraphTwistedIndex, TauCeti.TypeALieIndex, TauCeti.TypeCLieIndex, TauCeti.TypeE6LieIndex, TauCeti.TypeTwistedE6LieIndex, TauCeti.SuzukiLieIndex, TauCeti.TypeDDiagramLieIndex, TauCeti.TypeDLieIndex, TauCeti.TypeTwistedDLieIndex, TauCeti.TypeTrialityD4LieIndex, TauCeti.RankTwoBLieIndex, TauCeti.TypeB2LieIndex, and TauCeti.UnimodularLieIndex: the restricted domains consumed by later carrier and endomorphism constructions.
• TauCeti.SporadicName: the conventional twenty-six sporadic names.
• TauCeti.CFSGIndex: cyclic, alternating, Lie-type, and sporadic entries in the classification list.

References

The family names and parameter conventions, including the small isomorphism exclusions, follow Gorenstein--Lyons--Solomon, The Classification of the Finite Simple Groups, and Conway et al., Atlas of Finite Groups. The underlying diagrams are the Bourbaki-numbered TauCeti.DynkinType.

For the two families on the rank-two diagram B₂, the names B₂(q) and ²B₂(2^(2m+1)), the retention of the rank-two symplectic family under the B name, and the isomorphisms that exclude B₂(2), B₂(3) and ²B₂(2) are those of Gorenstein--Lyons--Solomon, Number 1, §2.2, and of the Atlas; the diagram itself is N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate II at rank two.

Prime powers and Lie-type families

structure TauCeti.PrimePower : Type

A prime power p ^ exponent, retaining the prime and positive exponent needed to construct its finite field. Unlike the proposition IsPrimePow, this is parameter data rather than a property of an already specified cardinality.

• p : ℕ

  The prime base of the prime power.

• exponent : ℕ

  The positive exponent of the prime power.

• prime_p : Nat.Prime self.p
• exponent_pos : 0 < self.exponent

theorem TauCeti.PrimePower.ext {x y : PrimePower} (p : x.p = y.p) (exponent : x.exponent = y.exponent) : x = y

theorem TauCeti.PrimePower.ext_iff {x y : PrimePower} : x = y ↔ x.p = y.p ∧ x.exponent = y.exponent

def TauCeti.instDecidableEqPrimePower.decEq (x✝ x✝¹ : PrimePower) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.instDecidableEqPrimePower : DecidableEq PrimePower

Equations

• TauCeti.instDecidableEqPrimePower = TauCeti.instDecidableEqPrimePower.decEq

def TauCeti.PrimePower.card (q : PrimePower) : ℕ

The cardinality represented by a prime-power parameter.

Equations

• q.card = q.p ^ q.exponent

@[simp]

theorem TauCeti.PrimePower.card_def (q : PrimePower) : q.card = q.p ^ q.exponent

The stored cardinality is the stored base raised to the stored exponent.

theorem TauCeti.PrimePower.isPrimePow_card (q : PrimePower) : IsPrimePow q.card

The cardinality stored by a prime-power parameter is a prime power in Mathlib's sense.

inductive TauCeti.LieTypeIndex : Type

The families of finite groups of Lie type, with ranks given by Dynkin subscripts.

The ordinary and graph-twisted constructors use the small-field GLS/ATLAS parameter q. The three Suzuki--Ree constructors record the integer m in field order p ^ (2 * m + 1). The Tits group ²F₄(2)' is listed separately from the uniform Ree family.

• A (rank : ℕ) (q : PrimePower) : LieTypeIndex
• twistedA (rank : ℕ) (q : PrimePower) : LieTypeIndex
• B (rank : ℕ) (q : PrimePower) : LieTypeIndex
• C (rank : ℕ) (q : PrimePower) : LieTypeIndex
• D (rank : ℕ) (q : PrimePower) : LieTypeIndex
• twistedD (rank : ℕ) (q : PrimePower) : LieTypeIndex
• E6 (q : PrimePower) : LieTypeIndex
• E7 (q : PrimePower) : LieTypeIndex
• E8 (q : PrimePower) : LieTypeIndex
• F4 (q : PrimePower) : LieTypeIndex
• G2 (q : PrimePower) : LieTypeIndex
• twistedE6 (q : PrimePower) : LieTypeIndex
• trialityD4 (q : PrimePower) : LieTypeIndex
• suzuki (m : ℕ) : LieTypeIndex
• reeG2 (m : ℕ) : LieTypeIndex
• reeF4 (m : ℕ) : LieTypeIndex
• tits : LieTypeIndex

@[instance_reducible]

instance TauCeti.instDecidableEqLieTypeIndex : DecidableEq LieTypeIndex

Equations

• TauCeti.instDecidableEqLieTypeIndex = TauCeti.instDecidableEqLieTypeIndex.decEq

def TauCeti.instDecidableEqLieTypeIndex.decEq (x✝ x✝¹ : LieTypeIndex) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.LieTypeIndex.InStandardRange : LieTypeIndex → Prop

Conventional rank and small-field restrictions on the Lie-type families. These remove the nonsimple members and systematic low-rank or characteristic-two overlaps. This is indexing data; it does not assert finiteness or simplicity of a group.

The B family starts at rank two, while C starts at rank three and has odd characteristic. Thus B₂(q) = C₂(q) is always named B₂(q), and the characteristic-two coincidence Bₙ(q) = Cₙ(q) is also kept only in the B family.

Equations

• (TauCeti.LieTypeIndex.A rank q).InStandardRange = (1 ≤ rank ∧ (rank = 1 → 4 ≤ q.card))
• (TauCeti.LieTypeIndex.twistedA rank q).InStandardRange = (2 ≤ rank ∧ (rank = 2 → 3 ≤ q.card))
• (TauCeti.LieTypeIndex.B rank q).InStandardRange = (2 ≤ rank ∧ ¬(rank = 2 ∧ q.card = 2))
• (TauCeti.LieTypeIndex.C rank q).InStandardRange = (3 ≤ rank ∧ q.p ≠ 2)
• (TauCeti.LieTypeIndex.D rank q).InStandardRange = (4 ≤ rank)
• (TauCeti.LieTypeIndex.twistedD rank q).InStandardRange = (4 ≤ rank)
• (TauCeti.LieTypeIndex.G2 q).InStandardRange = (3 ≤ q.card)
• (TauCeti.LieTypeIndex.suzuki m).InStandardRange = (1 ≤ m)
• (TauCeti.LieTypeIndex.reeG2 m).InStandardRange = (1 ≤ m)
• (TauCeti.LieTypeIndex.reeF4 m).InStandardRange = (1 ≤ m)
• (TauCeti.LieTypeIndex.E6 q).InStandardRange = True
• (TauCeti.LieTypeIndex.E7 q).InStandardRange = True
• (TauCeti.LieTypeIndex.E8 q).InStandardRange = True
• (TauCeti.LieTypeIndex.F4 q).InStandardRange = True
• (TauCeti.LieTypeIndex.twistedE6 q).InStandardRange = True
• (TauCeti.LieTypeIndex.trialityD4 q).InStandardRange = True
• TauCeti.LieTypeIndex.tits.InStandardRange = True

@[simp]

theorem TauCeti.LieTypeIndex.inStandardRange_iff (d : LieTypeIndex) : d.InStandardRange ↔ match d with | A rank q => 1 ≤ rank ∧ (rank = 1 → 4 ≤ q.card) | twistedA rank q => 2 ≤ rank ∧ (rank = 2 → 3 ≤ q.card) | B rank q => 2 ≤ rank ∧ ¬(rank = 2 ∧ q.card = 2) | C rank q => 3 ≤ rank ∧ q.p ≠ 2 | D rank q => 4 ≤ rank | twistedD rank q => 4 ≤ rank | G2 q => 3 ≤ q.card | suzuki m => 1 ≤ m | reeG2 m => 1 ≤ m | reeF4 m => 1 ≤ m | E6 q => True | E7 q => True | E8 q => True | F4 q => True | twistedE6 q => True | trialityD4 q => True | tits => True

Characterization of the conventional range restrictions on every Lie-type constructor.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredInStandardRange : DecidablePred InStandardRange

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.LieTypeIndex.IsDuplicateRepresentative : LieTypeIndex → Prop

Representatives omitted in favor of the alternating or Lie-type name under which the classification list keeps the same group. After InStandardRange, these are the remaining small isomorphism coincidences.

Equations

• (TauCeti.LieTypeIndex.A rank q).IsDuplicateRepresentative = (rank = 1 ∧ (q.card = 4 ∨ q.card = 5 ∨ q.card = 9) ∨ rank = 2 ∧ q.card = 2 ∨ rank = 3 ∧ q.card = 2)
• (TauCeti.LieTypeIndex.B rank q).IsDuplicateRepresentative = (rank = 2 ∧ q.card = 3)
• x✝.IsDuplicateRepresentative = False

@[simp]

theorem TauCeti.LieTypeIndex.isDuplicateRepresentative_iff (d : LieTypeIndex) : d.IsDuplicateRepresentative ↔ match d with | A rank q => rank = 1 ∧ (q.card = 4 ∨ q.card = 5 ∨ q.card = 9) ∨ rank = 2 ∧ q.card = 2 ∨ rank = 3 ∧ q.card = 2 | B rank q => rank = 2 ∧ q.card = 3 | x => False

Characterization of the deliberately omitted duplicate representatives.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsDuplicateRepresentative : DecidablePred IsDuplicateRepresentative

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.LieTypeIndex.Valid (d : LieTypeIndex) : Prop

A preferred Lie-type representative in the CFSG list. This is not a finiteness or simplicity predicate.

Equations

• d.Valid = (d.InStandardRange ∧ ¬d.IsDuplicateRepresentative)

@[simp]

theorem TauCeti.LieTypeIndex.valid_iff (d : LieTypeIndex) : d.Valid ↔ d.InStandardRange ∧ ¬d.IsDuplicateRepresentative

A Lie-type index is valid exactly when it is in range and is the preferred representative.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredValid : DecidablePred Valid

Equations

• d.instDecidablePredValid = ⋯.mpr inferInstance

theorem TauCeti.LieTypeIndex.two_le_of_twistedA_inStandardRange {n : ℕ} {q : PrimePower} (h : (twistedA n q).InStandardRange) : 2 ≤ n

An in-range ²Aₙ(q) index has rank at least two: the reversal of a one-node diagram is trivial, and ²A₁(q) is not a name on the classification list.

theorem TauCeti.LieTypeIndex.four_le_of_twistedD_inStandardRange {n : ℕ} {q : PrimePower} (h : (twistedD n q).InStandardRange) : 4 ≤ n

An in-range ²Dₙ(q) index has rank at least four, the range in which the Dₙ diagram has its fork.

def TauCeti.LieTypeIndex.UsesHalfFrobenius : LieTypeIndex → Prop

Whether the Steinberg map for an index is an odd power of a half-Frobenius. This selects the three Suzuki--Ree families and the Tits group, not the exceptional Dynkin types in general.

Equations

• (TauCeti.LieTypeIndex.suzuki m).UsesHalfFrobenius = True
• (TauCeti.LieTypeIndex.reeG2 m).UsesHalfFrobenius = True
• (TauCeti.LieTypeIndex.reeF4 m).UsesHalfFrobenius = True
• TauCeti.LieTypeIndex.tits.UsesHalfFrobenius = True
• x✝.UsesHalfFrobenius = False

@[simp]

theorem TauCeti.LieTypeIndex.usesHalfFrobenius_iff (d : LieTypeIndex) : d.UsesHalfFrobenius ↔ match d with | suzuki m => True | reeG2 m => True | reeF4 m => True | tits => True | x => False

Characterization of the families whose Steinberg map uses a half-Frobenius.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredUsesHalfFrobenius : DecidablePred UsesHalfFrobenius

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.LieTypeIndex.IsTypeA : LieTypeIndex → Prop

Whether a Lie-type index belongs to one of the two type-A families, A_r(q) or ²A_r(q).

This is a constructor selector, not a mathematical property of a group. The small-field and duplicate-representative restrictions come from the enclosing TauCeti.ValidLieTypeIndex; no finiteness or simplicity is asserted here.

Equations

• (TauCeti.LieTypeIndex.A rank q).IsTypeA = True
• (TauCeti.LieTypeIndex.twistedA rank q).IsTypeA = True
• x✝.IsTypeA = False

@[simp]

theorem TauCeti.LieTypeIndex.isTypeA_iff (d : LieTypeIndex) : d.IsTypeA ↔ match d with | A rank q => True | twistedA rank q => True | x => False

Characterization of the two type-A constructors.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsTypeA : DecidablePred IsTypeA

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LieTypeIndex.not_usesHalfFrobenius_of_isTypeA {d : LieTypeIndex} (h : d.IsTypeA) : ¬d.UsesHalfFrobenius

Neither type-A family uses a half-Frobenius, so both carry a diagram automorphism.

@[reducible, inline]

abbrev TauCeti.LieTypeIndex.IsTypeC : LieTypeIndex → Prop

Whether a Lie-type index belongs to the untwisted family C_r(q).

This is a constructor selector, not a mathematical property of a group. The rank, field, and preferred-representative restrictions come from the enclosing TauCeti.ValidLieTypeIndex.

Equations

• (TauCeti.LieTypeIndex.C rank q).IsTypeC = True
• x✝.IsTypeC = False

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsTypeC : DecidablePred IsTypeC

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LieTypeIndex.not_usesHalfFrobenius_of_isTypeC {d : LieTypeIndex} (h : d.IsTypeC) : ¬d.UsesHalfFrobenius

The untwisted type-C family does not use a half-Frobenius.

def TauCeti.LieTypeIndex.IsTypeE6 : LieTypeIndex → Prop

Whether a Lie-type index names the untwisted exceptional family E₆(q).

This is a constructor selector, not a mathematical property of a group. It is false on the graph-twisted family ²E₆(q), which shares the E₆ diagram but takes a different Steinberg map, and it asserts no finiteness or simplicity.

Equations

• (TauCeti.LieTypeIndex.E6 q).IsTypeE6 = True
• x✝.IsTypeE6 = False

@[simp]

theorem TauCeti.LieTypeIndex.isTypeE6_iff (d : LieTypeIndex) : d.IsTypeE6 ↔ match d with | E6 q => True | x => False

Characterization of the untwisted type-E₆ constructor.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsTypeE6 : DecidablePred IsTypeE6

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LieTypeIndex.not_usesHalfFrobenius_of_isTypeE6 {d : LieTypeIndex} (h : d.IsTypeE6) : ¬d.UsesHalfFrobenius

The untwisted family E₆(q) does not use a half-Frobenius, so it carries a diagram automorphism.

theorem TauCeti.LieTypeIndex.valid_E6 (q : PrimePower) : (E6 q).Valid

Every E₆(q) index is valid. The E₆ row of InStandardRange is unrestricted, and no E₆ parameter is a duplicate representative, so the family contributes one classification entry for each prime power.

def TauCeti.LieTypeIndex.IsTypeTwistedE6 : LieTypeIndex → Prop

Whether a Lie-type index names the graph-twisted exceptional family ²E₆(q).

This is a constructor selector, not a mathematical property of a group. It is false on the untwisted family E₆(q), which shares the E₆ diagram but takes the plain Frobenius as its Steinberg map, and it asserts no finiteness or simplicity.

Equations

• (TauCeti.LieTypeIndex.twistedE6 q).IsTypeTwistedE6 = True
• x✝.IsTypeTwistedE6 = False

@[simp]

theorem TauCeti.LieTypeIndex.isTypeTwistedE6_iff (d : LieTypeIndex) : d.IsTypeTwistedE6 ↔ match d with | twistedE6 q => True | x => False

Characterization of the graph-twisted type-E₆ constructor.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsTypeTwistedE6 : DecidablePred IsTypeTwistedE6

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LieTypeIndex.not_usesHalfFrobenius_of_isTypeTwistedE6 {d : LieTypeIndex} (h : d.IsTypeTwistedE6) : ¬d.UsesHalfFrobenius

The family ²E₆(q) does not use a half-Frobenius: it twists the Frobenius by a diagram automorphism instead.

theorem TauCeti.LieTypeIndex.valid_twistedE6 (q : PrimePower) : (twistedE6 q).Valid

Every ²E₆(q) index is valid. The ²E₆ row of InStandardRange is unrestricted, and no ²E₆ parameter is a duplicate representative, so the family contributes one classification entry for each prime power.

def TauCeti.LieTypeIndex.IsSuzuki : LieTypeIndex → Prop

Whether a Lie-type index names the Suzuki family ²B₂(2^(2m+1)).

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

Equations

• (TauCeti.LieTypeIndex.suzuki m).IsSuzuki = True
• x✝.IsSuzuki = False

@[simp]

theorem TauCeti.LieTypeIndex.isSuzuki_iff (d : LieTypeIndex) : d.IsSuzuki ↔ match d with | suzuki m => True | x => False

Characterization of the Suzuki constructor.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsSuzuki : DecidablePred IsSuzuki

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LieTypeIndex.usesHalfFrobenius_of_isSuzuki {d : LieTypeIndex} (h : d.IsSuzuki) : d.UsesHalfFrobenius

The Suzuki family uses a half-Frobenius, so it carries no diagram automorphism.

def TauCeti.LieTypeIndex.IsTypeD : LieTypeIndex → Prop

Whether a Lie-type index names the untwisted family Dₙ(q).

This is a constructor selector, not a mathematical property of a group. It is false on the two twisted families ²Dₙ(q) and ³D₄(q), which share the Dₙ diagram but take different Steinberg maps, and it asserts no finiteness or simplicity.

Equations

• (TauCeti.LieTypeIndex.D rank q).IsTypeD = True
• x✝.IsTypeD = False

@[simp]

theorem TauCeti.LieTypeIndex.isTypeD_iff (d : LieTypeIndex) : d.IsTypeD ↔ match d with | D rank q => True | x => False

Characterization of the untwisted type-D constructor.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsTypeD : DecidablePred IsTypeD

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.LieTypeIndex.IsTypeTwistedD : LieTypeIndex → Prop

Whether a Lie-type index names the graph-twisted family ²Dₙ(q).

This is a constructor selector, not a mathematical property of a group. Following the Gorenstein--Lyons--Solomon convention recorded above, the parameter q is the small field, the matrix realization being over 𝔽_(q²).

Equations

• (TauCeti.LieTypeIndex.twistedD rank q).IsTypeTwistedD = True
• x✝.IsTypeTwistedD = False

@[simp]

theorem TauCeti.LieTypeIndex.isTypeTwistedD_iff (d : LieTypeIndex) : d.IsTypeTwistedD ↔ match d with | twistedD rank q => True | x => False

Characterization of the graph-twisted type-D constructor.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsTypeTwistedD : DecidablePred IsTypeTwistedD

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.LieTypeIndex.IsTypeTrialityD4 : LieTypeIndex → Prop

Whether a Lie-type index names the triality-twisted family ³D₄(q).

This is a constructor selector, not a mathematical property of a group. Its matrix realization is over 𝔽_(q³), q again being the small field parameter.

Equations

• (TauCeti.LieTypeIndex.trialityD4 q).IsTypeTrialityD4 = True
• x✝.IsTypeTrialityD4 = False

@[simp]

theorem TauCeti.LieTypeIndex.isTypeTrialityD4_iff (d : LieTypeIndex) : d.IsTypeTrialityD4 ↔ match d with | trialityD4 q => True | x => False

Characterization of the triality-twisted constructor.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredIsTypeTrialityD4 : DecidablePred IsTypeTrialityD4

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LieTypeIndex.valid_trialityD4 (q : PrimePower) : (trialityD4 q).Valid

Every ³D₄(q) index is valid. The triality row of InStandardRange is unrestricted, and no triality parameter is a duplicate representative, so the family contributes one classification entry for each prime power.

def TauCeti.LieTypeIndex.dynkinType : LieTypeIndex → DynkinType

The underlying untwisted Dynkin diagram. Twisted types map to the diagram from which they are constructed, so all later root indices use the Bourbaki numbering of TauCeti.DynkinType.

This is exposed because it appears in the types of the numbered data attached to an index: for TauCeti.GraphTwistedIndex.diagramPerm on the ²Aₙ branch to be TauCeti.graphPermA n, the type Fin (twistedA n q).dynkinType.rank has to reduce to Fin n.

Equations

• (TauCeti.LieTypeIndex.A n q).dynkinType = TauCeti.DynkinType.A n
• (TauCeti.LieTypeIndex.twistedA n q).dynkinType = TauCeti.DynkinType.A n
• (TauCeti.LieTypeIndex.B n q).dynkinType = TauCeti.DynkinType.B n
• (TauCeti.LieTypeIndex.C n q).dynkinType = TauCeti.DynkinType.C n
• (TauCeti.LieTypeIndex.D n q).dynkinType = TauCeti.DynkinType.D n
• (TauCeti.LieTypeIndex.twistedD n q).dynkinType = TauCeti.DynkinType.D n
• (TauCeti.LieTypeIndex.trialityD4 q).dynkinType = TauCeti.DynkinType.D 4
• (TauCeti.LieTypeIndex.E6 q).dynkinType = TauCeti.DynkinType.E6
• (TauCeti.LieTypeIndex.twistedE6 q).dynkinType = TauCeti.DynkinType.E6
• (TauCeti.LieTypeIndex.E7 q).dynkinType = TauCeti.DynkinType.E7
• (TauCeti.LieTypeIndex.E8 q).dynkinType = TauCeti.DynkinType.E8
• (TauCeti.LieTypeIndex.F4 q).dynkinType = TauCeti.DynkinType.F4
• (TauCeti.LieTypeIndex.reeF4 m).dynkinType = TauCeti.DynkinType.F4
• TauCeti.LieTypeIndex.tits.dynkinType = TauCeti.DynkinType.F4
• (TauCeti.LieTypeIndex.G2 q).dynkinType = TauCeti.DynkinType.G2
• (TauCeti.LieTypeIndex.reeG2 m).dynkinType = TauCeti.DynkinType.G2
• (TauCeti.LieTypeIndex.suzuki m).dynkinType = TauCeti.DynkinType.B 2

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_A (n : ℕ) (q : PrimePower) : (A n q).dynkinType = DynkinType.A n

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_twistedA (n : ℕ) (q : PrimePower) : (twistedA n q).dynkinType = DynkinType.A n

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_B (n : ℕ) (q : PrimePower) : (B n q).dynkinType = DynkinType.B n

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_C (n : ℕ) (q : PrimePower) : (C n q).dynkinType = DynkinType.C n

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_D (n : ℕ) (q : PrimePower) : (D n q).dynkinType = DynkinType.D n

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_twistedD (n : ℕ) (q : PrimePower) : (twistedD n q).dynkinType = DynkinType.D n

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_trialityD4 (q : PrimePower) : (trialityD4 q).dynkinType = DynkinType.D 4

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_E6 (q : PrimePower) : (E6 q).dynkinType = DynkinType.E6

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_twistedE6 (q : PrimePower) : (twistedE6 q).dynkinType = DynkinType.E6

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_E7 (q : PrimePower) : (E7 q).dynkinType = DynkinType.E7

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_E8 (q : PrimePower) : (E8 q).dynkinType = DynkinType.E8

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_F4 (q : PrimePower) : (F4 q).dynkinType = DynkinType.F4

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_reeF4 (m : ℕ) : (reeF4 m).dynkinType = DynkinType.F4

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_tits : tits.dynkinType = DynkinType.F4

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_G2 (q : PrimePower) : (G2 q).dynkinType = DynkinType.G2

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_reeG2 (m : ℕ) : (reeG2 m).dynkinType = DynkinType.G2

@[simp]

theorem TauCeti.LieTypeIndex.dynkinType_suzuki (m : ℕ) : (suzuki m).dynkinType = DynkinType.B 2

def TauCeti.LieTypeIndex.HasUnimodularDiagram : LieTypeIndex → Prop

The Lie-type families whose underlying Dynkin diagram has unimodular Cartan matrix, namely E₈, F₄ and G₂.

Both the untwisted families E₈(q), F₄(q), G₂(q) and the Ree families ²G₂(3^(2m+1)), ²F₄(2^(2m+1)) together with the Tits index are included: the predicate constrains the diagram and not the Steinberg map. The Suzuki family is the one Suzuki--Ree constructor left out, its diagram being B₂, whose Cartan matrix has determinant two.

Equations

• (TauCeti.LieTypeIndex.E8 q).HasUnimodularDiagram = True
• (TauCeti.LieTypeIndex.F4 q).HasUnimodularDiagram = True
• (TauCeti.LieTypeIndex.G2 q).HasUnimodularDiagram = True
• (TauCeti.LieTypeIndex.reeG2 m).HasUnimodularDiagram = True
• (TauCeti.LieTypeIndex.reeF4 m).HasUnimodularDiagram = True
• TauCeti.LieTypeIndex.tits.HasUnimodularDiagram = True
• x✝.HasUnimodularDiagram = False

@[simp]

theorem TauCeti.LieTypeIndex.hasUnimodularDiagram_iff (d : LieTypeIndex) : d.HasUnimodularDiagram ↔ match d with | E8 q => True | F4 q => True | G2 q => True | reeG2 m => True | reeF4 m => True | tits => True | x => False

Characterization of the families with unimodular diagram.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredHasUnimodularDiagram : DecidablePred HasUnimodularDiagram

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LieTypeIndex.hasUnimodularDiagram_iff_dynkinType (d : LieTypeIndex) : d.HasUnimodularDiagram ↔ d.dynkinType = DynkinType.E8 ∨ d.dynkinType = DynkinType.F4 ∨ d.dynkinType = DynkinType.G2

An index has unimodular diagram exactly when its underlying Dynkin type is E₈, F₄ or G₂.

theorem TauCeti.LieTypeIndex.exists_eq_of_hasUnimodularDiagram {d : LieTypeIndex} (hd : d.HasUnimodularDiagram) : (∃ (q : PrimePower), d = E8 q ∨ d = F4 q ∨ d = G2 q) ∨ (∃ (m : ℕ), d = reeG2 m ∨ d = reeF4 m) ∨ d = tits

The six families with unimodular diagram.

theorem TauCeti.LieTypeIndex.exists_eq_of_hasUnimodularDiagram_of_not_usesHalfFrobenius {d : LieTypeIndex} (hd : d.HasUnimodularDiagram) (hf : ¬d.UsesHalfFrobenius) : ∃ (q : PrimePower), d = E8 q ∨ d = F4 q ∨ d = G2 q

The three untwisted families with unimodular diagram. Removing the Suzuki--Ree constructors from the previous list leaves E₈(q), F₄(q) and G₂(q).

def TauCeti.LieTypeIndex.HasTypeDDiagram : LieTypeIndex → Prop

The Lie-type families whose underlying Dynkin diagram is of type Dₙ: the untwisted family Dₙ(q), the graph-twisted family ²Dₙ(q), and the triality-twisted family ³D₄(q).

Like TauCeti.LieTypeIndex.HasUnimodularDiagram this constrains the diagram alone and says nothing about the Steinberg map, which is what makes it the right hypothesis for data depending only on the diagram. The three families differ in the diagram permutation their Steinberg map composes with, of order one, two and three respectively. They do not all share a carrier: triality has no linear realization on the spin module the other two are built on, so ³D₄(q) is built on the tripled carrier TauCeti.D4Tripled.groupScheme.

Equations

• (TauCeti.LieTypeIndex.D rank q).HasTypeDDiagram = True
• (TauCeti.LieTypeIndex.twistedD rank q).HasTypeDDiagram = True
• (TauCeti.LieTypeIndex.trialityD4 q).HasTypeDDiagram = True
• x✝.HasTypeDDiagram = False

@[simp]

theorem TauCeti.LieTypeIndex.hasTypeDDiagram_iff (d : LieTypeIndex) : d.HasTypeDDiagram ↔ match d with | D rank q => True | twistedD rank q => True | trialityD4 q => True | x => False

Characterization of the families on a type-D diagram.

@[instance_reducible]

instance TauCeti.LieTypeIndex.instDecidablePredHasTypeDDiagram : DecidablePred HasTypeDDiagram

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.LieTypeIndex.hasTypeDDiagram_iff_dynkinType (d : LieTypeIndex) : d.HasTypeDDiagram ↔ ∃ (n : ℕ), d.dynkinType = DynkinType.D n

An index has a type-D diagram exactly when its underlying Dynkin type is some Dₙ.

theorem TauCeti.LieTypeIndex.exists_eq_of_hasTypeDDiagram {d : LieTypeIndex} (hd : d.HasTypeDDiagram) : (∃ (n : ℕ) (q : PrimePower), d = D n q ∨ d = twistedD n q) ∨ ∃ (q : PrimePower), d = trialityD4 q

The three families on a type-D diagram.

theorem TauCeti.LieTypeIndex.not_usesHalfFrobenius_of_hasTypeDDiagram {d : LieTypeIndex} (hd : d.HasTypeDDiagram) : ¬d.UsesHalfFrobenius

No family on a type-D diagram uses a half-Frobenius, so each of the three carries a diagram permutation and an ordinary Steinberg map.

theorem TauCeti.LieTypeIndex.not_hasUnimodularDiagram_of_hasTypeDDiagram {d : LieTypeIndex} (hd : d.HasTypeDDiagram) : ¬d.HasUnimodularDiagram

A type-D diagram is not unimodular. Consequently the adjoint Geck carrier, whose weights span the whole character lattice exactly on the three types named by TauCeti.DynkinType.span_range_geckWeight_eq_top_iff, is not the simply connected form on these branches, and the type-D families need a carrier of their own.

theorem TauCeti.LieTypeIndex.hasTypeDDiagram_of_isTypeD {d : LieTypeIndex} (h : d.IsTypeD) : d.HasTypeDDiagram

The untwisted family Dₙ(q) is built on a type-D diagram.

theorem TauCeti.LieTypeIndex.hasTypeDDiagram_of_isTypeTwistedD {d : LieTypeIndex} (h : d.IsTypeTwistedD) : d.HasTypeDDiagram

The graph-twisted family ²Dₙ(q) is built on a type-D diagram.

theorem TauCeti.LieTypeIndex.hasTypeDDiagram_of_isTypeTrialityD4 {d : LieTypeIndex} (h : d.IsTypeTrialityD4) : d.HasTypeDDiagram

The triality-twisted family ³D₄(q) is built on a type-D diagram.

theorem TauCeti.LieTypeIndex.exists_eq_of_dynkinType_eq_B_two {d : LieTypeIndex} (hd : d.dynkinType = DynkinType.B 2) : (∃ (q : PrimePower), d = B 2 q) ∨ ∃ (m : ℕ), d = suzuki m

The two families on the rank-two diagram B₂. They are the untwisted B₂(q) and the Suzuki family ²B₂(2^(2m+1)); the converse inclusions are dynkinType_B and dynkinType_suzuki. No rank-two C index appears: the C family starts at rank three in InStandardRange, so B₂(q) = C₂(q) is always named in the B family.

theorem TauCeti.LieTypeIndex.exists_eq_B_of_dynkinType_eq_B_two_of_not_usesHalfFrobenius {d : LieTypeIndex} (hd : d.dynkinType = DynkinType.B 2) (hf : ¬d.UsesHalfFrobenius) : ∃ (q : PrimePower), d = B 2 q

The one untwisted family on the rank-two diagram B₂. Removing the Suzuki constructor, the one of the two families of exists_eq_of_dynkinType_eq_B_two using a half-Frobenius, leaves B₂(q).

def TauCeti.LieTypeIndex.characteristic : LieTypeIndex → ℕ

The characteristic of the field over which the ambient group will be constructed.

Equations

• (TauCeti.LieTypeIndex.A rank q).characteristic = q.p
• (TauCeti.LieTypeIndex.twistedA rank q).characteristic = q.p
• (TauCeti.LieTypeIndex.B rank q).characteristic = q.p
• (TauCeti.LieTypeIndex.C rank q).characteristic = q.p
• (TauCeti.LieTypeIndex.D rank q).characteristic = q.p
• (TauCeti.LieTypeIndex.twistedD rank q).characteristic = q.p
• (TauCeti.LieTypeIndex.E6 q).characteristic = q.p
• (TauCeti.LieTypeIndex.E7 q).characteristic = q.p
• (TauCeti.LieTypeIndex.E8 q).characteristic = q.p
• (TauCeti.LieTypeIndex.F4 q).characteristic = q.p
• (TauCeti.LieTypeIndex.G2 q).characteristic = q.p
• (TauCeti.LieTypeIndex.twistedE6 q).characteristic = q.p
• (TauCeti.LieTypeIndex.trialityD4 q).characteristic = q.p
• (TauCeti.LieTypeIndex.reeG2 m).characteristic = 3
• (TauCeti.LieTypeIndex.suzuki m).characteristic = 2
• (TauCeti.LieTypeIndex.reeF4 m).characteristic = 2
• TauCeti.LieTypeIndex.tits.characteristic = 2

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_A (n : ℕ) (q : PrimePower) : (A n q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_twistedA (n : ℕ) (q : PrimePower) : (twistedA n q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_B (n : ℕ) (q : PrimePower) : (B n q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_C (n : ℕ) (q : PrimePower) : (C n q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_D (n : ℕ) (q : PrimePower) : (D n q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_twistedD (n : ℕ) (q : PrimePower) : (twistedD n q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_E6 (q : PrimePower) : (E6 q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_E7 (q : PrimePower) : (E7 q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_E8 (q : PrimePower) : (E8 q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_F4 (q : PrimePower) : (F4 q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_G2 (q : PrimePower) : (G2 q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_twistedE6 (q : PrimePower) : (twistedE6 q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_trialityD4 (q : PrimePower) : (trialityD4 q).characteristic = q.p

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_reeG2 (m : ℕ) : (reeG2 m).characteristic = 3

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_suzuki (m : ℕ) : (suzuki m).characteristic = 2

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_reeF4 (m : ℕ) : (reeF4 m).characteristic = 2

@[simp]

theorem TauCeti.LieTypeIndex.characteristic_tits : tits.characteristic = 2

theorem TauCeti.LieTypeIndex.characteristic_prime (d : LieTypeIndex) : Nat.Prime d.characteristic

The characteristic attached to a Lie-type index is prime.

instance TauCeti.LieTypeIndex.instFactPrimeCharacteristic (d : LieTypeIndex) : Fact (Nat.Prime d.characteristic)

The fact instance that equips ZMod d.characteristic with its field structure downstream.

It is stated for a bare index rather than for a TauCeti.ValidLieTypeIndex, so that it also applies at an explicitly written constructor such as LieTypeIndex.A rank q: through Subtype.val ?d the validated form is not a matchable instance key.

def TauCeti.LieTypeIndex.fieldOrder : LieTypeIndex → ℕ

The Frobenius/classification parameter q. For ordinary and graph-twisted families this is the exponent in Frob_q, not the cardinality of the extension field used by a twisted matrix realization. For Suzuki--Ree families it is their field order p ^ (2 * m + 1).

Equations

• (TauCeti.LieTypeIndex.A rank q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.twistedA rank q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.B rank q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.C rank q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.D rank q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.twistedD rank q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.E6 q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.E7 q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.E8 q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.F4 q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.G2 q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.twistedE6 q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.trialityD4 q).fieldOrder = q.card
• (TauCeti.LieTypeIndex.suzuki m).fieldOrder = 2 ^ (2 * m + 1)
• (TauCeti.LieTypeIndex.reeF4 m).fieldOrder = 2 ^ (2 * m + 1)
• (TauCeti.LieTypeIndex.reeG2 m).fieldOrder = 3 ^ (2 * m + 1)
• TauCeti.LieTypeIndex.tits.fieldOrder = 2

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_A (n : ℕ) (q : PrimePower) : (A n q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_twistedA (n : ℕ) (q : PrimePower) : (twistedA n q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_B (n : ℕ) (q : PrimePower) : (B n q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_C (n : ℕ) (q : PrimePower) : (C n q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_D (n : ℕ) (q : PrimePower) : (D n q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_twistedD (n : ℕ) (q : PrimePower) : (twistedD n q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_E6 (q : PrimePower) : (E6 q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_E7 (q : PrimePower) : (E7 q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_E8 (q : PrimePower) : (E8 q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_F4 (q : PrimePower) : (F4 q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_G2 (q : PrimePower) : (G2 q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_twistedE6 (q : PrimePower) : (twistedE6 q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_trialityD4 (q : PrimePower) : (trialityD4 q).fieldOrder = q.card

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_suzuki (m : ℕ) : (suzuki m).fieldOrder = 2 ^ (2 * m + 1)

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_reeF4 (m : ℕ) : (reeF4 m).fieldOrder = 2 ^ (2 * m + 1)

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_reeG2 (m : ℕ) : (reeG2 m).fieldOrder = 3 ^ (2 * m + 1)

@[simp]

theorem TauCeti.LieTypeIndex.fieldOrder_tits : tits.fieldOrder = 2

def TauCeti.LieTypeIndex.fieldExponent : LieTypeIndex → ℕ

The exponent writing the Frobenius parameter q as a power of the characteristic. It is the stored exponent of the prime power on the ordinary and graph-twisted branches, the odd number 2 * m + 1 on the Suzuki--Ree branches, whose field order is p ^ (2 * m + 1), and 1 on the Tits branch, whose field order is the characteristic 2 itself.

This is not a second numeric parameter: fieldOrder_eq_characteristic_pow recovers fieldOrder from it, and it exists because the q-power Frobenius of a field of characteristic p is the fieldExponent-fold iterate of the p-power Frobenius.

Equations

• (TauCeti.LieTypeIndex.A rank q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.twistedA rank q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.B rank q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.C rank q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.D rank q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.twistedD rank q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.E6 q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.E7 q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.E8 q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.F4 q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.G2 q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.twistedE6 q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.trialityD4 q).fieldExponent = q.exponent
• (TauCeti.LieTypeIndex.suzuki m).fieldExponent = 2 * m + 1
• (TauCeti.LieTypeIndex.reeF4 m).fieldExponent = 2 * m + 1
• (TauCeti.LieTypeIndex.reeG2 m).fieldExponent = 2 * m + 1
• TauCeti.LieTypeIndex.tits.fieldExponent = 1

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_A (n : ℕ) (q : PrimePower) : (A n q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_twistedA (n : ℕ) (q : PrimePower) : (twistedA n q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_B (n : ℕ) (q : PrimePower) : (B n q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_C (n : ℕ) (q : PrimePower) : (C n q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_D (n : ℕ) (q : PrimePower) : (D n q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_twistedD (n : ℕ) (q : PrimePower) : (twistedD n q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_E6 (q : PrimePower) : (E6 q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_E7 (q : PrimePower) : (E7 q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_E8 (q : PrimePower) : (E8 q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_F4 (q : PrimePower) : (F4 q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_G2 (q : PrimePower) : (G2 q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_twistedE6 (q : PrimePower) : (twistedE6 q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_trialityD4 (q : PrimePower) : (trialityD4 q).fieldExponent = q.exponent

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_suzuki (m : ℕ) : (suzuki m).fieldExponent = 2 * m + 1

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_reeF4 (m : ℕ) : (reeF4 m).fieldExponent = 2 * m + 1

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_reeG2 (m : ℕ) : (reeG2 m).fieldExponent = 2 * m + 1

@[simp]

theorem TauCeti.LieTypeIndex.fieldExponent_tits : tits.fieldExponent = 1

theorem TauCeti.LieTypeIndex.fieldOrder_eq_characteristic_pow (d : LieTypeIndex) : d.fieldOrder = d.characteristic ^ d.fieldExponent

The Frobenius parameter is the recorded power of the characteristic.

theorem TauCeti.LieTypeIndex.fieldExponent_pos (d : LieTypeIndex) : 0 < d.fieldExponent

The exponent writing the Frobenius parameter as a power of the characteristic is positive, so the Frobenius parameter is never 1.

theorem TauCeti.LieTypeIndex.one_lt_fieldOrder (d : LieTypeIndex) : 1 < d.fieldOrder

The Frobenius parameter is a positive power of a prime, hence at least two.

theorem TauCeti.LieTypeIndex.fieldOrder_pos (d : LieTypeIndex) : 0 < d.fieldOrder

The Frobenius parameter of a Lie-type index is positive, being a power of its prime characteristic. This is the form in which the parameter is read as the scaling factor of the root-datum Frobenius.

def TauCeti.LieTypeIndex.fieldOrderPNat (d : LieTypeIndex) : ℕ+

The Frobenius parameter as a positive natural number, packaging one_lt_fieldOrder. This is the form taken by the later constructions that scale by q and need it to be positive.

Equations

• d.fieldOrderPNat = d.fieldOrder.toPNat ⋯

@[simp]

theorem TauCeti.LieTypeIndex.coe_fieldOrderPNat (d : LieTypeIndex) : ↑d.fieldOrderPNat = d.fieldOrder

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex : Type

A Lie-type index satisfying its rank, field, and preferred-representative conditions. Later carrier-valued constructions take this subtype, so they need no branch for an invalid Dynkin rank or an excluded small group.

Equations

• TauCeti.ValidLieTypeIndex = { d : TauCeti.LieTypeIndex // d.Valid }

@[reducible, inline]

abbrev TauCeti.SuzukiReeIndex : Type

A valid index whose Steinberg map is an odd power of a half-Frobenius: the three Suzuki--Ree families together with the Tits group.

Equations

• TauCeti.SuzukiReeIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).UsesHalfFrobenius }

@[reducible, inline]

abbrev TauCeti.GraphTwistedIndex : Type

A valid index whose Steinberg map uses ordinary Frobenius, possibly composed with a diagram automorphism. The Suzuki--Ree and Tits branches are excluded.

Equations

• TauCeti.GraphTwistedIndex = { d : TauCeti.ValidLieTypeIndex // ¬(↑d).UsesHalfFrobenius }

@[reducible, inline]

abbrev TauCeti.UnimodularLieIndex : Type

A valid index whose underlying Dynkin diagram has unimodular Cartan matrix: the six branches E₈(q), F₄(q), G₂(q), ²G₂(3^(2m+1)), ²F₄(2^(2m+1)) and ²F₄(2)'. These are the diagrams on which the Geck weights span the full character lattice (TauCeti.DynkinType.span_range_geckWeight_eq_top_iff), so this subtype is the domain of the lattice results that span buys.

Equations

• TauCeti.UnimodularLieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).HasUnimodularDiagram }

@[reducible, inline]

abbrev TauCeti.TypeALieIndex : Type

A validated index in one of the two type-A families A_r(q) and ²A_r(q).

The outer subtype is important: a raw type-A constructor with an excluded rank or field parameter is not a TypeALieIndex.

Equations

• TauCeti.TypeALieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).IsTypeA }

@[reducible, inline]

abbrev TauCeti.TypeCLieIndex : Type

A validated index in the untwisted type-C family C_r(q).

In particular, its rank is at least three and its characteristic is not two.

Equations

• TauCeti.TypeCLieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).IsTypeC }

@[reducible, inline]

abbrev TauCeti.TypeE6LieIndex : Type

A validated index in the untwisted exceptional family E₆(q).

Every E₆(q) is valid, by TauCeti.LieTypeIndex.valid_E6, so the outer subtype excludes nothing here; it is retained so that this family sits inside TauCeti.ValidLieTypeIndex, which the carrier-valued constructions take. The graph-twisted family ²E₆(q), which shares the diagram, is not of this subtype.

Equations

• TauCeti.TypeE6LieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).IsTypeE6 }

@[reducible, inline]

abbrev TauCeti.TypeTwistedE6LieIndex : Type

A validated index in the graph-twisted exceptional family ²E₆(q).

Every ²E₆(q) is valid, by TauCeti.LieTypeIndex.valid_twistedE6, so the outer subtype excludes nothing here; it is retained so that this family sits inside TauCeti.ValidLieTypeIndex, which the carrier-valued constructions take. The untwisted family E₆(q), which shares the diagram, is not of this subtype: the two differ by the diagram automorphism their Steinberg maps compose with, and they are built on different carriers, since the E₆ diagram symmetry does not act on the 27-dimensional minuscule one.

Equations

• TauCeti.TypeTwistedE6LieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).IsTypeTwistedE6 }

@[reducible, inline]

abbrev TauCeti.SuzukiLieIndex : Type

A validated index in the Suzuki family ²B₂(2^(2m+1)).

The outer subtype is important: ²B₂(2), the parameter m = 0, is excluded from the classification list. It is itself the Frobenius group of order twenty, whose derived subgroup is cyclic of order five and is its own centre, so the derived-subgroup recipe collapses to the trivial group rather than a simple one, and ²B₂(2) is not a SuzukiLieIndex. The Suzuki--Ree relatives ²G₂, ²F₄ and the Tits group are excluded too; they are the other three constructors of TauCeti.SuzukiReeIndex.

Equations

• TauCeti.SuzukiLieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).IsSuzuki }

@[reducible, inline]

abbrev TauCeti.TypeDDiagramLieIndex : Type

A validated index on a type-Dₙ diagram: the untwisted Dₙ(q), the graph-twisted ²Dₙ(q), or the triality-twisted ³D₄(q).

The three families are collected because they share their diagram, and with it everything read off the diagram, while the family enters through the diagram permutation. The untwisted and graph-twisted families also share their carrier, the spin carrier TauCeti.TypeDSpinCarrier; the triality-twisted family is built on the tripled carrier TauCeti.D4Tripled.groupScheme instead. Its rank is at least four, by TauCeti.TypeDDiagramLieIndex.four_le_rank.

Equations

• TauCeti.TypeDDiagramLieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).HasTypeDDiagram }

@[reducible, inline]

abbrev TauCeti.TypeDLieIndex : Type

A validated index in the untwisted type-D family Dₙ(q).

The outer subtype is important: D₂(q) and D₃(q) are not names on the classification list, their diagrams being A₁ × A₁ and A₃, so they are not indices of this subtype.

Equations

• TauCeti.TypeDLieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).IsTypeD }

@[reducible, inline]

abbrev TauCeti.TypeTwistedDLieIndex : Type

A validated index in the graph-twisted type-D family ²Dₙ(q), whose Steinberg map twists by the exchange of the two fork nodes. Its rank is at least four, for the same reason as for the untwisted family.

Equations

• TauCeti.TypeTwistedDLieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).IsTypeTwistedD }

@[reducible, inline]

abbrev TauCeti.TypeTrialityD4LieIndex : Type

A validated index in the triality-twisted family ³D₄(q), whose Steinberg map twists by the order-three symmetry of the D₄ diagram. Every ³D₄(q) is valid, by TauCeti.LieTypeIndex.valid_trialityD4.

Equations

• TauCeti.TypeTrialityD4LieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).IsTypeTrialityD4 }

@[reducible, inline]

abbrev TauCeti.RankTwoBLieIndex : Type

A validated index built on the rank-two diagram B₂: the untwisted family B₂(q) and the Suzuki family ²B₂(2^(2m+1)).

The condition constrains the diagram and not the Steinberg map, so it holds both of the untwisted family, whose Steinberg map is the q-power Frobenius, and of the Suzuki family, whose Steinberg map is an odd power of a half-Frobenius. No rank-two C index appears: the C family starts at rank three in InStandardRange, so B₂(q) = C₂(q) is always named in the B family.

This is diagram-level indexing data only; the carrier both branches share is attached in TauCeti/GroupTheory/SpecificGroups/CFSG/TypeB/Two/Basic.lean. The outer subtype is important: B₂(2), B₂(3) and ²B₂(2) are excluded from the classification list and are not indices of this subtype; those exclusions are the small isomorphisms of Gorenstein--Lyons--Solomon, Number 1, §2.2.

Equations

• TauCeti.RankTwoBLieIndex = { d : TauCeti.ValidLieTypeIndex // (↑d).dynkinType = TauCeti.DynkinType.B 2 }

@[reducible, inline]

abbrev TauCeti.TypeB2LieIndex : Type

A validated index in the untwisted rank-two family B₂(q). The Suzuki family, which shares the diagram, is excluded by the outer predicate.

Equations

• TauCeti.TypeB2LieIndex = { d : TauCeti.RankTwoBLieIndex // ¬(↑↑d).UsesHalfFrobenius }

@[reducible, inline]

abbrev TauCeti.TypeALieIndex.ofA (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.A rank q).Valid) : TypeALieIndex

Introduce a valid untwisted type-A index.

Equations

• TauCeti.TypeALieIndex.ofA rank q hvalid = ⟨⟨TauCeti.LieTypeIndex.A rank q, hvalid⟩, ⋯⟩

@[reducible, inline]

abbrev TauCeti.TypeALieIndex.ofTwistedA (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.twistedA rank q).Valid) : TypeALieIndex

Introduce a valid graph-twisted type-A index.

Equations

• TauCeti.TypeALieIndex.ofTwistedA rank q hvalid = ⟨⟨TauCeti.LieTypeIndex.twistedA rank q, hvalid⟩, ⋯⟩

theorem TauCeti.TypeALieIndex.exists_eq_ofA_or_exists_eq_ofTwistedA (d : TypeALieIndex) : (∃ (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.A rank q).Valid), d = ofA rank q hvalid) ∨ ∃ (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.twistedA rank q).Valid), d = ofTwistedA rank q hvalid

Every type-A index is one of the two introduction forms. This is the eliminator matching ofA and ofTwistedA, so a consumer never repeats the case split over the other constructors.

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex.dynkinType (d : ValidLieTypeIndex) : DynkinType

The total Dynkin-diagram map, restricted along the valid-index coercion.

Equations

• d.dynkinType = (↑d).dynkinType

theorem TauCeti.ValidLieTypeIndex.dynkinType_valid (d : ValidLieTypeIndex) : (↑d).dynkinType.Valid

Every valid Lie-type index names a valid Dynkin type.

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex.rank (d : ValidLieTypeIndex) : ℕ

The rank of the underlying untwisted Dynkin diagram. This is derived from dynkinType, not tabulated independently.

Equations

• d.rank = d.dynkinType.rank

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex.characteristic (d : ValidLieTypeIndex) : ℕ

The total characteristic map, restricted along the valid-index coercion.

Equations

• d.characteristic = (↑d).characteristic

theorem TauCeti.ValidLieTypeIndex.characteristic_prime (d : ValidLieTypeIndex) : Nat.Prime d.characteristic

The characteristic attached to a valid Lie-type index is prime.

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex.fieldOrder (d : ValidLieTypeIndex) : ℕ

The total Frobenius-parameter map, restricted along the valid-index coercion.

Equations

• d.fieldOrder = (↑d).fieldOrder

@[reducible, inline]

abbrev TauCeti.ValidLieTypeIndex.fieldExponent (d : ValidLieTypeIndex) : ℕ

The total field-exponent map, restricted along the valid-index coercion.

Equations

• d.fieldExponent = (↑d).fieldExponent

theorem TauCeti.ValidLieTypeIndex.fieldOrder_eq_characteristic_pow (d : ValidLieTypeIndex) : d.fieldOrder = d.characteristic ^ d.fieldExponent

The Frobenius parameter of a valid index is the recorded power of its characteristic.

theorem TauCeti.ValidLieTypeIndex.fieldExponent_pos (d : ValidLieTypeIndex) : 0 < d.fieldExponent

The field exponent of a valid index is positive.

theorem TauCeti.ValidLieTypeIndex.fieldOrder_pos (d : ValidLieTypeIndex) : 0 < d.fieldOrder

The Frobenius parameter of a valid index is positive.

@[reducible, inline]

abbrev TauCeti.TypeCLieIndex.of (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.C rank q).Valid) : TypeCLieIndex

Introduce a valid type-C index.

Equations

• TauCeti.TypeCLieIndex.of rank q hvalid = ⟨⟨TauCeti.LieTypeIndex.C rank q, hvalid⟩, trivial⟩

theorem TauCeti.TypeCLieIndex.exists_eq_of (d : TypeCLieIndex) : ∃ (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.C rank q).Valid), d = of rank q hvalid

Every type-C index is an introduction form of rank q hvalid.

theorem TauCeti.TypeCLieIndex.dynkinType_cartanMatrix_apply (d : TypeCLieIndex) (i j : Fin (↑d).rank) : (↑d).dynkinType.cartanMatrix i j = CartanMatrix.C (↑d).rank i j

The Cartan matrix of the diagram a validated type-C index names, entry by entry: it is the type-C Cartan matrix at the index's rank. This is the projection of the introduction form TauCeti.TypeCLieIndex.of through TauCeti.DynkinType.cartanMatrix_C, stated on entries rather than on matrices because the rank occurs in the index types of the two nodes.

theorem TauCeti.TypeCLieIndex.three_le_rank (d : TypeCLieIndex) : 3 ≤ (↑d).rank

The rank of a validated type-C index is at least three.

theorem TauCeti.TypeCLieIndex.characteristic_ne_two (d : TypeCLieIndex) : (↑d).characteristic ≠ 2

A validated type-C index has characteristic different from two.

The families on the B₂ diagram

This section follows ValidLieTypeIndex rather than sitting beside TypeALieIndex, because rank_eq_two reads the numbered data TauCeti.ValidLieTypeIndex.rank defined just above.

@[simp]

theorem TauCeti.RankTwoBLieIndex.dynkinType_eq (d : RankTwoBLieIndex) : (↑d).dynkinType = DynkinType.B 2

An index on the B₂ diagram names the Dynkin type B 2.

@[simp]

theorem TauCeti.RankTwoBLieIndex.rank_eq_two (d : RankTwoBLieIndex) : (↑d).rank = 2

An index on the B₂ diagram has rank two, that being the rank of B₂.

@[reducible, inline]

abbrev TauCeti.RankTwoBLieIndex.ofB (q : PrimePower) (hvalid : (LieTypeIndex.B 2 q).Valid) : RankTwoBLieIndex

Introduce the untwisted branch B₂(q).

Equations

• TauCeti.RankTwoBLieIndex.ofB q hvalid = ⟨⟨TauCeti.LieTypeIndex.B 2 q, hvalid⟩, ⋯⟩

@[reducible, inline]

abbrev TauCeti.RankTwoBLieIndex.ofSuzuki (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : RankTwoBLieIndex

Introduce the Suzuki branch ²B₂(2^(2m+1)).

Equations

• TauCeti.RankTwoBLieIndex.ofSuzuki m hvalid = ⟨⟨TauCeti.LieTypeIndex.suzuki m, hvalid⟩, ⋯⟩

theorem TauCeti.RankTwoBLieIndex.exists_eq_ofB_or_exists_eq_ofSuzuki (d : RankTwoBLieIndex) : (∃ (q : PrimePower) (hvalid : (LieTypeIndex.B 2 q).Valid), d = ofB q hvalid) ∨ ∃ (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid), d = ofSuzuki m hvalid

Every index on the B₂ diagram is one of the two introduction forms. This is the eliminator matching ofB and ofSuzuki, so a consumer never repeats the case split over the other constructors.

theorem TauCeti.RankTwoBLieIndex.ofB_ne_ofSuzuki (q : PrimePower) (hq : (LieTypeIndex.B 2 q).Valid) (m : ℕ) (hm : (LieTypeIndex.suzuki m).Valid) : ofB q hq ≠ ofSuzuki m hm

The two branches are disjoint, so the eliminator above splits every index on the B₂ diagram into exactly one of them.

@[reducible, inline]

abbrev TauCeti.TypeB2LieIndex.of (q : PrimePower) (hvalid : (LieTypeIndex.B 2 q).Valid) : TypeB2LieIndex

Introduce a valid untwisted index B₂(q). Validity forces 4 ≤ q.card, by four_le_fieldOrder below.

Equations

• TauCeti.TypeB2LieIndex.of q hvalid = ⟨TauCeti.RankTwoBLieIndex.ofB q hvalid, ⋯⟩

theorem TauCeti.TypeB2LieIndex.exists_eq_of (d : TypeB2LieIndex) : ∃ (q : PrimePower) (hvalid : (LieTypeIndex.B 2 q).Valid), d = of q hvalid

Every untwisted rank-two type-B index is of the introduction form.

theorem TauCeti.TypeB2LieIndex.four_le_fieldOrder (d : TypeB2LieIndex) : 4 ≤ (↑↑d).fieldOrder

The field order of an untwisted rank-two type-B index is at least four. The two smaller prime powers are excluded from the classification list as duplicate representatives.

@[reducible, inline]

abbrev TauCeti.SuzukiLieIndex.of (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : SuzukiLieIndex

Introduce a valid Suzuki index ²B₂(2^(2m+1)). Validity forces 1 ≤ m.

Equations

• TauCeti.SuzukiLieIndex.of m hvalid = ⟨⟨TauCeti.LieTypeIndex.suzuki m, hvalid⟩, ⋯⟩

theorem TauCeti.SuzukiLieIndex.exists_eq_of (d : SuzukiLieIndex) : ∃ (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid), d = of m hvalid

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

@[simp]

theorem TauCeti.SuzukiLieIndex.dynkinType_eq (d : SuzukiLieIndex) : (↑d).dynkinType = DynkinType.B 2

The Suzuki family is built on the rank-two diagram B₂.

@[simp]

theorem TauCeti.SuzukiLieIndex.rank_eq_two (d : SuzukiLieIndex) : (↑d).rank = 2

The Suzuki family has rank two, that being the rank of B₂.

@[simp]

theorem TauCeti.SuzukiLieIndex.characteristic_eq_two (d : SuzukiLieIndex) : (↑d).characteristic = 2

The Suzuki family lives in characteristic two.

@[reducible, inline]

abbrev TauCeti.SuzukiLieIndex.toSuzukiReeIndex (d : SuzukiLieIndex) : SuzukiReeIndex

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

Equations

• d.toSuzukiReeIndex = ⟨↑d, ⋯⟩

@[reducible, inline]

abbrev TauCeti.SuzukiLieIndex.toRankTwoBLieIndex (d : SuzukiLieIndex) : RankTwoBLieIndex

A Suzuki index is an index on the rank-two diagram B₂. This is the reading through which the Suzuki family reaches the carrier data that TauCeti/GroupTheory/SpecificGroups/CFSG/TypeB/Two/Basic.lean attaches to that diagram and that it shares with the untwisted family B₂(q), the two differing only in the endomorphism taken of it.

Equations

• d.toRankTwoBLieIndex = ⟨↑d, ⋯⟩

The untwisted family E₆(q)

This section, like the Suzuki one above, follows ValidLieTypeIndex because rank_eq_six reads the numbered data TauCeti.ValidLieTypeIndex.rank defined there.

@[reducible, inline]

abbrev TauCeti.TypeE6LieIndex.of (q : PrimePower) : TypeE6LieIndex

Introduce the index E₆(q). No validity hypothesis is taken: every E₆ parameter is valid by TauCeti.LieTypeIndex.valid_E6.

Equations

• TauCeti.TypeE6LieIndex.of q = ⟨⟨TauCeti.LieTypeIndex.E6 q, ⋯⟩, ⋯⟩

theorem TauCeti.TypeE6LieIndex.exists_eq_of (d : TypeE6LieIndex) : ∃ (q : PrimePower), d = of q

Every untwisted type-E₆ index is of the introduction form. This is the eliminator matching of, so a consumer never repeats the case split over the other constructors.

@[simp]

theorem TauCeti.TypeE6LieIndex.dynkinType_eq (d : TypeE6LieIndex) : (↑d).dynkinType = DynkinType.E6

The untwisted family E₆(q) is built on the diagram E₆.

@[simp]

theorem TauCeti.TypeE6LieIndex.rank_eq_six (d : TypeE6LieIndex) : (↑d).rank = 6

The untwisted family E₆(q) has rank six, that being the rank of E₆.

The graph-twisted family ²E₆(q)

@[reducible, inline]

abbrev TauCeti.TypeTwistedE6LieIndex.of (q : PrimePower) : TypeTwistedE6LieIndex

Introduce the index ²E₆(q). No validity hypothesis is taken: every ²E₆ parameter is valid by TauCeti.LieTypeIndex.valid_twistedE6.

Equations

• TauCeti.TypeTwistedE6LieIndex.of q = ⟨⟨TauCeti.LieTypeIndex.twistedE6 q, ⋯⟩, ⋯⟩

theorem TauCeti.TypeTwistedE6LieIndex.exists_eq_of (d : TypeTwistedE6LieIndex) : ∃ (q : PrimePower), d = of q

Every graph-twisted type-E₆ index is of the introduction form. This is the eliminator matching of, so a consumer never repeats the case split over the other constructors.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.dynkinType_eq (d : TypeTwistedE6LieIndex) : (↑d).dynkinType = DynkinType.E6

The graph-twisted family ²E₆(q) is built on the diagram E₆.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.rank_eq_six (d : TypeTwistedE6LieIndex) : (↑d).rank = 6

The graph-twisted family ²E₆(q) has rank six, that being the rank of E₆.

The families on a type-D diagram

The untwisted Dₙ(q), the graph-twisted ²Dₙ(q) and the triality-twisted ³D₄(q) are the three classification-list families built on a Dₙ diagram. This section, like the two above, follows ValidLieTypeIndex because the rank statements read the numbered data TauCeti.ValidLieTypeIndex.rank defined there.

theorem TauCeti.TypeDDiagramLieIndex.dynkinType_eq (d : TypeDDiagramLieIndex) : (↑d).dynkinType = DynkinType.D (↑d).rank

The underlying Dynkin type of an index on a type-D diagram is Dₙ at the index's own rank.

It is deliberately not a simp lemma: the right-hand side mentions the rank, which is itself read off the Dynkin type, so the rewrite would reintroduce its own left-hand side.

theorem TauCeti.TypeDDiagramLieIndex.dynkinType_cartanMatrix_apply (d : TypeDDiagramLieIndex) (i j : Fin (↑d).rank) : (↑d).dynkinType.cartanMatrix i j = CartanMatrix.D (↑d).rank i j

The Cartan matrix of the diagram a validated index on a type-D diagram names, entry by entry: it is the type-D Cartan matrix at the index's rank. Like TauCeti.TypeCLieIndex.dynkinType_cartanMatrix_apply it is stated on entries rather than on matrices, because the rank occurs in the index types of the two nodes, so the Dynkin-type equation TauCeti.TypeDDiagramLieIndex.dynkinType_eq cannot be rewritten with directly.

theorem TauCeti.TypeDDiagramLieIndex.four_le_rank (d : TypeDDiagramLieIndex) : 4 ≤ (↑d).rank

The rank of a validated index on a type-D diagram is at least four. This is the range on which Dₙ is a valid Dynkin type, D₂ being A₁ × A₁ and D₃ being A₃ relabelled, and it is the hypothesis the type-D spin carrier TauCeti.TypeDSpinCarrier.groupScheme takes.

@[reducible, inline]

abbrev TauCeti.TypeDLieIndex.of (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.D rank q).Valid) : TypeDLieIndex

Introduce a valid untwisted type-D index.

Equations

• TauCeti.TypeDLieIndex.of rank q hvalid = ⟨⟨TauCeti.LieTypeIndex.D rank q, hvalid⟩, ⋯⟩

theorem TauCeti.TypeDLieIndex.exists_eq_of (d : TypeDLieIndex) : ∃ (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.D rank q).Valid), d = of rank q hvalid

Every untwisted type-D index is an introduction form of rank q hvalid. This is the eliminator matching of, so a consumer never repeats the case split over the other constructors.

@[reducible, inline]

abbrev TauCeti.TypeDLieIndex.toTypeDDiagramLieIndex (d : TypeDLieIndex) : TypeDDiagramLieIndex

The untwisted family Dₙ(q), regarded as a family on a type-D diagram.

Equations

• d.toTypeDDiagramLieIndex = ⟨↑d, ⋯⟩

@[reducible, inline]

abbrev TauCeti.TypeTwistedDLieIndex.of (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.twistedD rank q).Valid) : TypeTwistedDLieIndex

Introduce a valid graph-twisted type-D index.

Equations

• TauCeti.TypeTwistedDLieIndex.of rank q hvalid = ⟨⟨TauCeti.LieTypeIndex.twistedD rank q, hvalid⟩, ⋯⟩

theorem TauCeti.TypeTwistedDLieIndex.exists_eq_of (d : TypeTwistedDLieIndex) : ∃ (rank : ℕ) (q : PrimePower) (hvalid : (LieTypeIndex.twistedD rank q).Valid), d = of rank q hvalid

Every graph-twisted type-D index is an introduction form of rank q hvalid.

@[reducible, inline]

abbrev TauCeti.TypeTwistedDLieIndex.toTypeDDiagramLieIndex (d : TypeTwistedDLieIndex) : TypeDDiagramLieIndex

The graph-twisted family ²Dₙ(q), regarded as a family on a type-D diagram.

Equations

• d.toTypeDDiagramLieIndex = ⟨↑d, ⋯⟩

@[reducible, inline]

abbrev TauCeti.TypeTrialityD4LieIndex.of (q : PrimePower) : TypeTrialityD4LieIndex

Introduce the index ³D₄(q). No validity hypothesis is taken: every triality parameter is valid by TauCeti.LieTypeIndex.valid_trialityD4.

Equations

• TauCeti.TypeTrialityD4LieIndex.of q = ⟨⟨TauCeti.LieTypeIndex.trialityD4 q, ⋯⟩, ⋯⟩

theorem TauCeti.TypeTrialityD4LieIndex.exists_eq_of (d : TypeTrialityD4LieIndex) : ∃ (q : PrimePower), d = of q

Every triality-twisted index is of the introduction form.

@[reducible, inline]

abbrev TauCeti.TypeTrialityD4LieIndex.toTypeDDiagramLieIndex (d : TypeTrialityD4LieIndex) : TypeDDiagramLieIndex

The triality-twisted family ³D₄(q), regarded as a family on a type-D diagram.

Equations

• d.toTypeDDiagramLieIndex = ⟨↑d, ⋯⟩

@[simp]

theorem TauCeti.TypeTrialityD4LieIndex.dynkinType_eq (d : TypeTrialityD4LieIndex) : (↑d).dynkinType = DynkinType.D 4

The triality-twisted family ³D₄(q) is built on the diagram D₄.

@[simp]

theorem TauCeti.TypeTrialityD4LieIndex.rank_eq_four (d : TypeTrialityD4LieIndex) : (↑d).rank = 4

The triality-twisted family ³D₄(q) has rank four, that being the rank of D₄.

@[reducible, inline]

abbrev TauCeti.UnimodularLieIndex.e8 (q : PrimePower) : UnimodularLieIndex

The index E₈(q).

Equations

• TauCeti.UnimodularLieIndex.e8 q = ⟨⟨TauCeti.LieTypeIndex.E8 q, ⋯⟩, ⋯⟩

@[reducible, inline]

abbrev TauCeti.UnimodularLieIndex.f4 (q : PrimePower) : UnimodularLieIndex

The index F₄(q).

Equations

• TauCeti.UnimodularLieIndex.f4 q = ⟨⟨TauCeti.LieTypeIndex.F4 q, ⋯⟩, ⋯⟩

@[reducible, inline]

abbrev TauCeti.UnimodularLieIndex.g2 (q : PrimePower) (hq : 3 ≤ q.card) : UnimodularLieIndex

The index G₂(q), for q at least three: G₂(2) is excluded from the classification list, its recipe producing a group already named ²A₂(3).

Equations

• TauCeti.UnimodularLieIndex.g2 q hq = ⟨⟨TauCeti.LieTypeIndex.G2 q, ⋯⟩, ⋯⟩

@[reducible, inline]

abbrev TauCeti.UnimodularLieIndex.reeG2 (m : ℕ) (hm : 1 ≤ m) : UnimodularLieIndex

The Ree index ²G₂(3^(2m+1)), for m at least one: ²G₂(3) is excluded from the classification list, its recipe producing a group already named A₁(8).

Equations

• TauCeti.UnimodularLieIndex.reeG2 m hm = ⟨⟨TauCeti.LieTypeIndex.reeG2 m, ⋯⟩, ⋯⟩

@[reducible, inline]

abbrev TauCeti.UnimodularLieIndex.reeF4 (m : ℕ) (hm : 1 ≤ m) : UnimodularLieIndex

The Ree index ²F₄(2^(2m+1)), for m at least one: at m = 0 the recipe returns the Tits group ²F₄(2)', which the classification list carries under the separate name tits.

Equations

• TauCeti.UnimodularLieIndex.reeF4 m hm = ⟨⟨TauCeti.LieTypeIndex.reeF4 m, ⋯⟩, ⋯⟩

@[reducible, inline]

abbrev TauCeti.UnimodularLieIndex.tits : UnimodularLieIndex

The Tits index ²F₄(2)'.

Equations

• TauCeti.UnimodularLieIndex.tits = ⟨⟨TauCeti.LieTypeIndex.tits, TauCeti.UnimodularLieIndex.tits._proof_1⟩, TauCeti.UnimodularLieIndex.tits._proof_2⟩

@[reducible, inline]

abbrev TauCeti.UnimodularLieIndex.dynkinType (d : UnimodularLieIndex) : DynkinType

The underlying untwisted Dynkin diagram of an index with unimodular diagram.

Equations

• d.dynkinType = (↑d).dynkinType

theorem TauCeti.UnimodularLieIndex.dynkinType_valid (d : UnimodularLieIndex) : d.dynkinType.Valid

That diagram is a valid Dynkin type, so the pinned Geck carrier is available for it.

theorem TauCeti.UnimodularLieIndex.dynkinType_eq_E8_or_eq_F4_or_eq_G2 (d : UnimodularLieIndex) : d.dynkinType = DynkinType.E8 ∨ d.dynkinType = DynkinType.F4 ∨ d.dynkinType = DynkinType.G2

The underlying Dynkin type of an index with unimodular diagram is one of the three unimodular types.

Executable checks for the range conventions

Sporadic names and the full classification index

inductive TauCeti.SporadicName : Type

The twenty-six sporadic group names. Fi24Prime denotes Fi₂₄', and B and M denote the Baby Monster and Monster.

• M11 : SporadicName
• M12 : SporadicName
• M22 : SporadicName
• M23 : SporadicName
• M24 : SporadicName
• J1 : SporadicName
• J2 : SporadicName
• J3 : SporadicName
• J4 : SporadicName
• HS : SporadicName
• McL : SporadicName
• He : SporadicName
• Ru : SporadicName
• Suz : SporadicName
• ONan : SporadicName
• Co1 : SporadicName
• Co2 : SporadicName
• Co3 : SporadicName
• Fi22 : SporadicName
• Fi23 : SporadicName
• Fi24Prime : SporadicName
• HN : SporadicName
• Ly : SporadicName
• Th : SporadicName
• B : SporadicName
• M : SporadicName

@[instance_reducible]

instance TauCeti.instDecidableEqSporadicName : DecidableEq SporadicName

Equations

• TauCeti.instDecidableEqSporadicName x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TauCeti.instFintypeSporadicName : Fintype SporadicName

The finite enumeration of the twenty-six sporadic group names.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.card_sporadicName : Fintype.card SporadicName = 26

The sporadic-name enumeration has exactly twenty-six entries.

inductive TauCeti.CFSGIndex : Type

Indices for the preferred representatives on the CFSG list. The proof fields restrict the cyclic and alternating parameters without asserting that any candidate group is finite or simple.

• cyclic (p : ℕ) (prime_p : Nat.Prime p) : CFSGIndex
• alternating (degree : ℕ) (degree_ge_five : 5 ≤ degree) : CFSGIndex
• lie (index : ValidLieTypeIndex) : CFSGIndex
• sporadic (name : SporadicName) : CFSGIndex

@[instance_reducible]

instance TauCeti.instDecidableEqCFSGIndex : DecidableEq CFSGIndex

Equations

• TauCeti.instDecidableEqCFSGIndex = TauCeti.instDecidableEqCFSGIndex.decEq

def TauCeti.instDecidableEqCFSGIndex.decEq (x✝ x✝¹ : CFSGIndex) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.cyclic p prime_p) (TauCeti.CFSGIndex.alternating degree degree_ge_five) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.cyclic p prime_p) (TauCeti.CFSGIndex.lie index) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.cyclic p prime_p) (TauCeti.CFSGIndex.sporadic name) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.alternating degree degree_ge_five) (TauCeti.CFSGIndex.cyclic p prime_p) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.alternating degree degree_ge_five) (TauCeti.CFSGIndex.lie index) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.alternating degree degree_ge_five) (TauCeti.CFSGIndex.sporadic name) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.lie index) (TauCeti.CFSGIndex.cyclic p prime_p) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.lie index) (TauCeti.CFSGIndex.alternating degree degree_ge_five) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.lie a) (TauCeti.CFSGIndex.lie b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.lie index) (TauCeti.CFSGIndex.sporadic name) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.sporadic name) (TauCeti.CFSGIndex.cyclic p prime_p) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.sporadic name) (TauCeti.CFSGIndex.alternating degree degree_ge_five) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.sporadic name) (TauCeti.CFSGIndex.lie index) = isFalse ⋯
• TauCeti.instDecidableEqCFSGIndex.decEq (TauCeti.CFSGIndex.sporadic a) (TauCeti.CFSGIndex.sporadic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯