Frobenius-fixed points are the points over the fixed subring

Let H be a Hopf algebra over ℤ and let A be a commutative ring of exponential characteristic p. The p ^ n-power Frobenius acts on the convolution group of A-valued points of H by TauCeti.Bialgebra.iterateFrobeniusPoints, and a point is fixed by it exactly when each of its values is fixed in A. Since those values form the subring TauCeti.frobeniusFixedSubring A p n, the fixed points of the Frobenius are precisely the points of H valued in that subring:

WithConv (H →ₐ[ℤ] frobeniusFixedSubring A p n) ≃* fixedSubgroup (iterateFrobeniusPoints p n).

This is what makes the fixed-point construction of the finite groups of Lie type a construction of 𝔽_q-rational points: for p prime, 0 < n, A an algebraic closure of ZMod p and q = p ^ n the fixed subring is the field of q elements inside A, so the fixed subgroup is the group of 𝔽_q-points of H — and, when H is moreover commutative, of the affine group scheme Spec H. At n = 0 the Frobenius iterate is the identity and the fixed subgroup is all of the A-valued points. Nothing here needs A to be a field, algebraically closed, or of finite type, and no finiteness is asserted.

Main definitions

• TauCeti.Bialgebra.frobeniusFixedInclusion: the inclusion of the points valued in the Frobenius-fixed subring into the points valued in A.
• TauCeti.Bialgebra.frobeniusFixedPointsMulEquiv: the resulting isomorphism onto the fixed subgroup of the Frobenius.

Main results

• TauCeti.Bialgebra.iterateFrobeniusPoints_eq_self_iff: a point is Frobenius-fixed exactly when all of its values are.
• TauCeti.Bialgebra.range_frobeniusFixedInclusion: the inclusion has the fixed subgroup as its range.
• TauCeti.Bialgebra.frobeniusFixedInclusion_frobeniusFixedPointsMulEquiv_symm_apply and TauCeti.Bialgebra.coe_frobeniusFixedPointsMulEquiv_symm_apply_apply: the inverse of that isomorphism reads a fixed point as a point over the fixed subring, with the same values.
• TauCeti.Bialgebra.fixedSubgroup_iterateFrobeniusPoints_le_of_dvd: the fixed subgroups grow along divisibility of the exponent, the inclusion G(𝔽_{p ^ m}) ⊆ G(𝔽_{p ^ k}) in the motivating case.
• TauCeti.Bialgebra.map_fixedSubgroup_iterateFrobeniusPoints_le and TauCeti.Bialgebra.mapValue_mem_fixedSubgroup_iterateFrobeniusPoints: a homomorphism of value algebras carries Frobenius-fixed points to Frobenius-fixed points.

References

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" in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which names the q-power Frobenius as the first case a consumer asks for. The consumer is milestone L3 of TauCetiRoadmap/CFSGStatement/README.md, which sets H_d = fixedSubgroup d.steinberg; the construction is standard, see R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.

@[simp]

theorem TauCeti.Bialgebra.iterateFrobeniusPoints_eq_self_iff (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] {f : WithConv (H →ₐ[ℤ] A)} : (iterateFrobeniusPoints p n) f = f ↔ ∀ (h : H), f.ofConv h ^ p ^ n = f.ofConv h

A point is fixed by the p ^ n-power Frobenius exactly when every one of its values lies in the Frobenius-fixed subring of the value algebra.

noncomputable def TauCeti.Bialgebra.frobeniusFixedInclusion (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] : WithConv (H →ₐ[ℤ] ↥(frobeniusFixedSubring A p n)) →* WithConv (H →ₐ[ℤ] A)

The homomorphism of convolution monoids that reads a point valued in the Frobenius-fixed subring of A as a point valued in A. It is post-composition with the inclusion of the subring, so it needs only the bialgebra structure; for a Hopf algebra it is a homomorphism of the convolution groups.

Equations

• TauCeti.Bialgebra.frobeniusFixedInclusion p n = TauCeti.AlgHom.mapValue (TauCeti.frobeniusFixedSubring A p n).subtype.toIntAlgHom

@[simp]

theorem TauCeti.Bialgebra.frobeniusFixedInclusion_apply_apply (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] (f : WithConv (H →ₐ[ℤ] ↥(frobeniusFixedSubring A p n))) (h : H) : ((frobeniusFixedInclusion p n) f).ofConv h = ↑(f.ofConv h)

Pointwise, the inclusion of the points valued in the Frobenius-fixed subring is the inclusion of that subring applied to each value.

theorem TauCeti.Bialgebra.frobeniusFixedInclusion_injective (p n : ℕ) {H : Type u} [Semiring H] [Bialgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] : Function.Injective ⇑(frobeniusFixedInclusion p n)

Reading a point valued in the Frobenius-fixed subring as a point valued in A loses no information.

theorem TauCeti.Bialgebra.range_frobeniusFixedInclusion (p n : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] : (frobeniusFixedInclusion p n).range = fixedSubgroup (iterateFrobeniusPoints p n)

The points valued in the Frobenius-fixed subring are exactly the Frobenius-fixed points.

noncomputable def TauCeti.Bialgebra.frobeniusFixedPointsMulEquiv (p n : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] : WithConv (H →ₐ[ℤ] ↥(frobeniusFixedSubring A p n)) ≃* ↥(fixedSubgroup (iterateFrobeniusPoints p n))

The fixed points of the p ^ n-power Frobenius on the A-valued points of H are the points of H valued in the Frobenius-fixed subring of A. When H is moreover commutative these are the points of the affine group scheme Spec H.

For p prime, 0 < n, A an algebraic closure of ZMod p and q = p ^ n the right-hand side is the group of 𝔽_q-points, which is why the finite groups of Lie type are defined as fixed points of a Steinberg endomorphism.

Equations

• TauCeti.Bialgebra.frobeniusFixedPointsMulEquiv p n = (MonoidHom.ofInjective ⋯).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem TauCeti.Bialgebra.coe_frobeniusFixedPointsMulEquiv (p n : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] (f : WithConv (H →ₐ[ℤ] ↥(frobeniusFixedSubring A p n))) : ↑((frobeniusFixedPointsMulEquiv p n) f) = (frobeniusFixedInclusion p n) f

The isomorphism onto the fixed subgroup is the inclusion of the points valued in the Frobenius-fixed subring, read in the ambient group of A-valued points.

@[simp]

theorem TauCeti.Bialgebra.frobeniusFixedInclusion_frobeniusFixedPointsMulEquiv_symm_apply (p n : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] (g : ↥(fixedSubgroup (iterateFrobeniusPoints p n))) : (frobeniusFixedInclusion p n) ((frobeniusFixedPointsMulEquiv p n).symm g) = ↑g

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

@[simp]

theorem TauCeti.Bialgebra.coe_frobeniusFixedPointsMulEquiv_symm_apply_apply (p n : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] (g : ↥(fixedSubgroup (iterateFrobeniusPoints p n))) (h : H) : ↑(((frobeniusFixedPointsMulEquiv p n).symm g).ofConv h) = (↑g).ofConv h

Pointwise form: the values of the point over the Frobenius-fixed subring produced by the inverse of the isomorphism are the values of the Frobenius-fixed point it came from.

Elementary properties of the fixed subgroup

theorem TauCeti.Bialgebra.fixedSubgroup_iterateFrobeniusPoints_zero (p : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] : fixedSubgroup (iterateFrobeniusPoints p 0) = ⊤

The zeroth Frobenius iterate fixes every point.

Deliberately not @[simp]: iterateFrobeniusPoints_zero already rewrites the endomorphism to the identity, after which MonoidHom.eqLocus_same closes the goal, so a simp attribute here would be redundant and the simpNF linter rejects it.

theorem TauCeti.Bialgebra.fixedSubgroup_iterateFrobeniusPoints_le_of_dvd (p : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] {m k : ℕ} (hmk : m ∣ k) : fixedSubgroup (iterateFrobeniusPoints p m) ≤ fixedSubgroup (iterateFrobeniusPoints p k)

Fixed subgroups grow along divisibility of the exponent. In the motivating case this is the inclusion G(𝔽_{p ^ m}) ⊆ G(𝔽_{p ^ k}) of groups of rational points.

theorem TauCeti.Bialgebra.map_fixedSubgroup_iterateFrobeniusPoints_le (p n : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] {B : Type w} [CommRing B] [ExpChar B p] (φ : A →ₐ[ℤ] B) : Subgroup.map (AlgHom.mapValue φ) (fixedSubgroup (iterateFrobeniusPoints p n)) ≤ fixedSubgroup (iterateFrobeniusPoints p n)

The image of the Frobenius-fixed subgroup under a homomorphism of value algebras lands in the Frobenius-fixed subgroup: the functoriality of the points in the value algebra restricts to the rational points.

Frobenius on points is natural in the value algebra (mapValue_comp_iterateFrobeniusPoints), so this is an instance of TauCeti.map_fixedSubgroup_le: an intertwiner carries fixed points to fixed points.

theorem TauCeti.Bialgebra.mapValue_mem_fixedSubgroup_iterateFrobeniusPoints (p n : ℕ) {H : Type u} [Semiring H] [HopfAlgebra ℤ H] {A : Type v} [CommRing A] [ExpChar A p] {B : Type w} [CommRing B] [ExpChar B p] (φ : A →ₐ[ℤ] B) {f : WithConv (H →ₐ[ℤ] A)} (hf : f ∈ fixedSubgroup (iterateFrobeniusPoints p n)) : (AlgHom.mapValue φ) f ∈ fixedSubgroup (iterateFrobeniusPoints p n)

The pointwise form of map_fixedSubgroup_iterateFrobeniusPoints_le: a homomorphism of value algebras carries Frobenius-fixed points to Frobenius-fixed points.