Cyclic subgroups generated by Frobenius twists

The Galois-theoretic lower-bound argument uses elements (σ, τ) in a direct product. The first component σ generates the constant-field Galois group, while the order of the second finite group divides the order of σ.

This file records the resulting elementary group facts: every twist has the same order as σ, its cyclic subgroup meets the kernel of first projection trivially, and that cyclic subgroup has the expected cardinality. These are the group-theoretic inputs for taking fixed fields of Frobenius twists.

theorem BGS.HasseWeil.orderOf_prod_eq_left_of_natCard_dvd {A : Type u_1} {B : Type u_2} [Group A] [Group B] (a : A) (b : B) (hcard : Nat.card B ∣ orderOf a) : orderOf (a, b) = orderOf a

If the order of the finite second factor divides the order of a, then the pair (a,b) has the same order as a.

theorem BGS.HasseWeil.zpowers_prod_inf_fst_ker_eq_bot_of_natCard_dvd {A : Type u_1} {B : Type u_2} [Group A] [Group B] (a : A) (b : B) (hcard : Nat.card B ∣ orderOf a) : Subgroup.zpowers (a, b) ⊓ (MonoidHom.fst A B).ker = ⊥

The cyclic subgroup generated by a Frobenius twist meets the kernel of first projection trivially.

theorem BGS.HasseWeil.natCard_zpowers_prod_eq_orderOf_left_of_natCard_dvd {A : Type u_1} {B : Type u_2} [Group A] [Group B] (a : A) (b : B) (hcard : Nat.card B ∣ orderOf a) : Nat.card ↥(Subgroup.zpowers (a, b)) = orderOf a

The cyclic subgroup generated by a Frobenius twist has cardinality equal to the order of the constant-field generator.