The Frobenius on the matrix points of a closed subgroup scheme of GLₙ

Let A be a commutative ring of exponential characteristic p. On the A-valued points of an integral Hopf algebra the p ^ k-power Frobenius acts by TauCeti.Bialgebra.iterateFrobeniusPoints, raising every value of a point to the p ^ k-th power. This file reads that endomorphism in matrix coordinates, for the general linear group and for the closed subgroup schemes of it cut out by a Hopf ideal over ℤ.

Three things are proved. Under the identification of the convolution points of TauCeti.GeneralLinear.coordinateHopfAlgebra with GLₙ(A), the Frobenius on points is the entrywise p ^ k-power map. That map preserves the matrix subgroup TauCeti.GeneralLinear.hopfIdealPointsSubgroup cut out by a Hopf ideal, so it restricts to a group endomorphism of the points of the closed subgroup scheme, with the expected iteration laws. And the points fixed by that restriction are exactly the points of the same subgroup scheme valued in the Frobenius-fixed subring of A, both as an equality of subgroups of GLₙ(A) and as an isomorphism of groups.

For p prime, 0 < k, A an algebraic closure of ZMod p and q = p ^ k, the fixed subring is the field of q elements inside A, so the last statement is G(𝔽_q) ≃* G(A)^F for a closed subgroup scheme G of GLₙ defined over ℤ. Nothing here asserts that either side is finite, and no algebraic closedness, field, or finite-type hypothesis is used.

The purely matrix-level description of the invertible matrices fixed by the entrywise Frobenius, which needs no coordinate ring, is TauCeti/LinearAlgebra/Matrix/GeneralLinearGroup/Frobenius.lean.

Main definitions

• TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints: the p ^ k-power Frobenius as a group endomorphism of the matrix points cut out by a Hopf ideal.
• TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsInclusion: the entrywise inclusion of the matrix points valued in the Frobenius-fixed subring.
• TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsMulEquiv: the resulting isomorphism onto the Frobenius-fixed points.
• TauCeti.GeneralLinear.frobeniusFixedMulEquivOfCoeEq: that isomorphism transported to a named carrier, from a presentation of its point group by a Hopf ideal and an entrywise description of its Frobenius.

Main results

• TauCeti.GeneralLinear.pointToGeneralLinear_iterateFrobeniusPoints and TauCeti.GeneralLinear.pointsMulEquiv_iterateFrobeniusPoints: the Frobenius on general-linear points is the entrywise Frobenius on matrices.
• TauCeti.GeneralLinear.map_fixedSubgroup_iterateFrobeniusPoints: the point equivalence carries the Frobenius-fixed points onto the entrywise-fixed matrices.
• TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints_eq_self_iff: a matrix point of the closed subgroup scheme is Frobenius-fixed exactly when all of its entries are.
• TauCeti.GeneralLinear.map_subtype_fixedSubgroup_iterateFrobeniusHopfIdealPoints: the fixed points of the restricted Frobenius, read in GLₙ(A).
• TauCeti.GeneralLinear.map_hopfIdealPointsSubgroup_frobeniusFixedSubring and TauCeti.GeneralLinear.range_frobeniusFixedHopfIdealPointsInclusion: those fixed points are the points of the same subgroup scheme over the Frobenius-fixed subring.
• TauCeti.GeneralLinear.coe_frobeniusFixedMulEquivOfCoeEq and TauCeti.GeneralLinear.coe_frobeniusFixedMulEquivOfCoeEq_symm_apply: the transported isomorphism is the entrywise inclusion of the Frobenius-fixed subring, read in both directions.

Coordinate-free constructions and matrix carriers

TauCeti/Algebra/AlgebraicGroup/Frobenius/Points.lean constructs the Frobenius on convolution points, and TauCeti/Algebra/AlgebraicGroup/Frobenius/FixedPoints.lean identifies its fixed points with points over the Frobenius-fixed subring. Here the general-linear point equivalence reads those constructions entrywise and restricts them to the points cut out by a Hopf ideal. In particular, the toral closure TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme is presented by a Hopf ideal in the coordinate algebra of GLₙ over ℤ, so it is an instance of the subgroup schemes treated here.

References

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

@[simp]

theorem TauCeti.GeneralLinear.pointToGeneralLinear_iterateFrobeniusPoints (n p k : ℕ) {A : Type w} [CommRing A] [ExpChar A p] (f : WithConv (↑(coordinateHopfAlgebra ℤ n) →ₐ[ℤ] A)) : pointToGeneralLinear n ((Bialgebra.iterateFrobeniusPoints p k) f) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) (pointToGeneralLinear n f)

Reading the p ^ k-power Frobenius of a point as an invertible matrix gives the entrywise p ^ k-power map.

theorem TauCeti.GeneralLinear.pointsMulEquiv_iterateFrobeniusPoints (n p k : ℕ) {A : Type w} [CommRing A] [ExpChar A p] (f : WithConv (↑(coordinateHopfAlgebra ℤ n) →ₐ[ℤ] A)) : (pointsMulEquiv n) ((Bialgebra.iterateFrobeniusPoints p k) f) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ((pointsMulEquiv n) f)

The p ^ k-power Frobenius on the points of the general linear coordinate Hopf algebra is the entrywise p ^ k-power map on invertible matrices.

Not a simp lemma, matching TauCeti.GeneralLinear.pointsMulEquiv_mapValue: pointsMulEquiv_apply already rewrites the group equivalence to pointToGeneralLinear, so the simp-normal form of this statement is pointToGeneralLinear_iterateFrobeniusPoints.

theorem TauCeti.GeneralLinear.pointsMulEquiv_comp_iterateFrobeniusPoints (n p k : ℕ) {A : Type w} [CommRing A] [ExpChar A p] : (pointsMulEquiv n).toMonoidHom.comp (Bialgebra.iterateFrobeniusPoints p k) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)).comp (pointsMulEquiv n).toMonoidHom

The point equivalence intertwines the Frobenius on points with the entrywise Frobenius.

theorem TauCeti.GeneralLinear.map_fixedSubgroup_iterateFrobeniusPoints (n p k : ℕ) {A : Type w} [CommRing A] [ExpChar A p] : Subgroup.map (pointsMulEquiv n).toMonoidHom (fixedSubgroup (Bialgebra.iterateFrobeniusPoints p k)) = fixedSubgroup (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k))

The point equivalence carries the Frobenius-fixed points of the general linear coordinate Hopf algebra onto the invertible matrices fixed entrywise by the Frobenius.

noncomputable def TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) (A : Type w) [CommRing A] [ExpChar A p] : ↥(hopfIdealPointsSubgroup n I A) →* ↥(hopfIdealPointsSubgroup n I A)

The p ^ k-power Frobenius as a group endomorphism of the matrix points cut out by a Hopf ideal over ℤ.

For p prime, 0 < k, A an algebraic closure of ZMod p and a Hopf ideal presenting a Chevalley carrier, this is the untwisted Steinberg endomorphism of that carrier; for k = 0, or in characteristic zero, it is the identity. Unlike TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup along a general value-algebra homomorphism, it is an endomorphism, so it has a fixed subgroup and an iteration law.

Equations

• TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints n p k I A = TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup n I (iterateFrobenius A p k).toIntAlgHom

@[simp]

theorem TauCeti.GeneralLinear.coe_iterateFrobeniusHopfIdealPoints (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (g : ↥(hopfIdealPointsSubgroup n I A)) : ↑((iterateFrobeniusHopfIdealPoints n p k I A) g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g

The Frobenius endomorphism of the matrix points cut out by a Hopf ideal acts by the entrywise Frobenius.

theorem TauCeti.GeneralLinear.coe_iterateFrobeniusHopfIdealPoints_apply (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (g : ↥(hopfIdealPointsSubgroup n I A)) (i j : Fin n) : ↑↑((iterateFrobeniusHopfIdealPoints n p k I A) g) i j = ↑↑g i j ^ p ^ k

Entrywise, the Frobenius endomorphism of the matrix points cut out by a Hopf ideal raises each entry to the p ^ k-th power.

@[simp]

theorem TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints_eq_self_iff (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (x : ↥(hopfIdealPointsSubgroup n I A)) : (iterateFrobeniusHopfIdealPoints n p k I A) x = x ↔ ∀ (i j : Fin n), ↑↑x i j ∈ frobeniusFixedSubring A p k

A matrix point of a closed subgroup scheme is fixed by the Frobenius endomorphism exactly when every one of its entries lies in the Frobenius-fixed subring. The generic equality-locus simplifier rewrites membership in fixedSubgroup (iterateFrobeniusHopfIdealPoints n p k I A) to the equation below, so this is the membership criterion for the group of rational points.

@[simp]

theorem TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints_zero (n p : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] : iterateFrobeniusHopfIdealPoints n p 0 I A = MonoidHom.id ↥(hopfIdealPointsSubgroup n I A)

The zeroth Frobenius iterate is the identity on the matrix points cut out by a Hopf ideal.

theorem TauCeti.GeneralLinear.iterateFrobeniusHopfIdealPoints_add (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (m : ℕ) : iterateFrobeniusHopfIdealPoints n p (k + m) I A = (iterateFrobeniusHopfIdealPoints n p k I A).comp (iterateFrobeniusHopfIdealPoints n p m I A)

Frobenius iterates add under composition on the matrix points cut out by a Hopf ideal.

theorem TauCeti.GeneralLinear.map_subtype_fixedSubgroup_iterateFrobeniusHopfIdealPoints (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] : Subgroup.map (hopfIdealPointsSubgroup n I A).subtype (fixedSubgroup (iterateFrobeniusHopfIdealPoints n p k I A)) = hopfIdealPointsSubgroup n I A ⊓ fixedSubgroup (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k))

The points of a closed subgroup scheme fixed by the Frobenius, read as a subgroup of GLₙ(A), are the points of that subgroup scheme that the entrywise Frobenius fixes.

theorem TauCeti.GeneralLinear.map_hopfIdealPointsSubgroup_frobeniusFixedSubring (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] : Subgroup.map (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) (hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k)) = hopfIdealPointsSubgroup n I A ⊓ fixedSubgroup (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k))

The points of a closed subgroup scheme of GLₙ over ℤ valued in the Frobenius-fixed subring of A are exactly the A-valued points of that subgroup scheme fixed by the entrywise p ^ k-power Frobenius.

For p prime, 0 < k, A an algebraic closure of ZMod p and q = p ^ k this is G(𝔽_q) = G(A)^F, the description of the rational points of a group of Lie type as the fixed points of a Frobenius endomorphism.

noncomputable def TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsInclusion (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) (A : Type w) [CommRing A] [ExpChar A p] : ↥(hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k)) →* ↥(hopfIdealPointsSubgroup n I A)

The entrywise inclusion of the matrix points of a closed subgroup scheme valued in the Frobenius-fixed subring of A into its A-valued matrix points. In the motivating case this is G(𝔽_q) → G(A).

Equations

• TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsInclusion n p k I A = TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup n I (TauCeti.frobeniusFixedSubring A p k).subtype.toIntAlgHom

@[simp]

theorem TauCeti.GeneralLinear.coe_frobeniusFixedHopfIdealPointsInclusion (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (g : ↥(hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k))) : ↑((frobeniusFixedHopfIdealPointsInclusion n p k I A) g) = (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) ↑g

The inclusion of the rational points reads each entry of a matrix over the Frobenius-fixed subring as an element of A.

theorem TauCeti.GeneralLinear.coe_frobeniusFixedHopfIdealPointsInclusion_apply (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (g : ↥(hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k))) (i j : Fin n) : ↑↑((frobeniusFixedHopfIdealPointsInclusion n p k I A) g) i j = ↑(↑↑g i j)

Entrywise, the inclusion of the rational points is the inclusion of the Frobenius-fixed subring on each entry.

theorem TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsInclusion_injective (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] : Function.Injective ⇑(frobeniusFixedHopfIdealPointsInclusion n p k I A)

Reading a matrix point over the Frobenius-fixed subring as one over A loses no information.

theorem TauCeti.GeneralLinear.range_frobeniusFixedHopfIdealPointsInclusion (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] : (frobeniusFixedHopfIdealPointsInclusion n p k I A).range = fixedSubgroup (iterateFrobeniusHopfIdealPoints n p k I A)

The rational points of a closed subgroup scheme are exactly the points fixed by its Frobenius endomorphism. This is TauCeti.GeneralLinear.map_hopfIdealPointsSubgroup_frobeniusFixedSubring read inside the point group of the subgroup scheme rather than inside GLₙ(A).

noncomputable def TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsMulEquiv (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) (A : Type w) [CommRing A] [ExpChar A p] : ↥(hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k)) ≃* ↥(fixedSubgroup (iterateFrobeniusHopfIdealPoints n p k I A))

The rational points of a closed subgroup scheme of GLₙ are the Frobenius-fixed points. For p prime, 0 < k, A an algebraic closure of ZMod p and q = p ^ k this is the isomorphism G(𝔽_q) ≃* G(A)^F identifying the rational points of a group of Lie type with the fixed points of its Frobenius.

Equations

• TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsMulEquiv n p k I A = (MonoidHom.ofInjective ⋯).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem TauCeti.GeneralLinear.coe_frobeniusFixedHopfIdealPointsMulEquiv (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (g : ↥(hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k))) : ↑((frobeniusFixedHopfIdealPointsMulEquiv n p k I A) g) = (frobeniusFixedHopfIdealPointsInclusion n p k I A) g

The isomorphism onto the Frobenius-fixed points is the inclusion of the rational points.

@[simp]

theorem TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsInclusion_frobeniusFixedHopfIdealPointsMulEquiv_symm_apply (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (x : ↥(fixedSubgroup (iterateFrobeniusHopfIdealPoints n p k I A))) : (frobeniusFixedHopfIdealPointsInclusion n p k I A) ((frobeniusFixedHopfIdealPointsMulEquiv n p k I A).symm x) = ↑x

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

@[simp]

theorem TauCeti.GeneralLinear.coe_frobeniusFixedHopfIdealPointsMulEquiv_symm_apply_apply (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) {A : Type w} [CommRing A] [ExpChar A p] (x : ↥(fixedSubgroup (iterateFrobeniusHopfIdealPoints n p k I A))) (i j : Fin n) : ↑(↑↑((frobeniusFixedHopfIdealPointsMulEquiv n p k I A).symm x) i j) = ↑↑↑x i j

Entrywise form: the entries of the matrix over the Frobenius-fixed subring produced by the inverse of the isomorphism are the entries of the Frobenius-fixed point it came from.

noncomputable def TauCeti.GeneralLinear.frobeniusFixedMulEquivOfCoeEq (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) (A : Type w) [CommRing A] [ExpChar A p] {P : Subgroup (GL (Fin n) A)} {Q : Subgroup (GL (Fin n) ↥(frobeniusFixedSubring A p k))} (F : ↥P →* ↥P) (hP : P = hopfIdealPointsSubgroup n I A) (hQ : Q = hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k)) (hF : ∀ (g : ↥P), ↑(F g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g) : ↥Q ≃* ↥(fixedSubgroup F)

The rational points of a named carrier are its Frobenius-fixed points, for any carrier whose point group is presented by a Hopf ideal and whose Frobenius acts entrywise.

This is TauCeti.GeneralLinear.frobeniusFixedHopfIdealPointsMulEquiv transported along the two presentations hP and hQ. A carrier supplies them, together with the entrywise description hF of its own Frobenius, and reads off the isomorphism G(𝔽) ≃* G(A)^F in its own API without reproving anything; TauCeti.GeneralLinear.coe_frobeniusFixedMulEquivOfCoeEq says that the transport changes no matrix. It is the MulEquiv counterpart of TauCeti.map_subtype_fixedSubgroup_of_coe_eq, which describes the same fixed points as a subgroup of GLₙ(A) rather than as a group in its own right.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.coe_frobeniusFixedMulEquivOfCoeEq (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) (A : Type w) [CommRing A] [ExpChar A p] {P : Subgroup (GL (Fin n) A)} {Q : Subgroup (GL (Fin n) ↥(frobeniusFixedSubring A p k))} (F : ↥P →* ↥P) (hP : P = hopfIdealPointsSubgroup n I A) (hQ : Q = hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k)) (hF : ∀ (g : ↥P), ↑(F g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g) (g : ↥Q) : ↑↑((frobeniusFixedMulEquivOfCoeEq n p k I A F hP hQ hF) g) = (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) ↑g

The transported 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.

@[simp]

theorem TauCeti.GeneralLinear.coe_frobeniusFixedMulEquivOfCoeEq_symm_apply (n p k : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) (A : Type w) [CommRing A] [ExpChar A p] {P : Subgroup (GL (Fin n) A)} {Q : Subgroup (GL (Fin n) ↥(frobeniusFixedSubring A p k))} (F : ↥P →* ↥P) (hP : P = hopfIdealPointsSubgroup n I A) (hQ : Q = hopfIdealPointsSubgroup n I ↥(frobeniusFixedSubring A p k)) (hF : ∀ (g : ↥P), ↑(F g) = (Matrix.GeneralLinearGroup.map (iterateFrobenius A p k)) ↑g) (x : ↥(fixedSubgroup F)) : (Matrix.GeneralLinearGroup.map (frobeniusFixedSubring A p k).subtype) ↑((frobeniusFixedMulEquivOfCoeEq n p k I A F hP hQ hF).symm x) = ↑↑x

The inverse of the transported 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.