The spin carrier and the candidate group of the untwisted family Bₙ(q)

The untwisted odd orthogonal family Bₙ(q) is built on the diagram Bₙ, and Tau Ceti's explicit full-weight Chevalley carrier for that diagram is TauCeti.TypeBSpinCarrier.groupScheme, the Kostant toral closure of the split spin representation inside GL_(2^n) over ℤ, whose weights span the whole character lattice of the simply connected form. This file attaches that carrier to a validated type-B index: the group of algebraic-closure-valued points of the carrier at the index's rank, its Bourbaki-numbered simple root subgroups, the reading of their root characters in the type-B root datum the index names, and the carrier's q-power Frobenius, where q is the field order the index records. The family is untwisted, so that Frobenius is its Steinberg endomorphism outright, and the candidate group of the family is the derived subgroup of the Steinberg fixed points modulo the centre of that derived subgroup,

H_d = fixedSubgroup d.steinberg,        d.Group = [H_d, H_d] / Z([H_d, H_d]).

The carrier is indexed by n in the spelling B (n + 1), so a validated index of rank r uses the carrier at TauCeti.TypeBLieIndex.carrierRank, which is r - 1. That subtraction is harmless because TauCeti.TypeBLieIndex.two_le_rank bounds the rank below by two: TauCeti.TypeBLieIndex.carrierRank_add_one recovers r, and every numbered object below is indexed by Fin d.1.rank, the upstream Bourbaki index type of the index's own Dynkin type, rather than by a node of the carrier. The two numberings agree node for node, so TauCeti.TypeBLieIndex.carrierNode is the rank identification and nothing more; that is what TauCeti.TypeBLieIndex.rootWeight_carrierNode_eq_root_simpleIndex records, reading the character of the i-th raising subgroup as the i-th simple root of the type-B root datum the index names.

The spin carrier takes no rank hypothesis beyond the one the subtype supplies, so everything below is stated for every validated type-B index, the rank-two members B₂(q) included. Those members are also served, beside the Suzuki family that shares their diagram, by the rank-two type-C carrier of TauCeti/GroupTheory/SpecificGroups/CFSG/TypeB/Two/Basic.lean, reached through TauCeti.TypeB2LieIndex. The two carriers of the B₂ diagram are identified with each other, and the spin carrier of B₂(q) with the pinned Sp₄/ℤ scheme points, in TauCeti/GroupTheory/SpecificGroups/CFSG/TypeB/Two/SpinAgreement.lean.

The spin carrier rather than the Geck carrier is used because the Geck carrier is built from the adjoint representation, so its weights span the whole character lattice exactly in the types E₈, F₄ and G₂, by TauCeti.DynkinType.span_range_geckWeight_eq_top_iff; the spin representation is what sees the spinor coset of the type-B root lattice, and its weights span the whole weight lattice, the root lattice together with that coset, by TauCeti.TypeBSpinCarrier.span_range_basisWeight_eq_top.

Nothing here asserts that the carrier is reductive, that its weight torus is maximal, that it is the spin group scheme or the pinned simply connected Chevalley--Demazure group scheme of type Bₙ, or that any group below is finite, perfect, or simple. The Steinberg endomorphism and the candidate group transfer to that pinned group scheme only along an identification of the carrier with it, once one is proved.

Main declarations

• TauCeti.TypeBLieIndex.AmbientGroup: the algebraic-closure-valued points of the full-weight type-B spin carrier at the index's rank.

• TauCeti.TypeBLieIndex.simpleRootSubgroup: its positive simple-root subgroup at a Bourbaki-numbered node, with TauCeti.TypeBLieIndex.rootWeight_carrierNode_eq_root_simpleIndex identifying the character of that subgroup with the corresponding simple root of the type-B root datum.

• TauCeti.TypeBLieIndex.frobenius, TauCeti.TypeBLieIndex.coe_frobenius_apply and TauCeti.TypeBLieIndex.frobenius_simpleRootSubgroup: the carrier's q-power Frobenius, its entrywise description, and its simple-root-subgroup action formula Frob_q (x_i(u)) = x_i(u ^ q).

• TauCeti.TypeBLieIndex.frobenius_weightTorusPoints: its action on the split spin weight torus, raising every coordinate to the q-th power.

• TauCeti.TypeBLieIndex.mem_fixedSubgroup_frobenius_iff: its fixed points are the carrier points whose matrix entries all lie in the field of q elements inside the closure.

• TauCeti.TypeBLieIndex.steinberg, TauCeti.TypeBLieIndex.steinberg_simpleRootSubgroup and TauCeti.TypeBLieIndex.mem_fixedSubgroup_steinberg_iff: the Steinberg endomorphism of the untwisted family, its simple-root-subgroup action formula, and the description of the group it fixes.

• TauCeti.TypeBLieIndex.FixedPoints and TauCeti.TypeBLieIndex.Group: that fixed group and the candidate group of Bₙ(q), its derived central quotient.

• TauCeti.TypeBLieIndex.primeFrobenius, with TauCeti.TypeBLieIndex.primeFrobenius_simpleRootSubgroup, TauCeti.TypeBLieIndex.primeFrobenius_weightTorusPoints and TauCeti.TypeBLieIndex.frobenius_eq_primeFrobenius_pow: the prime-field Frobenius, its pinned equation Frob_p (x_i(u)) = x_i(u ^ p), its action on the split spin weight torus, and the q-power Frobenius as its e-th power.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II, for the spin representation the carrier is built from.
• 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, for the entrywise Frobenius action.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate II, for the numbering of the Bₙ diagram that the root subgroups below are indexed by.

The carrier rank and the node correspondence

def TauCeti.TypeBLieIndex.carrierRank (d : TypeBLieIndex) : ℕ

The rank parameter of the spin carrier serving a validated type-B index. TauCeti.TypeBSpinCarrier.groupScheme n is the carrier of type B (n + 1), so the carrier serving an index of rank r is the one at r - 1. The subtraction never truncates, r being at least two by TauCeti.TypeBLieIndex.two_le_rank; TauCeti.TypeBLieIndex.carrierRank_add_one is the identification that recovers r.

Equations

• d.carrierRank = (↑d).rank - 1

@[simp]

theorem TauCeti.TypeBLieIndex.carrierRank_add_one (d : TypeBLieIndex) : d.carrierRank + 1 = (↑d).rank

The carrier rank of a validated type-B index is one less than its rank.

@[reducible, inline]

abbrev TauCeti.TypeBLieIndex.carrierNode (d : TypeBLieIndex) (i : Fin (↑d).rank) : Fin (d.carrierRank + 1)

The carrier node numbered by a Bourbaki node of the index's diagram. This is the rank identification and nothing else: the spin carrier at TauCeti.TypeBLieIndex.carrierRank numbers its generators by the Bourbaki numbering of the type-B diagram that the index names, node for node.

Equations

• d.carrierNode i = Fin.cast ⋯ i

theorem TauCeti.TypeBLieIndex.cartanMatrix_B_carrierNode (d : TypeBLieIndex) (i j : Fin (↑d).rank) : CartanMatrix.B (d.carrierRank + 1) (d.carrierNode i) (d.carrierNode j) = CartanMatrix.B (↑d).rank i j

The node correspondence transports the type-B Cartan matrix. The entry at a pair of carrier nodes is the entry at the pair of Bourbaki nodes they number: carrierNode moves no node value, only the rank its index type is built on, and TauCeti.TypeBLieIndex.carrierRank_add_one identifies the two ranks.

The ambient group and its simple root subgroups

@[reducible, inline]

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

The ambient group this file attaches to a validated type-B index: the points of the explicit full-weight type-B spin Chevalley carrier at the index's rank, over the algebraic closure of its prime field. It is infinite. No finiteness, reductivity, pinning or maximality statement is attached to it. In rank two, TauCeti.TypeB2LieIndex.spinEquivPinned identifies it with the points of the pinned Sp₄/ℤ group scheme; in higher rank it is not claimed to be the points of the pinned simply connected group scheme of type Bₙ, no such identification being proved.

Equations

• d.AmbientGroup = ↥(TauCeti.TypeBSpinCarrier.points d.carrierRank (↑d).Closure)

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

The positive simple-root subgroup at the Bourbaki-numbered node i of the type-B diagram. It is the carrier's numbered raising subgroup at the node that carrierNode names.

Equations

• d.simpleRootSubgroup i = TauCeti.TypeBSpinCarrier.rootSubgroupPoints d.carrierRank (Sum.inl (d.carrierNode i)) (↑d).Closure

theorem TauCeti.TypeBLieIndex.simpleRootSubgroup_def (d : TypeBLieIndex) (i : Fin (↑d).rank) : d.simpleRootSubgroup i = TypeBSpinCarrier.rootSubgroupPoints d.carrierRank (Sum.inl (d.carrierNode i)) (↑d).Closure

The simple-root subgroup is the carrier's numbered raising subgroup at the corresponding carrier node.

theorem TauCeti.TypeBLieIndex.rootWeight_carrierNode_eq_root_simpleIndex (d : TypeBLieIndex) (i j : Fin (↑d).rank) : TypeBSpinCarrier.rootWeight d.carrierRank (Sum.inl (d.carrierNode i)) (d.carrierNode j) = ((↑d).dynkinType.simplyConnectedRootDatum ⋯).root ((↑d).dynkinType.simpleIndex ⋯ i) j

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

The character itself is TauCeti.TypeBSpinCarrier.rootWeight, which TauCeti.TypeBSpinCarrier.weightTorusPoints_conj_rootSubgroupPoints exhibits as the one conjugation by the carrier's split torus rescales the parameter by.

The Frobenius endomorphism

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

The q-power Frobenius of the spin carrier attached to a validated type-B index, where q is the field order recorded by the index. It is the endomorphism of the point group raising every matrix entry to the q-th power, and it is the Steinberg endomorphism of the family, by TauCeti.TypeBLieIndex.steinberg_def.

Equations

• d.frobenius = TauCeti.TypeBSpinCarrier.frobenius d.carrierRank (↑d).characteristic (↑d).fieldExponent (↑d).Closure

theorem TauCeti.TypeBLieIndex.frobenius_def (d : TypeBLieIndex) : d.frobenius = TypeBSpinCarrier.frobenius d.carrierRank (↑d).characteristic (↑d).fieldExponent (↑d).Closure

The Frobenius is the spin carrier's Frobenius at the characteristic and field exponent recorded by the index.

@[simp]

theorem TauCeti.TypeBLieIndex.coe_frobenius_apply (d : TypeBLieIndex) (g : d.AmbientGroup) (r c : Fin (TypeBSpinCarrier.dimension d.carrierRank)) : ↑↑(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.TypeBLieIndex.frobenius_simpleRootSubgroup (d : TypeBLieIndex) (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 fixes the Bourbaki numbering of a simple-root subgroup and raises its parameter to the q-th power, that is, Frob_q (x_i(u)) = x_i(u ^ q).

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

The prime-field Frobenius of the spin carrier attached to a validated type-B index, the p-power map for p the defining characteristic. The q-power Frobenius is its e-th power, for e the field exponent the index records, by frobenius_eq_primeFrobenius_pow.

Equations

• d.primeFrobenius = TauCeti.TypeBSpinCarrier.frobenius d.carrierRank (↑d).characteristic 1 (↑d).Closure

theorem TauCeti.TypeBLieIndex.primeFrobenius_def (d : TypeBLieIndex) : d.primeFrobenius = TypeBSpinCarrier.frobenius d.carrierRank (↑d).characteristic 1 (↑d).Closure

The prime-field Frobenius is the spin carrier's Frobenius at exponent one.

@[simp]

theorem TauCeti.TypeBLieIndex.coe_primeFrobenius_apply (d : TypeBLieIndex) (g : d.AmbientGroup) (r c : Fin (TypeBSpinCarrier.dimension d.carrierRank)) : ↑↑(d.primeFrobenius g) r c = ↑↑g r c ^ (↑d).characteristic

The prime-field Frobenius acts on the ambient group by raising every matrix entry to the p-th power, for p the defining characteristic.

@[simp]

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

The prime-field Frobenius fixes the Bourbaki numbering of a simple-root subgroup and raises its parameter to the p-th power, that is, Frob_p (x_i(u)) = x_i(u ^ p).

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

The q-power Frobenius is the e-th power of the prime-field Frobenius, for e the field exponent the index records.

@[simp]

theorem TauCeti.TypeBLieIndex.primeFrobenius_weightTorusPoints (d : TypeBLieIndex) (s : Fin (d.carrierRank + 1) → (↑d).Closureˣ) : d.primeFrobenius ((TypeBSpinCarrier.weightTorusPoints d.carrierRank (↑d).Closure) s) = (TypeBSpinCarrier.weightTorusPoints d.carrierRank (↑d).Closure) (s ^ (↑d).characteristic)

The prime-field Frobenius raises every coordinate of the split spin weight torus to the p-th power.

@[simp]

theorem TauCeti.TypeBLieIndex.frobenius_weightTorusPoints (d : TypeBLieIndex) (s : Fin (d.carrierRank + 1) → (↑d).Closureˣ) : d.frobenius ((TypeBSpinCarrier.weightTorusPoints d.carrierRank (↑d).Closure) s) = (TypeBSpinCarrier.weightTorusPoints d.carrierRank (↑d).Closure) (s ^ (↑d).fieldOrder)

The Frobenius raises every coordinate of the split spin weight torus to the q-th power.

theorem TauCeti.TypeBLieIndex.mem_fixedSubgroup_frobenius_iff (d : TypeBLieIndex) (g : d.AmbientGroup) : g ∈ fixedSubgroup d.frobenius ↔ ∀ (r c : Fin (TypeBSpinCarrier.dimension d.carrierRank)), ↑↑g r c ∈ (↑d).fixedField

A point of the ambient group is fixed by the Frobenius exactly when all of its matrix entries lie in the field of definition. Writing 𝔽_q for TauCeti.ValidLieTypeIndex.fixedField, the copy of the field of q elements inside the algebraic closure, the Frobenius fixed points are the points of the spin carrier whose entries lie in 𝔽_q.

The Steinberg endomorphism

noncomputable def TauCeti.TypeBLieIndex.steinberg (d : TypeBLieIndex) : d.AmbientGroup →* d.AmbientGroup

The Steinberg endomorphism of a validated type-B index: the q-power Frobenius of the ambient group, q being the field order the index records. The family is untwisted, so no diagram automorphism and no half-Frobenius enters; TauCeti.TypeBLieIndex.diagramPerm_eq_one records that the diagram permutation attached to the index is trivial.

It is formed on the spin carrier. In rank two, TauCeti.TypeB2LieIndex.spinEquivPinned_steinberg shows that the identification of that carrier with the pinned Sp₄/ℤ points intertwines it with the pinned q-power Frobenius; in higher rank the carrier is not identified with the pinned simply connected group scheme of type Bₙ, and the map transfers to that pinned group only along such an identification, and not before.

Equations

• d.steinberg = d.frobenius

theorem TauCeti.TypeBLieIndex.steinberg_def (d : TypeBLieIndex) : d.steinberg = d.frobenius

The Steinberg map of a type-B index is the carrier's Frobenius.

@[simp]

theorem TauCeti.TypeBLieIndex.steinberg_simpleRootSubgroup (d : TypeBLieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.steinberg ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup i) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ (↑d).fieldOrder))

The Steinberg map fixes the Bourbaki numbering of a simple-root subgroup and raises its parameter to the q-th power, that is, Frob_q (x_i(u)) = x_i(u ^ q), the simple-root-subgroup action formula of an untwisted Steinberg endomorphism.

theorem TauCeti.TypeBLieIndex.mem_fixedSubgroup_steinberg_iff (d : TypeBLieIndex) (g : d.AmbientGroup) : g ∈ fixedSubgroup d.steinberg ↔ ∀ (r c : Fin (TypeBSpinCarrier.dimension d.carrierRank)), ↑↑g r c ∈ (↑d).fixedField

A point of the ambient group is fixed by the Steinberg map exactly when all of its matrix entries lie in the field of definition, so the fixed group H_d of the family is the group of points of the spin carrier whose entries lie in 𝔽_q.

The finite-group candidate

@[reducible, inline]

abbrev TauCeti.TypeBLieIndex.FixedPoints (d : TypeBLieIndex) : Type

The fixed subgroup of the Steinberg endomorphism attached to a type-B index.

Equations

• d.FixedPoints = ↥(TauCeti.fixedSubgroup d.steinberg)

@[reducible, inline]

abbrev TauCeti.TypeBLieIndex.Group (d : TypeBLieIndex) : Type

The finite-simple-group candidate attached to a type-B index: the derived subgroup of the Steinberg fixed points, modulo the centre of that derived subgroup. No finiteness or simplicity assertion is part of this definition, nor any identification of the spin carrier with the pinned simply connected group scheme of type Bₙ.

Equations

• d.Group = TauCeti.FixedPointCandidate d.steinberg