Frobenius on the full-weight type-B spin carrier

TauCeti.TypeBSpinCarrier.groupScheme n is the explicit full-weight Chevalley carrier of type Bₙ₊₁, cut out inside GL_(2^(n+1)) over ℤ by the split spin representation and its exterior coordinate lattice. For a commutative value ring A of exponential characteristic p, this file equips its point group TauCeti.TypeBSpinCarrier.points n A with the p ^ k-power Frobenius endomorphism.

The endomorphism raises every matrix entry to its p ^ k-th power. In particular it satisfies the pinned root-subgroup equation

F (x_i(u)) = x_i(u ^ (p ^ k))

for every Bourbaki-numbered raising or lowering generator, and it raises every coordinate of the split spin weight torus by the same exponent. Its fixed points are exactly the points of the same carrier over the Frobenius-fixed subring of A.

The construction uses the carrier's functorial point map at the iterated Frobenius of the value ring. Nothing asserts that the carrier is reductive, that it is the spin group scheme, or that any fixed-point group is finite or simple.

Main declarations

• TauCeti.TypeBSpinCarrier.frobenius: the p ^ k-power Frobenius endomorphism of the type-Bₙ₊₁ spin carrier's point group.
• TauCeti.TypeBSpinCarrier.frobenius_rootSubgroupPoints and TauCeti.TypeBSpinCarrier.frobenius_weightTorusPoints: the equations on the numbered root subgroups and split weight torus.
• TauCeti.TypeBSpinCarrier.frobenius_zero, TauCeti.TypeBSpinCarrier.frobenius_add and TauCeti.TypeBSpinCarrier.frobenius_pow: the iteration laws.
• TauCeti.TypeBSpinCarrier.frobenius_eq_self_iff: the coefficientwise fixed-point criterion.
• TauCeti.TypeBSpinCarrier.map_subtype_fixedSubgroup_frobenius_eq: the fixed points are the carrier's points over the Frobenius-fixed subring.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

The organization follows the carrier specializations TauCeti.Algebra.Lie.E6.Minuscule.Frobenius and TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.Frobenius.

noncomputable def TauCeti.TypeBSpinCarrier.frobenius (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : ↥(points n A) →* ↥(points n A)

The p ^ k-power Frobenius endomorphism of the full-weight type-Bₙ₊₁ spin carrier.

For p prime, 0 < k, and A an algebraic closure of ZMod p, this is intended to supply the Frobenius component in a future construction of the Bₙ₊₁(p ^ k) Steinberg map.

Equations

• TauCeti.TypeBSpinCarrier.frobenius n p k A = (TauCeti.TypeBSpinCarrier.pointsPresentation n A).map (TauCeti.TypeBSpinCarrier.pointsPresentation n A) (iterateFrobenius A p k)

theorem TauCeti.TypeBSpinCarrier.coe_frobenius (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n A)) : ↑((frobenius n p k A) g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g

The Frobenius endomorphism of the type-Bₙ₊₁ spin carrier acts by entrywise Frobenius.

This is not a simp lemma because coe_frobenius_apply is the coefficient-level normal form.

@[simp]

theorem TauCeti.TypeBSpinCarrier.coe_frobenius_apply (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n A)) (r c : Fin (dimension n)) : ↑↑((frobenius n p k A) g) r c = ↑↑g r c ^ p ^ k

Entrywise, the Frobenius endomorphism raises each matrix coefficient to its p ^ k-th power.

@[simp]

theorem TauCeti.TypeBSpinCarrier.frobenius_rootSubgroupPoints (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (i : Fin (n + 1) ⊕ Fin (n + 1)) (u : Multiplicative A) : (frobenius n p k A) ((rootSubgroupPoints n i A) u) = (rootSubgroupPoints n i A) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ p ^ k))

Frobenius raises the parameter of a numbered type-Bₙ₊₁ root subgroup to its p ^ k-th power on both the raising and lowering generators.

@[simp]

theorem TauCeti.TypeBSpinCarrier.frobenius_weightTorusPoints (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (s : Fin (n + 1) → Aˣ) : (frobenius n p k A) ((weightTorusPoints n A) s) = (weightTorusPoints n A) (s ^ p ^ k)

Frobenius raises every coordinate of the split spin weight torus to its p ^ k-th power.

@[simp]

theorem TauCeti.TypeBSpinCarrier.frobenius_zero (n p : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : frobenius n p 0 A = MonoidHom.id ↥(points n A)

The zeroth Frobenius iterate is the identity on the type-Bₙ₊₁ spin carrier's point group.

theorem TauCeti.TypeBSpinCarrier.frobenius_add (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) : frobenius n p (k + m) A = (frobenius n p k A).comp (frobenius n p m A)

Frobenius iterates add under composition on the type-Bₙ₊₁ spin carrier's point group.

theorem TauCeti.TypeBSpinCarrier.frobenius_pow (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (m : ℕ) : (have this := frobenius n p k A; this) ^ m = frobenius n p (k * m) A

Frobenius exponents multiply under taking powers: the m-th power of the p ^ k-power Frobenius of the type-B_(n+1) spin carrier's point group, in the endomorphism monoid of its points, is its p ^ (k * m)-power Frobenius.

@[simp]

theorem TauCeti.TypeBSpinCarrier.frobenius_eq_self_iff (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n A)) : (frobenius n p k A) g = g ↔ ∀ (r c : Fin (dimension n)), ↑↑g r c ∈ frobeniusFixedSubring A p k

A type-Bₙ₊₁ spin-carrier point is fixed by Frobenius exactly when all of its matrix entries lie in the Frobenius-fixed subring.

theorem TauCeti.TypeBSpinCarrier.map_subtype_fixedSubgroup_frobenius_eq (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : Subgroup.map (points n A).subtype (fixedSubgroup (frobenius n p k A)) = Subgroup.map (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) (points n ↥(frobeniusFixedSubring A p k))

The Frobenius-fixed points of the full-weight type-Bₙ₊₁ spin carrier are its points over the Frobenius-fixed subring. Interpreting this as a statement about a finite group of type Bₙ₊₁ will require the future identification of this carrier with the corresponding spin group scheme.