The q-Frobenius on the points of a group scheme over 𝔽_q

Let K be a finite field with q elements and let H be a Hopf algebra over K, the coordinate algebra of an affine group scheme G₀ over K. No splitting, ℤ-model or reductivity is assumed: H is an arbitrary K-form. For a commutative K-algebra A, the q ^ n-Frobenius acts on the convolution group of A-valued points WithConv (H →ₐ[K] A) by post-composition with the K-algebra endomorphism x ↦ x ^ q ^ n of A (TauCeti.FiniteField.frobeniusPoints).

When H is commutative, the q-power map on the functions of G₀ is the bialgebra endomorphism TauCeti.frobeniusBialgHom K H, the Frobenius endomorphism of G₀ defined by its 𝔽_q-structure, and the q-Frobenius on points is pre-composition with it. For A = k an algebraic closure of 𝔽_q, reading the k-points of G = G₀ ×_{𝔽_q} k as the k-valued points of H, this is the geometric Frobenius F of G. On the coordinate algebra k ⊗[K] H of the base change it is the scalar extension id ⊗ Frob of the q-power map (TauCeti.FiniteField.geometricFrobeniusBialgHom), which is not the q-power map of k ⊗[K] H since that is not k-linear; under G(R) ≃ Hom_K(H, R) it becomes the q-Frobenius on points.

The fixed points of the Frobenius are the points valued in the Frobenius-fixed subalgebra of A (TauCeti.FiniteField.frobeniusFixedPointsMulEquiv). When A is a domain, for instance a field extension of K, the points fixed by the q-Frobenius are exactly the K-rational points: G^F ≃ G₀(K) (TauCeti.FiniteField.rationalPointsMulEquiv). If moreover H is of finite type, the points fixed by every positive iterate F ^ n form a finite group (TauCeti.FiniteField.finite_fixedSubgroup_frobeniusPoints). All of this is natural in the coordinate algebra, so it applies to every morphism of group schemes over K and in particular to the inclusion of a closed subgroup scheme, whose coordinate algebra is again of finite type.

Main definitions

• TauCeti.FiniteField.frobeniusPoints: the q ^ n-Frobenius on A-valued points.
• TauCeti.FiniteField.frobeniusFixedPointsMulEquiv: the Frobenius-fixed points are the points valued in the Frobenius-fixed subalgebra.
• TauCeti.FiniteField.rationalPointsMulEquiv: over a domain, the q-Frobenius-fixed points are the K-points.
• TauCeti.FiniteField.geometricFrobeniusBialgHom: the geometric Frobenius id ⊗ Frob of a base change k ⊗[K] H.
• TauCeti.FiniteField.rationalPointsMulEquivFixedSubgroupGeometricFrobenius: G₀(K) ≃ G^F for the geometric Frobenius of the base change to a domain.

Main results

• TauCeti.FiniteField.frobeniusPoints_apply_apply: the Frobenius raises every value of a point to the q ^ n-th power.
• TauCeti.FiniteField.mapDomain_frobeniusBialgHom: for commutative H, the q-Frobenius on points is pre-composition with the Frobenius endomorphism TauCeti.frobeniusBialgHom K H.
• TauCeti.FiniteField.mapDomain_comp_frobeniusPoints: the Frobenius on points commutes with every morphism of group schemes over K.
• TauCeti.FiniteField.coe_rationalPointsMulEquiv_mapDomain: the identification of the fixed points with the K-points is natural in the group scheme.
• TauCeti.FiniteField.finite_fixedSubgroup_frobeniusPoints: for H of finite type and A a domain, the points fixed by a positive iterate of the Frobenius form a finite group.
• TauCeti.FiniteField.baseChangePointsMulEquiv_symm_comp_mapDomain_geometricFrobeniusBialgHom: base change identifies the geometric Frobenius with the q-Frobenius on points.
• BialgHom.map_fixedSubgroup_frobeniusPoints_of_surjective: the fixed points of a closed subgroup scheme are its points that are fixed in the ambient group.
• BialgHom.tensorProductMap_comp_geometricFrobeniusBialgHom: the geometric Frobenius commutes with the base change of every morphism of monoid schemes over K.
• BialgHom.map_fixedSubgroup_mapDomain_geometricFrobeniusBialgHom_of_surjective: the same description of the fixed points of a closed subgroup scheme for the geometric Frobenius.
• TauCeti.FiniteField.finite_fixedSubgroup_mapDomain_geometricFrobeniusBialgHom: G^F is finite for H of finite type.
• TauCeti.FiniteField.baseChangePointsMulEquiv_symm_frobeniusPoints: for a model over ℤ and q = p ^ n, the q ^ m-Frobenius is the iterated prime-power Frobenius TauCeti.Bialgebra.iterateFrobeniusPoints p (n * m).

References

R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17; O. Dudas and J. Michel, Lectures on finite reductive groups and their representations, §7.

noncomputable def TauCeti.FiniteField.frobeniusPoints (K : Type u_1) [Field K] [Fintype K] {H : Type u_2} [Semiring H] [Bialgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] (n : ℕ) : WithConv (H →ₐ[K] A) →* WithConv (H →ₐ[K] A)

The q ^ n-Frobenius on the convolution monoid of A-valued points of a bialgebra H over a finite field K with q elements. It post-composes a point with the K-algebra endomorphism x ↦ x ^ q ^ n of A.

@[simp]

theorem TauCeti.FiniteField.frobeniusPoints_apply_apply {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [Bialgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] (n : ℕ) (f : WithConv (H →ₐ[K] A)) (h : H) : ((frobeniusPoints K n) f).ofConv h = f.ofConv h ^ Nat.card K ^ n

The q ^ n-Frobenius raises every value of a point to the q ^ n-th power.

@[simp]

theorem TauCeti.FiniteField.frobeniusPoints_eq_self_iff {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [Bialgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] {n : ℕ} {f : WithConv (H →ₐ[K] A)} : (frobeniusPoints K n) f = f ↔ ∀ (h : H), f.ofConv h ^ Nat.card K ^ n = f.ofConv h

A point is fixed by the q ^ n-Frobenius exactly when each of its values is.

@[simp]

theorem TauCeti.FiniteField.frobeniusPoints_zero (K : Type u_1) [Field K] [Fintype K] {H : Type u_2} [Semiring H] [Bialgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] : frobeniusPoints K 0 = MonoidHom.id (WithConv (H →ₐ[K] A))

The zeroth iterate of the Frobenius is the identity on points.

theorem TauCeti.FiniteField.frobeniusPoints_add (K : Type u_1) [Field K] [Fintype K] {H : Type u_2} [Semiring H] [Bialgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] (m n : ℕ) : frobeniusPoints K (m + n) = (frobeniusPoints K m).comp (frobeniusPoints K n)

Iterates of the Frobenius on points compose by adding exponents.

theorem TauCeti.FiniteField.mapDomain_comp_frobeniusPoints {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [Bialgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] {H₁ : Type u_4} [Semiring H₁] [Bialgebra K H₁] (φ : H₁ →ₐc[K] H) (n : ℕ) : φ.mapDomain.comp (frobeniusPoints K n) = (frobeniusPoints K n).comp φ.mapDomain

The Frobenius on points is natural in the coordinate bialgebra: it commutes with the map on points induced by any bialgebra morphism, that is, with every morphism of group schemes over K.

theorem TauCeti.FiniteField.mapValue_comp_frobeniusPoints {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [Bialgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] {B : Type u_4} [CommRing B] [Algebra K B] (φ : A →ₐ[K] B) (n : ℕ) : φ.mapValue.comp (frobeniusPoints K n) = (frobeniusPoints K n).comp φ.mapValue

The Frobenius on points is natural in the value algebra.

The Frobenius endomorphism of a commutative bialgebra

theorem TauCeti.FiniteField.mapDomain_frobeniusBialgHom {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [CommSemiring H] [Bialgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] : (frobeniusBialgHom K H).mapDomain = frobeniusPoints K 1

The Frobenius on points is the map induced by the Frobenius endomorphism: for a commutative bialgebra H over K, raising the values of a point to the q-th power is the same as pre-composing it with the q-power map TauCeti.frobeniusBialgHom K H of H, the Frobenius endomorphism of Spec H defined by its K-structure.

Frobenius-fixed points

theorem TauCeti.FiniteField.range_mapValue_val_frobeniusFixedSubalgebra (K : Type u_1) [Field K] [Fintype K] (H : Type u_2) [Semiring H] [HopfAlgebra K H] (A : Type u_3) [CommRing A] [Algebra K A] (n : ℕ) : (frobeniusFixedSubalgebra K A n).val.mapValue.range = fixedSubgroup (frobeniusPoints K n)

The points valued in the Frobenius-fixed subalgebra of A are exactly the Frobenius-fixed points.

noncomputable def TauCeti.FiniteField.frobeniusFixedPointsMulEquiv (K : Type u_1) [Field K] [Fintype K] (H : Type u_2) [Semiring H] [HopfAlgebra K H] (A : Type u_3) [CommRing A] [Algebra K A] (n : ℕ) : WithConv (H →ₐ[K] ↥(frobeniusFixedSubalgebra K A n)) ≃* ↥(fixedSubgroup (frobeniusPoints K n))

The Frobenius-fixed points are the points over the Frobenius-fixed subalgebra. For A an algebraic closure of 𝔽_q and 0 < n the subalgebra is 𝔽_{q ^ n}, so the points fixed by F ^ n are the 𝔽_{q ^ n}-points.

@[simp]

theorem TauCeti.FiniteField.coe_frobeniusFixedPointsMulEquiv {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [HopfAlgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] {n : ℕ} (f : WithConv (H →ₐ[K] ↥(frobeniusFixedSubalgebra K A n))) : ↑((frobeniusFixedPointsMulEquiv K H A n) f) = (frobeniusFixedSubalgebra K A n).val.mapValue f

The isomorphism onto the Frobenius-fixed points reads a point over the fixed subalgebra as an A-valued point.

@[simp]

theorem TauCeti.FiniteField.coe_frobeniusFixedPointsMulEquiv_symm_apply_apply {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [HopfAlgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] {n : ℕ} (g : ↥(fixedSubgroup (frobeniusPoints K n))) (h : H) : ↑(((frobeniusFixedPointsMulEquiv K H A n).symm g).ofConv h) = (↑g).ofConv h

The inverse isomorphism keeps the values of a Frobenius-fixed point.

theorem TauCeti.FiniteField.range_mapValue_ofId (K : Type u_1) [Field K] [Fintype K] (H : Type u_2) [Semiring H] [HopfAlgebra K H] (L : Type u_4) [CommRing L] [IsDomain L] [Algebra K L] : (Algebra.ofId K L).mapValue.range = fixedSubgroup (frobeniusPoints K 1)

Over a domain, the points fixed by the q-Frobenius are exactly those coming from K-points.

noncomputable def TauCeti.FiniteField.rationalPointsMulEquiv (K : Type u_1) [Field K] [Fintype K] (H : Type u_2) [Semiring H] [HopfAlgebra K H] (L : Type u_4) [CommRing L] [IsDomain L] [Algebra K L] : WithConv (H →ₐ[K] K) ≃* ↥(fixedSubgroup (frobeniusPoints K 1))

The q-Frobenius-fixed points are the K-rational points. For a Hopf algebra H over the finite field K = 𝔽_q, the coordinate algebra of an arbitrary 𝔽_q-form G₀, and a domain L over K such as an algebraic closure of 𝔽_q, the points fixed by the Frobenius F are the image of the K-points: G^F ≃ G₀(𝔽_q).

@[simp]

theorem TauCeti.FiniteField.coe_rationalPointsMulEquiv {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [HopfAlgebra K H] (L : Type u_4) [CommRing L] [IsDomain L] [Algebra K L] (f : WithConv (H →ₐ[K] K)) : ↑((rationalPointsMulEquiv K H L) f) = (Algebra.ofId K L).mapValue f

The identification of the K-points with the Frobenius-fixed points composes a K-point with the structure map K → L.

@[simp]

theorem TauCeti.FiniteField.algebraMap_rationalPointsMulEquiv_symm_apply_apply {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [HopfAlgebra K H] (L : Type u_4) [CommRing L] [IsDomain L] [Algebra K L] (g : ↥(fixedSubgroup (frobeniusPoints K 1))) (h : H) : (algebraMap K L) (((rationalPointsMulEquiv K H L).symm g).ofConv h) = (↑g).ofConv h

The inverse identification sends a Frobenius-fixed point to the K-point whose values map to its values under the structure map K → L.

theorem TauCeti.FiniteField.coe_rationalPointsMulEquiv_mapDomain {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [HopfAlgebra K H] (L : Type u_4) [CommRing L] [IsDomain L] [Algebra K L] {H₁ : Type u_5} [Semiring H₁] [HopfAlgebra K H₁] (φ : H₁ →ₐc[K] H) (f : WithConv (H →ₐ[K] K)) : ↑((rationalPointsMulEquiv K H₁ L) (φ.mapDomain f)) = φ.mapDomain ↑((rationalPointsMulEquiv K H L) f)

The identification of the Frobenius-fixed points with the K-points is natural in the group scheme: a morphism φ of group schemes over K acts compatibly on K-points and on Frobenius-fixed L-points.

theorem TauCeti.FiniteField.map_fixedSubgroup_frobeniusPoints_le {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [HopfAlgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] {H₁ : Type u_4} [Semiring H₁] [HopfAlgebra K H₁] (φ : H₁ →ₐc[K] H) (n : ℕ) : Subgroup.map φ.mapDomain (fixedSubgroup (frobeniusPoints K n)) ≤ fixedSubgroup (frobeniusPoints K n)

A morphism of group schemes over K carries Frobenius-fixed points to Frobenius-fixed points.

theorem TauCeti.FiniteField.finite_fixedSubgroup_frobeniusPoints {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [HopfAlgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] [Algebra.FiniteType K H] [IsDomain A] {n : ℕ} (hn : n ≠ 0) : Finite ↥(fixedSubgroup (frobeniusPoints K n))

Finiteness of the Frobenius-fixed points. For a Hopf algebra H of finite type over K and a domain A over K, the points fixed by a positive iterate of the Frobenius form a finite group: they are the points over the finite Frobenius-fixed subalgebra. In particular G^F is finite for every affine group scheme G₀ of finite type over 𝔽_q, and so is the group of rational points of each of its closed subgroup schemes.

theorem BialgHom.map_fixedSubgroup_frobeniusPoints_of_surjective {K : Type u_1} [Field K] [Fintype K] {H : Type u_2} [Semiring H] [HopfAlgebra K H] {A : Type u_3} [CommRing A] [Algebra K A] {H₁ : Type u_4} [Semiring H₁] [HopfAlgebra K H₁] (ψ : H →ₐc[K] H₁) (hψ : Function.Surjective ⇑ψ) (n : ℕ) : Subgroup.map ψ.mapDomain (TauCeti.fixedSubgroup (TauCeti.FiniteField.frobeniusPoints K n)) = ψ.mapDomain.range ⊓ TauCeti.fixedSubgroup (TauCeti.FiniteField.frobeniusPoints K n)

Frobenius-fixed points of a closed subgroup scheme. For a surjective bialgebra morphism ψ : H → H₁, cutting out a closed subgroup scheme of Spec H, the points of that subgroup fixed by its own Frobenius are exactly its points that are fixed in the ambient group.

The geometric Frobenius of a base change

noncomputable def TauCeti.FiniteField.geometricFrobeniusBialgHom (K : Type u_1) [Field K] [Fintype K] (k : Type u_2) [CommSemiring k] [Algebra K k] (H : Type u_3) [CommSemiring H] [Bialgebra K H] : TensorProduct K k H →ₐc[k] TensorProduct K k H

The geometric Frobenius of the base change Spec (k ⊗[K] H) of an affine monoid scheme over a finite field K: the scalar extension id ⊗ Frob of the q-power bialgebra endomorphism of H.

@[simp]

theorem TauCeti.FiniteField.geometricFrobeniusBialgHom_tmul (K : Type u_1) [Field K] [Fintype K] (k : Type u_2) [CommSemiring k] [Algebra K k] (H : Type u_3) [CommSemiring H] [Bialgebra K H] (s : k) (h : H) : (geometricFrobeniusBialgHom K k H) (s ⊗ₜ[K] h) = s ⊗ₜ[K] (h ^ Fintype.card K)

On pure tensors, the geometric Frobenius raises the second factor to its q-th power.

theorem TauCeti.FiniteField.baseChangePointsMulEquiv_symm_comp_mapDomain_geometricFrobeniusBialgHom {K : Type u_1} [Field K] [Fintype K] {k : Type u_2} [CommSemiring k] [Algebra K k] {H : Type u_3} [CommSemiring H] [Bialgebra K H] {R : Type u_4} [CommRing R] [Algebra k R] [Algebra K R] [IsScalarTower K k R] : (↑AlgHom.baseChangePointsMulEquiv.symm).comp (geometricFrobeniusBialgHom K k H).mapDomain = (frobeniusPoints K 1).comp ↑AlgHom.baseChangePointsMulEquiv.symm

Base change identifies the geometric Frobenius with the q-Frobenius on points. Under G(R) ≃ Hom_K(H, R), the map on points induced by the geometric Frobenius of k ⊗[K] H is frobeniusPoints K 1.

Naturality of the geometric Frobenius

theorem BialgHom.tensorProductMap_comp_geometricFrobeniusBialgHom {K : Type u_1} [Field K] [Fintype K] (k : Type u_2) [CommSemiring k] [Algebra K k] {H : Type u_3} {H₁ : Type u_4} [CommSemiring H] [CommSemiring H₁] [Bialgebra K H] [Bialgebra K H₁] (ψ : H →ₐc[K] H₁) : (Bialgebra.TensorProduct.map (BialgHom.id k k) ψ).comp (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H) = (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H₁).comp (Bialgebra.TensorProduct.map (BialgHom.id k k) ψ)

The geometric Frobenius is natural: it commutes with the scalar extension id ⊗ ψ : k ⊗[K] H → k ⊗[K] H₁ of every bialgebra morphism ψ over K, that is, with the base change of every morphism of monoid schemes over K.

theorem BialgHom.mapDomain_tensorProductMap_comp_mapDomain_geometricFrobeniusBialgHom {K : Type u_1} [Field K] [Fintype K] (k : Type u_2) [CommSemiring k] [Algebra K k] {H : Type u_3} {H₁ : Type u_4} [CommSemiring H] [CommSemiring H₁] {R : Type u_5} [CommSemiring R] [Algebra k R] [Bialgebra K H] [Bialgebra K H₁] (ψ : H →ₐc[K] H₁) : (Bialgebra.TensorProduct.map (BialgHom.id k k) ψ).mapDomain.comp (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H₁).mapDomain = (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H).mapDomain.comp (Bialgebra.TensorProduct.map (BialgHom.id k k) ψ).mapDomain

The map on points induced by the base change of a bialgebra morphism ψ over K commutes with the maps on points induced by the geometric Frobenius.

theorem BialgHom.map_fixedSubgroup_mapDomain_geometricFrobeniusBialgHom_le {K : Type u_1} [Field K] [Fintype K] (k : Type u_2) [CommSemiring k] [Algebra K k] {H : Type u_3} {H₁ : Type u_4} [CommSemiring H] [CommSemiring H₁] {R : Type u_5} [CommSemiring R] [Algebra k R] [HopfAlgebra K H] [HopfAlgebra K H₁] (ψ : H →ₐc[K] H₁) : Subgroup.map (Bialgebra.TensorProduct.map (BialgHom.id k k) ψ).mapDomain (TauCeti.fixedSubgroup (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H₁).mapDomain) ≤ TauCeti.fixedSubgroup (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H).mapDomain

The base change of a morphism of group schemes over K carries points fixed by the geometric Frobenius to points fixed by the geometric Frobenius.

theorem BialgHom.map_fixedSubgroup_mapDomain_geometricFrobeniusBialgHom_of_surjective {K : Type u_1} [Field K] [Fintype K] (k : Type u_2) [CommSemiring k] [Algebra K k] {H : Type u_3} {H₁ : Type u_4} [CommSemiring H] [CommSemiring H₁] {R : Type u_5} [CommSemiring R] [Algebra k R] [HopfAlgebra K H] [HopfAlgebra K H₁] (ψ : H →ₐc[K] H₁) (hψ : Function.Surjective ⇑ψ) : Subgroup.map (Bialgebra.TensorProduct.map (BialgHom.id k k) ψ).mapDomain (TauCeti.fixedSubgroup (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H₁).mapDomain) = (Bialgebra.TensorProduct.map (BialgHom.id k k) ψ).mapDomain.range ⊓ TauCeti.fixedSubgroup (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H).mapDomain

Geometric-Frobenius-fixed points of a closed subgroup scheme. For a surjective bialgebra morphism ψ : H → H₁, cutting out a closed subgroup scheme of Spec H over K, the points of its base change fixed by its own geometric Frobenius are exactly its points that are fixed by the geometric Frobenius of the ambient group.

noncomputable def TauCeti.FiniteField.rationalPointsMulEquivFixedSubgroupGeometricFrobenius (K : Type u_1) [Field K] [Fintype K] (k : Type u_2) [CommRing k] [IsDomain k] [Algebra K k] (H : Type u_3) [CommSemiring H] [HopfAlgebra K H] : WithConv (H →ₐ[K] K) ≃* ↥(fixedSubgroup (geometricFrobeniusBialgHom K k H).mapDomain)

G₀(K) ≃ G^F. The K-rational points of H are isomorphic to the points of the base change k ⊗[K] H over a domain k fixed by the geometric Frobenius. The isomorphism sends a rational point g to s ⊗ h ↦ s * g h.

@[simp]

theorem TauCeti.FiniteField.coe_rationalPointsMulEquivFixedSubgroupGeometricFrobenius_apply (K : Type u_1) [Field K] [Fintype K] (k : Type u_2) [CommRing k] [IsDomain k] [Algebra K k] (H : Type u_3) [CommSemiring H] [HopfAlgebra K H] (g : WithConv (H →ₐ[K] K)) : ↑((rationalPointsMulEquivFixedSubgroupGeometricFrobenius K k H) g) = (AlgHom.pointsBaseChange k) g

The isomorphism rationalPointsMulEquivFixedSubgroupGeometricFrobenius is the base change of rational points.

@[simp]

theorem TauCeti.FiniteField.algebraMap_rationalPointsMulEquivFixedSubgroupGeometricFrobenius_symm_apply_apply (K : Type u_1) [Field K] [Fintype K] (k : Type u_2) [CommRing k] [IsDomain k] [Algebra K k] (H : Type u_3) [CommSemiring H] [HopfAlgebra K H] (g : ↥(fixedSubgroup (geometricFrobeniusBialgHom K k H).mapDomain)) (h : H) : (algebraMap K k) (((rationalPointsMulEquivFixedSubgroupGeometricFrobenius K k H).symm g).ofConv h) = (↑g).ofConv (1 ⊗ₜ[K] h)

The inverse isomorphism G^F ≃ G₀(K) sends a fixed point g to the rational point whose value at h maps to g (1 ⊗ h) under the structure map K → k.

theorem TauCeti.FiniteField.mapDomain_rationalPointsMulEquivFixedSubgroupGeometricFrobenius (K : Type u_1) [Field K] [Fintype K] (k : Type u_2) [CommRing k] [IsDomain k] [Algebra K k] {H : Type u_3} [CommSemiring H] [HopfAlgebra K H] {H₁ : Type u_4} [CommSemiring H₁] [HopfAlgebra K H₁] (ψ : H →ₐc[K] H₁) (g : WithConv (H₁ →ₐ[K] K)) : (Bialgebra.TensorProduct.map (BialgHom.id k k) ψ).mapDomain ↑((rationalPointsMulEquivFixedSubgroupGeometricFrobenius K k H₁) g) = ↑((rationalPointsMulEquivFixedSubgroupGeometricFrobenius K k H) (ψ.mapDomain g))

The isomorphism G₀(K) ≃ G^F is natural in the coordinate Hopf algebra: for a morphism ψ : H → H₁, the induced map on rational points corresponds to the map on Frobenius-fixed points induced by the scalar extension of ψ.

theorem TauCeti.FiniteField.finite_fixedSubgroup_mapDomain_geometricFrobeniusBialgHom (K : Type u_1) [Field K] [Fintype K] (k : Type u_2) [CommRing k] [IsDomain k] [Algebra K k] (H : Type u_3) [CommSemiring H] [HopfAlgebra K H] [Algebra.FiniteType K H] : Finite ↥(fixedSubgroup (geometricFrobeniusBialgHom K k H).mapDomain)

The fixed points of the geometric Frobenius form a finite group when the coordinate algebra is of finite type.

Comparison with a model over ℤ

theorem TauCeti.FiniteField.baseChangePointsMulEquiv_symm_frobeniusPoints {K : Type u_1} [Field K] [Fintype K] {p n : ℕ} {H : Type u_2} [Semiring H] [Bialgebra ℤ H] {A : Type u_3} [CommRing A] [Algebra K A] [ExpChar A p] (hq : Nat.card K = p ^ n) (m : ℕ) (f : WithConv (TensorProduct ℤ K H →ₐ[K] A)) : AlgHom.baseChangePointsMulEquiv.symm ((frobeniusPoints K m) f) = (Bialgebra.iterateFrobeniusPoints p (n * m)) (AlgHom.baseChangePointsMulEquiv.symm f)

For a model over ℤ, the q-Frobenius is the iterated prime-power Frobenius. If q = p ^ n, then under (K ⊗ H)(A) ≃ Hom_ℤ(H, A) the q ^ m-Frobenius of the base change K ⊗[ℤ] H is iterateFrobeniusPoints p (n * m).