Coprime exponents in a group

If n and m are coprime natural numbers then every element y of a group lies in the subgroup generated by y ^ n and y ^ m: a Bézout identity 1 = n * i + m * j turns into the factorization y = (y ^ n) ^ i * (y ^ m) ^ j, with i and j the same for every y.

The same arithmetic, run over all primes at once, detects membership in a subgroup: if for every prime p some power x ^ m with p ∤ m lies in H, then x ∈ H, because the exponents m with x ^ m ∈ H are the multiples of a single number that no prime divides. This is the prime-by-prime assembly step of Brauer's induction theorem, where m • 1 lies in the span of virtual characters induced from p-elementary subgroups.

Main results

• TauCeti.exists_zpow_mul_zpow_eq_of_coprime and its additive form TauCeti.exists_zsmul_add_zsmul_eq_of_coprime: the factorization above, with coefficients independent of y.
• Subgroup.mem_of_forall_prime_exists_pow_mem and its additive form AddSubgroup.mem_of_forall_prime_exists_nsmul_mem: membership from prime-to-p powers, one prime at a time.

theorem TauCeti.exists_zpow_mul_zpow_eq_of_coprime {G : Type u_1} [Group G] {n m : ℕ} (h : n.Coprime m) : ∃ (i : ℤ), ∃ (j : ℤ), ∀ (y : G), (y ^ n) ^ i * (y ^ m) ^ j = y

For coprime n and m, every element y of a group factors as a product of an integer power of y ^ n and an integer power of y ^ m, the exponents being the Bézout coefficients of n and m and hence independent of y. Consequently y lies in any subgroup product A * B with y ^ n ∈ A and y ^ m ∈ B.

theorem TauCeti.exists_zsmul_add_zsmul_eq_of_coprime {G : Type u_1} [AddGroup G] {n m : ℕ} (h : n.Coprime m) : ∃ (i : ℤ), ∃ (j : ℤ), ∀ (y : G), i • n • y + j • m • y = y

For coprime n and m, every element y of an additive group decomposes as a sum of an integer multiple of n • y and an integer multiple of m • y, the coefficients being the Bézout coefficients of n and m and hence independent of y.

theorem Subgroup.mem_of_forall_prime_exists_pow_mem {G : Type u_1} [Group G] {H : Subgroup G} {x : G} (h : ∀ (p : ℕ), Nat.Prime p → ∃ (m : ℕ), ¬p ∣ m ∧ x ^ m ∈ H) : x ∈ H

Membership from prime-to-p powers. If for every prime p some power x ^ m with p ∤ m lies in the subgroup H, then x lies in H.

theorem AddSubgroup.mem_of_forall_prime_exists_nsmul_mem {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {x : G} (h : ∀ (p : ℕ), Nat.Prime p → ∃ (m : ℕ), ¬p ∣ m ∧ m • x ∈ H) : x ∈ H

Membership from prime-to-p multiples. If for every prime p some multiple m • x with p ∤ m lies in the additive subgroup H, then x lies in H.