The p-part and the p-free part of an element of finite order

This file defines two power-based constructions, TauCeti.pFreePart p x and TauCeti.pPart p x. When p is prime and x has finite order, they give the unique factorisation of x as a product x = s * u of two commuting elements with the order of s prime to p and the order of u a power of p. Their orders are respectively the complementary part ordCompl[p] (orderOf x) and the projected part ordProj[p] (orderOf x). In the group-theoretic literature the two are the p'-part and the p-part of x.

The p-free construction and its order and uniqueness results require only a monoid; the complementary p-part uses group inverses. Both factors are powers of x, so anything commuting with x commutes with both; this is how the factorisation gets used, since it lets a p-subgroup be attached to x inside the centraliser of its p-free factor.

Main definitions

• TauCeti.pFreePart p x: the power-based construction underlying the p-free factor.
• TauCeti.pPart p x: the complementary construction underlying the p-power factor.

Main results

• TauCeti.pFreePart_mem_powers: the p-free part is a natural power in any monoid.
• TauCeti.pFreePart_mul_pPart: the two factors multiply back to x.
• TauCeti.commute_pFreePart_pPart: the two factors commute.
• TauCeti.commute_pFreePart, TauCeti.commute_pPart: anything commuting with x commutes with both factors.
• TauCeti.orderOf_pFreePart, TauCeti.orderOf_pPart: when p is prime and x has finite order, their orders are ordCompl[p] (orderOf x) and ordProj[p] (orderOf x).
• TauCeti.pPart_ne_one_of_dvd_orderOf, TauCeti.isPGroup_zpowers_pPart: if p divides the order of x, its p-part is nontrivial, and the subgroup it generates is a p-group.
• TauCeti.eq_pFreePart, TauCeti.eq_pPart: the factorisation is the only one of its kind.
• TauCeti.pFreePart_conj, TauCeti.pPart_conj: conjugation transports both factors.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), Part II, §10.

noncomputable def TauCeti.pFreePart {G : Type u_1} [Monoid G] (p : ℕ) (x : G) : G

The power of x that gives its p-free part when p is prime and x has finite order. In a group, together with TauCeti.pPart p x, it factors x into two commuting elements.

Equations

• TauCeti.pFreePart p x = x ^ TauCeti.pFreeExponent✝ p x

theorem TauCeti.pFreePart_mem_powers {G : Type u_1} [Monoid G] (p : ℕ) (x : G) : pFreePart p x ∈ Submonoid.powers x

The p-free part of x is a natural power of x.

theorem TauCeti.commute_pFreePart {G : Type u_1} [Monoid G] {x : G} (p : ℕ) {y : G} (h : Commute y x) : Commute y (pFreePart p x)

An element commuting with x commutes with the p-free part of x.

@[simp]

theorem TauCeti.pFreePart_one {G : Type u_1} [Monoid G] (p : ℕ) : pFreePart p 1 = 1

@[simp]

theorem TauCeti.orderOf_pFreePart {p : ℕ} {G : Type u_1} [Monoid G] {x : G} (hp : Nat.Prime p) (hx : orderOf x ≠ 0) : orderOf (pFreePart p x) = orderOf x / p ^ (orderOf x).factorization p

The order of the p-free part of x is the p-free part of the order of x.

theorem TauCeti.not_dvd_orderOf_pFreePart {p : ℕ} {G : Type u_1} [Monoid G] {x : G} (hp : Nat.Prime p) (hx : orderOf x ≠ 0) : ¬p ∣ orderOf (pFreePart p x)

The order of the p-free part of x is prime to p.

theorem TauCeti.eq_pFreePart {p : ℕ} {G : Type u_1} [Monoid G] {x : G} (hp : Nat.Prime p) {s u : G} (hsu : Commute s u) (hmul : s * u = x) (hs : ¬p ∣ orderOf s) {k : ℕ} (hu : orderOf u = p ^ k) : s = pFreePart p x

The factorisation is unique. A commuting factorisation x = s * u in which the order of s is prime to p and the order of u is a power of p has s the p-free part of x.

noncomputable def TauCeti.pPart {G : Type u_1} [Group G] (p : ℕ) (x : G) : G

The element complementary to TauCeti.pFreePart p x in x; when p is prime and x has finite order, it is the p-part of x.

Equations

• TauCeti.pPart p x = (TauCeti.pFreePart p x)⁻¹ * x

@[simp]

theorem TauCeti.pFreePart_mul_pPart {G : Type u_1} [Group G] (p : ℕ) (x : G) : pFreePart p x * pPart p x = x

The p-free and p-parts of x multiply back to x.

theorem TauCeti.pFreePart_mem_zpowers {G : Type u_1} [Group G] (p : ℕ) (x : G) : pFreePart p x ∈ Subgroup.zpowers x

The p-free part of x is a power of x.

theorem TauCeti.pPart_mem_zpowers {G : Type u_1} [Group G] (p : ℕ) (x : G) : pPart p x ∈ Subgroup.zpowers x

The p-part of x is a power of x.

theorem TauCeti.commute_pFreePart_pPart {G : Type u_1} [Group G] (p : ℕ) (x : G) : Commute (pFreePart p x) (pPart p x)

The p-free and p-parts of x commute.

theorem TauCeti.commute_pPart {G : Type u_1} [Group G] {x : G} (p : ℕ) {y : G} (h : Commute y x) : Commute y (pPart p x)

An element commuting with x commutes with the p-part of x.

@[simp]

theorem TauCeti.pPart_mul_pFreePart {G : Type u_1} [Group G] (p : ℕ) (x : G) : pPart p x * pFreePart p x = x

The reversed product of the p-part and p-free part of x is x.

@[simp]

theorem TauCeti.pPart_one {G : Type u_1} [Group G] (p : ℕ) : pPart p 1 = 1

@[simp]

theorem TauCeti.pFreePart_conj {G : Type u_1} [Group G] (p : ℕ) (g x : G) : pFreePart p (g * x * g⁻¹) = g * pFreePart p x * g⁻¹

Conjugation transports the p-free part. Both factors are powers of x cut out by an exponent that only depends on the order of x, and conjugation preserves orders.

@[simp]

theorem TauCeti.pPart_conj {G : Type u_1} [Group G] (p : ℕ) (g x : G) : pPart p (g * x * g⁻¹) = g * pPart p x * g⁻¹

Conjugation transports the p-part.

@[simp]

theorem TauCeti.orderOf_pPart {p : ℕ} {G : Type u_1} [Group G] {x : G} (hp : Nat.Prime p) (hx : orderOf x ≠ 0) : orderOf (pPart p x) = p ^ (orderOf x).factorization p

The order of the p-part of x is the p-part of the order of x. In particular it is a power of p.

theorem TauCeti.pPart_ne_one_of_dvd_orderOf {p : ℕ} {G : Type u_1} [Group G] {x : G} (hp : Nat.Prime p) (hx : orderOf x ≠ 0) (hpx : p ∣ orderOf x) : pPart p x ≠ 1

If p divides the order of x, then the p-part of x is nontrivial.

theorem TauCeti.isPGroup_zpowers_pPart {p : ℕ} {G : Type u_1} [Group G] {x : G} (hp : Nat.Prime p) (hx : orderOf x ≠ 0) : IsPGroup p ↥(Subgroup.zpowers (pPart p x))

The subgroup generated by the p-part of an element of finite order is a p-group.

theorem TauCeti.eq_pPart {p : ℕ} {G : Type u_1} [Group G] {x : G} (hp : Nat.Prime p) {s u : G} (hsu : Commute s u) (hmul : s * u = x) (hs : ¬p ∣ orderOf s) {k : ℕ} (hu : orderOf u = p ^ k) : u = pPart p x

The companion to TauCeti.eq_pFreePart: the p-power factor of a commuting factorisation is the p-part.