The Frobenius-fixed points of the full-weight type-C carrier

TauCeti.SpStd.groupScheme n is the explicit full-weight Chevalley carrier of type C_(n+1), and TauCeti.SpStd.frobenius n p k A is the p ^ k-power Frobenius endomorphism of its point group over a value ring A of exponential characteristic p. This file names an isomorphism onto the group that endomorphism fixes:

G(𝔽) ≃* G(A)^F,        𝔽 = frobeniusFixedSubring A p k.

For p prime, 0 < k and A an algebraic closure of ZMod p this reads G(𝔽_q) ≃* G(A)^F with q = p ^ k.

What the isomorphism adds over TauCeti.SpStd.map_subtype_fixedSubgroup_frobenius_eq, which is already available, is a map. That lemma equates two subgroups of the ambient GL_(2n+2)(A): the image of the fixed subgroup and the image of the points over 𝔽. It names no map between G(𝔽) and G(A)^F themselves, and a consumer that wants to read a property of G(A)^F off the same property of G(𝔽) needs one. Finiteness is such a property, and it is recorded here: as soon as the Frobenius-fixed subring is finite the fixed group is finite, which over a field of characteristic p holds for every nonzero exponent.

Nothing is reproved, and nothing is rebuilt. The identification already exists for the matrix points that a Hopf ideal cuts out of GLₙ, as TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsMulEquiv, and TauCeti.GeneralLinear.frobeniusFixedMulEquivOfCoeEq transports it to any carrier presenting its point group by a Hopf ideal and its Frobenius entrywise. This file feeds that transport TauCeti.SpStd.points_def and TauCeti.SpStd.coe_frobenius, exactly as GeneralLinear.IntegralPointsPresentation.map consumes TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup and TauCeti.SpStd.map_subtype_fixedSubgroup_frobenius_eq consumes TauCeti.GeneralLinear.map_hopfIdealPointsSubgroup_frobeniusFixedSubring.

Naturality on the pinned generating families is not restated: the isomorphism is the functorial point map along the inclusion of 𝔽, by TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_eq_map, so TauCeti.SpStd.map_rootSubgroupPoints and TauCeti.SpStd.map_weightTorusPoints at that inclusion already describe its action on the numbered root subgroups and on the weight torus.

Two limitations carry over from the file this one builds on. The carrier is not identified with the symplectic group scheme, so the fixed group is described as the carrier's points over the fixed subring rather than as a classical matrix group; and no statement here restricts to the elementary subgroup generated by the root subgroups. Nothing below asserts that the carrier is reductive, or that a group in sight is perfect, simple, or a named finite group of Lie type.

Main definitions

• TauCeti.SpStd.pointsMulEquivFixedSubgroupFrobenius: the isomorphism from the points of the carrier over the Frobenius-fixed subring onto the Frobenius-fixed points.

Main results

• TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius and TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_apply: the isomorphism is the entrywise inclusion of the Frobenius-fixed subring into the value ring.
• TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_symm_apply and TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_symm_apply_apply: the same read backwards, so that a Frobenius-fixed point is recovered from its inverse image entry by entry.
• TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_eq_map and TauCeti.SpStd.map_pointsMulEquivFixedSubgroupFrobenius_symm_apply: both readings again inside TauCeti.SpStd.points, where the isomorphism is the shared map along the inclusion of the Frobenius-fixed subring.
• TauCeti.SpStd.finite_fixedSubgroup_frobenius and TauCeti.SpStd.finite_fixedSubgroup_frobenius_of_charP: the fixed group is finite as soon as the Frobenius-fixed subring is, which over a field of characteristic p needs only k ≠ 0.

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 type-A counterpart is TauCeti/Algebra/Lie/SpecialLinear/StandardCarrier/FixedPoints.lean, which identifies the Frobenius-fixed points of TauCeti.SlStd with SL_(r+1) over the fixed subfield; no such identification with a classical matrix group is available here, so the fixed group is described as the carrier's points over the fixed subring instead, as in TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/GeckLattice/FixedPoints.lean, whose statement shapes and proofs this file follows. The coordinate-free form of the isomorphism, for the points of a Hopf algebra rather than for matrix points, is TauCeti.Bialgebra.frobeniusFixedPointsMulEquiv.

Roadmap

This advances the target "points over an algebraically closed field as a group, functorially in the field, so that a field endomorphism induces a group endomorphism of the points. The q-power Frobenius is the case a consumer asks for first" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, by naming an isomorphism onto the group that endomorphism fixes, from the points over the fixed subring. Its consumer is milestone L3 of TauCetiRoadmap/CFSGStatement/README.md, which takes the derived central quotient of H_d = fixedSubgroup d.steinberg. The families this isomorphism serves directly are the untwisted C_n(q) and B₂(q), whose Steinberg endomorphism is the Frobenius treated here. The Suzuki family ²B₂(2^(2m+1)) is carried by the same carrier but is not among them: its Steinberg endomorphism is the twisted one built from the special isogeny, and no isomorphism for the subgroup it fixes is established here. Reading H_d on that branch through the carrier's points awaits the group-scheme lift of the special isogeny and a twisted counterpart of the result below.

The fixed points as points over the fixed subring

noncomputable def TauCeti.SpStd.pointsMulEquivFixedSubgroupFrobenius (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] : ↥(points n ↥(frobeniusFixedSubring A p k)) ≃* ↥(fixedSubgroup (frobenius n p k A))

The Frobenius-fixed points of the full-weight type-C_(n+1) carrier are its points over the Frobenius-fixed subring, as an isomorphism between the two element types rather than as the equality of their images in GL_(2n+2)(A) recorded by TauCeti.SpStd.map_subtype_fixedSubgroup_frobenius_eq. For p prime, 0 < k and A an algebraic closure of ZMod p this reads G(𝔽_q) ≃* G(A)^F with q = p ^ k.

It is TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsMulEquiv, the same isomorphism for the matrix points cut out by a Hopf ideal, transported along TauCeti.SpStd.points_def into the named type-C API by TauCeti.GeneralLinear.frobeniusFixedMulEquivOfCoeEq; nothing is reproved. The transport consumes only that presentation of the point group and the entrywise description TauCeti.SpStd.coe_frobenius of the carrier Frobenius. TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius says that it leaves the matrices alone, so the isomorphism is the entrywise inclusion.

Equations

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

theorem TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n ↥(frobeniusFixedSubring A p k))) : ↑↑((pointsMulEquivFixedSubgroupFrobenius n p k A) g) = (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) ↑g

The isomorphism onto the Frobenius-fixed points includes the matrix entries of a point over the Frobenius-fixed subring into the value ring, and does nothing else.

Not a simp lemma: TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_eq_map and GeneralLinear.IntegralPointsPresentation.coe_map are; rewriting with both reaches this right-hand side, so simp proves this statement already.

theorem TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_apply (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n ↥(frobeniusFixedSubring A p k))) (r c : Fin (n + 1 + (n + 1))) : ↑↑↑((pointsMulEquivFixedSubgroupFrobenius n p k A) g) r c = ↑(↑↑g r c)

Entrywise, the isomorphism includes each matrix entry of a point over the Frobenius-fixed subring into the value ring.

@[simp]

theorem TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_eq_map (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (g : ↥(points n ↥(frobeniusFixedSubring A p k))) : ↑((pointsMulEquivFixedSubgroupFrobenius n p k A) g) = ((pointsPresentation n ↥(frobeniusFixedSubring A p k)).map (pointsPresentation n A) (frobeniusFixedSubring A p k).subtype) g

The isomorphism is the functorial point map along the inclusion of the Frobenius-fixed subring. This is TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius read inside points n A rather than inside GL_(2n+2)(A), which is the level at which the carrier's naturality statements TauCeti.SpStd.map_rootSubgroupPoints and TauCeti.SpStd.map_weightTorusPoints are made; through it they describe the action of the isomorphism on the numbered root subgroups and on the weight torus.

@[simp]

theorem TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_symm_apply (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (x : ↥(fixedSubgroup (frobenius n p k A))) : (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) ↑((pointsMulEquivFixedSubgroupFrobenius n p k A).symm x) = ↑↑x

The inverse of the isomorphism reads a Frobenius-fixed point as a point over the Frobenius-fixed subring: including its matrix back into the A-valued points returns the point one started from.

@[simp]

theorem TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_symm_apply_apply (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (x : ↥(fixedSubgroup (frobenius n p k A))) (r c : Fin (n + 1 + (n + 1))) : ↑(↑↑((pointsMulEquivFixedSubgroupFrobenius n p k A).symm x) r c) = ↑↑↑x r c

Entrywise, the point over the Frobenius-fixed subring produced by the inverse of the isomorphism has the entries of the Frobenius-fixed point it came from.

@[simp]

theorem TauCeti.SpStd.map_pointsMulEquivFixedSubgroupFrobenius_symm_apply (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] (x : ↥(fixedSubgroup (frobenius n p k A))) : ((pointsPresentation n ↥(frobeniusFixedSubring A p k)).map (pointsPresentation n A) (frobeniusFixedSubring A p k).subtype) ((pointsMulEquivFixedSubgroupFrobenius n p k A).symm x) = ↑x

The inverse of the isomorphism read inside points n A: the functorial point map along the inclusion of the Frobenius-fixed subring returns the Frobenius-fixed point one started from. This is the points-level form of TauCeti.SpStd.coe_pointsMulEquivFixedSubgroupFrobenius_symm_apply.

Finiteness

theorem TauCeti.SpStd.finite_fixedSubgroup_frobenius (n p k : ℕ) (A : Type v) [CommRing A] [ExpChar A p] [Finite ↥(frobeniusFixedSubring A p k)] : Finite ↥(fixedSubgroup (frobenius n p k A))

The Frobenius-fixed points of the full-weight type-C_(n+1) carrier form a finite group as soon as the Frobenius-fixed subring is finite, because they are then the points of the carrier over a finite ring, and those form a subgroup of a finite general linear group.

theorem TauCeti.SpStd.finite_fixedSubgroup_frobenius_of_charP (n p k : ℕ) (K : Type v) [Field K] [Fact (Nat.Prime p)] [CharP K p] (hk : k ≠ 0) : Finite ↥(fixedSubgroup (frobenius n p k K))

The Frobenius-fixed points of the full-weight type-C_(n+1) carrier over a field of characteristic p form a finite group, for every nonzero exponent: the Frobenius-fixed subfield is a set of roots of X ^ p ^ k - X, hence finite.

Separable closedness is not needed for finiteness, only for the count: when K is separably closed the subfield has exactly p ^ k elements by TauCeti.card_frobeniusFixedSubfield. This is the first point at which the type-C carrier produces a finite group; no order formula, perfectness or simplicity statement is claimed, and the group is not identified with Sp_(2n+2)(q), an identification of the carrier with the symplectic group scheme not being available.