The p-free part of a cyclic group

Let g be an element of finite order m in a group, and p a prime. Write m = ordProj[p] m * ordCompl[p] m for the factorisation of m into its p-power part and its p-free part. Inside the cyclic group ⟨g⟩ the subgroup generated by the p-free part TauCeti.pFreePart p g of g then has order ordCompl[p] m, hence order prime to p and index ordProj[p] m, and it absorbs ordProj[p] m-th powers, so every element of ⟨g⟩ has a p-power power inside it. It is the p-complement of ⟨g⟩, which exists because a cyclic group is abelian and so has a Hall subgroup for every set of primes; no general Hall theory is used here, the generator making the subgroup explicit.

The subgroup is intrinsic to ⟨g⟩: it consists of the elements of ⟨g⟩ whose order is prime to p, so it does not depend on the chosen generator, and it is equally generated by g ^ ordProj[p] m. For a finite cyclic subgroup C of a group the properties combine into the single existence statement TauCeti.exists_coprimePart_of_isCyclic: C has a normal subgroup D of order prime to p with C / D of p-power exponent, which is how the p-part of a cyclic subgroup is stripped off inside a sum over the cyclic subgroups of a finite group.

Main results

• TauCeti.natCard_zpowers_pFreePart: the subgroup generated by the p-free part of g has order ordCompl[p] (orderOf g), and TauCeti.not_dvd_natCard_zpowers_pFreePart: that order is prime to p.
• TauCeti.relIndex_zpowers_pFreePart: its index in ⟨g⟩ is ordProj[p] (orderOf g).
• TauCeti.pow_ordProj_mem_zpowers_pFreePart_of_mem_zpowers: raising any element of ⟨g⟩ to the power ordProj[p] (orderOf g) lands in it, so the quotient has p-power exponent.
• TauCeti.zpowers_pFreePart_eq_zpowers_pow_ordProj: it is generated by g ^ ordProj[p] (orderOf g).
• TauCeti.mem_zpowers_pFreePart_iff: it consists exactly of the elements of ⟨g⟩ of order prime to p.
• TauCeti.exists_coprimePart_of_isCyclic: the p-free part of a cyclic subgroup, the four properties together, for a finite cyclic subgroup of a group.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), (7.3.4), where the assembled statement is the group-theoretic input to the modular Artin induction theorem.

theorem TauCeti.zpowers_pFreePart_le {G : Type u_1} [Group G] (p : ℕ) (g : G) : Subgroup.zpowers (pFreePart p g) ≤ Subgroup.zpowers g

The subgroup generated by the p-free part of g sits inside the one generated by g, because the p-free part is a power of g.

theorem TauCeti.natCard_zpowers_pFreePart {G : Type u_1} [Group G] {p : ℕ} {g : G} (hp : Nat.Prime p) (hg : orderOf g ≠ 0) : Nat.card ↥(Subgroup.zpowers (pFreePart p g)) = orderOf g / p ^ (orderOf g).factorization p

The order of the p-free part subgroup. For an element of finite order it is the p-free part ordCompl[p] (orderOf g) of the order of g.

theorem TauCeti.not_dvd_natCard_zpowers_pFreePart {G : Type u_1} [Group G] {p : ℕ} {g : G} (hp : Nat.Prime p) (hg : orderOf g ≠ 0) : ¬p ∣ Nat.card ↥(Subgroup.zpowers (pFreePart p g))

The p-free part subgroup has order prime to p.

@[simp]

theorem TauCeti.relIndex_zpowers_pFreePart {G : Type u_1} [Group G] {p : ℕ} {g : G} (hp : Nat.Prime p) (hg : orderOf g ≠ 0) : (Subgroup.zpowers (pFreePart p g)).relIndex (Subgroup.zpowers g) = p ^ (orderOf g).factorization p

The index of the p-free part subgroup in ⟨g⟩ is the p-power part ordProj[p] (orderOf g) of the order of g: the two factors of orderOf g are the order of the subgroup and its index.

theorem TauCeti.pow_ordProj_mem_zpowers_pFreePart {G : Type u_1} [Group G] {p : ℕ} {g : G} (hp : Nat.Prime p) (hg : orderOf g ≠ 0) : g ^ p ^ (orderOf g).factorization p ∈ Subgroup.zpowers (pFreePart p g)

The p-free part subgroup absorbs ordProj[p] (orderOf g)-th powers of g. Raising g to the p-power part of its order lands in the subgroup generated by the p-free part of g.

theorem TauCeti.pow_ordProj_mem_zpowers_pFreePart_of_mem_zpowers {G : Type u_1} [Group G] {p : ℕ} {g : G} (hp : Nat.Prime p) (hg : orderOf g ≠ 0) {c : G} (hc : c ∈ Subgroup.zpowers g) : c ^ p ^ (orderOf g).factorization p ∈ Subgroup.zpowers (pFreePart p g)

The quotient of ⟨g⟩ by its p-free part has p-power exponent. Every element of ⟨g⟩ raised to the power ordProj[p] (orderOf g) lies in the subgroup generated by the p-free part of g.

theorem TauCeti.zpowers_pFreePart_eq_zpowers_pow_ordProj {G : Type u_1} [Group G] {p : ℕ} {g : G} (hp : Nat.Prime p) (hg : orderOf g ≠ 0) : Subgroup.zpowers (pFreePart p g) = Subgroup.zpowers (g ^ p ^ (orderOf g).factorization p)

The p-free part subgroup is generated by g ^ ordProj[p] (orderOf g). The p-free part of g and the ordProj[p] (orderOf g)-th power of g generate the same subgroup, so either spelling of the p-complement of ⟨g⟩ may be used.

@[simp]

theorem TauCeti.mem_zpowers_pFreePart_iff {G : Type u_1} [Group G] {p : ℕ} {g : G} (hp : Nat.Prime p) (hg : orderOf g ≠ 0) {x : G} : x ∈ Subgroup.zpowers (pFreePart p g) ↔ x ∈ Subgroup.zpowers g ∧ ¬p ∣ orderOf x

The p-free part subgroup is exactly the set of p-free elements of ⟨g⟩. An element of ⟨g⟩ lies in it precisely when its order is prime to p, so the subgroup is intrinsic to ⟨g⟩ and does not depend on the chosen generator.

theorem TauCeti.exists_coprimePart_of_isCyclic {G : Type u_1} [Group G] {p : ℕ} (hp : Nat.Prime p) {C : Subgroup G} [Finite ↥C] [IsCyclic ↥C] : ∃ D ≤ C, (D.subgroupOf C).Normal ∧ ¬p ∣ Nat.card ↥D ∧ (∀ c ∈ C, ∃ (n : ℕ), c ^ p ^ n ∈ D) ∧ D.relIndex C = p ^ (Nat.card ↥C).factorization p

The p-free part of a cyclic subgroup. A finite cyclic subgroup C of a group has a subgroup D which is normal in C, has order prime to p, has relative index the p-power part of |C|, and contains a p-power power of every element of C; concretely D is the subgroup generated by the p-free part (TauCeti.pFreePart) of a generator of C.