Lemma 3.1 — structure of finite tame quotients

Paper Lemma 3.1: In every finite quotient generated by s, t with t^s = t^2, the element t has odd order, and the quotient has the form C_e ⋊ C_n (e odd) with s⁻¹ t s = t^2. Every normal 2-subgroup of such a quotient is central and lies in the unramified cyclic direction.

Here the paper's t^s = t^2 means s⁻¹ * t * s = t^2 (right-conjugation convention).

The first assertion — t has odd order — is elementary and is proved in full below. The further claims used by the formalization — normality of ⟨t⟩ and centrality of normal 2-subgroups — are also proved below. The explicit C_e ⋊ C_n decomposition is not separately packaged because no downstream theorem consumes it.

theorem GQ2.Tame.conj_pow_iterate {G : Type u_1} [Group G] {s t : G} (h : s⁻¹ * t * s = t ^ 2) (n : ℕ) : (s ^ n)⁻¹ * t * s ^ n = t ^ 2 ^ n

Iterated conjugation: (sⁿ)⁻¹ t sⁿ = t^(2ⁿ), from the tame relation s⁻¹ t s = t².

theorem GQ2.Tame.tame_odd_order {G : Type u_1} [Group G] {s t : G} (hs : orderOf s ≠ 0) (h : s⁻¹ * t * s = t ^ 2) : Odd (orderOf t)

Lemma 3.1 (first assertion). If a finite group is generated by s, t with the tame relation s⁻¹ t s = t² (so in particular s has finite order), then t has odd order.

theorem GQ2.Tame.zpowers_sq_eq_of_odd {G : Type u_1} [Group G] {t : G} (ht : Odd (orderOf t)) : Subgroup.zpowers (t ^ 2) = Subgroup.zpowers t

For an element t of odd order, ⟨t²⟩ = ⟨t⟩ (squaring is an automorphism of ⟨t⟩).

theorem GQ2.Tame.zpowers_normal_of_tame {G : Type u_1} [Group G] {s t : G} [Finite G] (hgen : Subgroup.closure {s, t} = ⊤) (h : s⁻¹ * t * s = t ^ 2) : (Subgroup.zpowers t).Normal

The cyclic subgroup ⟨t⟩ is normal in G = ⟨s, t⟩.

The proof uses zpowers_sq_eq_of_odd: conjugation by s⁻¹ is the automorphism MulAut.conj s⁻¹, and (MulAut.conj s⁻¹) t = s⁻¹ t s = t², so (⟨t⟩).map (conj s⁻¹) = ⟨t²⟩ = ⟨t⟩ (odd order). Hence s (and trivially t) lie in (⟨t⟩).normalizer; since ⟨s,t⟩ = ⊤, the normalizer is ⊤, i.e. ⟨t⟩ is normal.

theorem GQ2.Tame.tame_normal_two_subgroup_central {G : Type u_1} [Group G] {s t : G} [Finite G] (hgen : Subgroup.closure {s, t} = ⊤) (h : s⁻¹ * t * s = t ^ 2) (N : Subgroup G) [hNnorm : N.Normal] (hN : IsPGroup 2 ↥N) : N ≤ Subgroup.center G

Lemma 3.1 (normal 2-subgroups are central). Every normal 2-subgroup N of a finite tame quotient ⟨s,t | s⁻¹ t s = t²⟩ is central.

Key idea: N ⊓ ⟨t⟩ = ⊥ (coprime orders), so for n ∈ N the commutator ⁅n,s⁆ lies in N (normality) and in ⟨t⟩ (the quotient G/⟨t⟩ is cyclic, hence abelian), whence ⁅n,s⁆ = 1; together with ⁅n,t⁆ = 1 this puts n in the centralizer of the generators {s,t}, i.e. the centre.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 3.1 = ⟦lem-tamefinite⟧