Elementary and hyperelementary groups

Fix a natural number p. A group is p-elementary when it is the internal direct product of a cyclic subgroup of order prime to p and a p-subgroup, and p-hyperelementary when it has a cyclic normal subgroup of order prime to p whose quotient is a p-group; a group is elementary (respectively hyperelementary) when it is p-elementary (respectively p-hyperelementary) for some prime p. Mathlib has IsCyclic and IsPGroup but no predicate built from them in this shape, so this file supplies the two definitions together with the closure properties they are used through.

The definitions are the ones Brauer's induction theorem is stated against: Artin's theorem writes a character as a rational combination of characters induced from cyclic subgroups, and Brauer's sharpens this to an integral combination of characters induced from elementary subgroups. That the elementary groups include the cyclic ones is the content of TauCeti.isPElementary_of_isCyclic below: a finite cyclic group is p-elementary for every prime p, by splitting it as the product of its p-part and its p'-part.

The second half of the file builds the p-elementary subgroups that carry arithmetic information. For a finite-order element x and a prime p, a suitable Sylow p-subgroup of the centraliser of the p-free part s of x yields a join with ⟨s⟩ that contains x. Every such join is p-elementary, and when the Sylow subgroup has finite index in the centraliser the join has index prime to p there. The cyclic subgroups are already elementary, so it is this larger subgroup, not ⟨x⟩, that carries content.

Main definitions

• TauCeti.IsPElementary p G: G is the internal direct product of a cyclic subgroup of order prime to p and a p-subgroup.
• TauCeti.IsPHyperelementary p G: G has a cyclic normal subgroup of order prime to p with p-group quotient.
• TauCeti.IsElementary G, TauCeti.IsHyperelementary G: the same, for some prime p.
• TauCeti.pElementaryOfSylow s P: for an element s of order prime to p and a Sylow p-subgroup P of the centraliser of s, the subgroup of G generated by s together with P.
• TauCeti.pFreePartHom s P: the p-free part as a homomorphism from that subgroup onto its cyclic factor ⟨s⟩, the projection along which class functions of ⟨s⟩ are pulled back.

Each of the four predicates is restated as an Iff by TauCeti.isPElementary_def, TauCeti.isPHyperelementary_def, TauCeti.isElementary_def and TauCeti.isHyperelementary_def.

Main results

• TauCeti.isPElementary_of_isCyclic: every finite cyclic group is p-elementary, for every prime p; hence TauCeti.isElementary_of_isCyclic, cyclic groups are elementary.
• TauCeti.IsPElementary.isPHyperelementary: p-elementary groups are p-hyperelementary.
• TauCeti.IsPElementary.of_injective, TauCeti.IsPHyperelementary.of_injective: both classes are closed under passing to a subgroup, in the form of an injective homomorphism into the group. The subgroup forms are TauCeti.IsPElementary.subgroup and TauCeti.IsPHyperelementary.subgroup.
• TauCeti.IsHyperelementary.isSolvable: a finite hyperelementary group is solvable, whence TauCeti.not_isElementary_perm_fin_5, the symmetric group on five letters is not elementary.
• TauCeti.IsElementary.isNilpotent: a finite elementary group is nilpotent, its cyclic factor being central.
• TauCeti.isPElementary_sup_of_commute: a cyclic subgroup of order prime to p and a p-subgroup that centralises it generate a p-elementary subgroup, and TauCeti.disjoint_of_not_dvd_natCard_of_isPGroup supplies the disjointness it asks for.
• TauCeti.isPElementary_pElementaryOfSylow and TauCeti.not_dvd_relIndex_pElementaryOfSylow: TauCeti.pElementaryOfSylow s P is p-elementary, and, provided P has finite index in the centraliser of s, its index there is prime to p.
• TauCeti.exists_mem_pElementaryOfSylow: every element x lies in TauCeti.pElementaryOfSylow of its p-free part, for a suitable Sylow p-subgroup.
• TauCeti.pFreePart_mem_zpowers_of_mem_pElementaryOfSylow and TauCeti.pPart_mem_map_sylow_of_mem_pElementaryOfSylow: the p-free part and the p-part of an element of TauCeti.pElementaryOfSylow s P lie in its cyclic and its Sylow factor, and TauCeti.pFreePart_mul_of_mem_pElementaryOfSylow: the p-free part is multiplicative there.

Implementation notes

The p-group condition on the quotient in TauCeti.IsPHyperelementary is spelled out elementwise, as ∀ g, ∃ k, g ^ p ^ k ∈ C, rather than as IsPGroup p (G ⧸ C). The two are equivalent (TauCeti.isPHyperelementary_iff_isPGroup_quotient, and the two implications it is assembled from, TauCeti.isPGroup_quotient_of_forall_exists_pow_mem and TauCeti.isPHyperelementary_of_isPGroup_quotient), but the quotient G ⧸ C is a group only once the normality of C is available as an instance, which an existential quantifier inside the definition cannot supply. The elementwise form keeps the definition free of that bookkeeping and is also the form the closure proofs use directly.

TauCeti.IsPElementary records the internal direct product decomposition as Subgroup.IsComplement' together with elementwise commutation, rather than as normality of both factors: this is the form the proofs consume, and normality of the cyclic factor is derived from it in TauCeti.normal_of_commute_of_sup_eq_top.

TauCeti.pElementaryOfSylow takes the Sylow subgroup as an argument instead of choosing one: a centraliser has in general several Sylow p-subgroups, and everything proved about the resulting subgroup holds for each of them. TauCeti.exists_mem_pElementaryOfSylow makes the choice that puts a prescribed element inside.

References

This supplies a prerequisite for TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md, Layer 6 ("Elementary and hyperelementary subgroups"), which asks for exactly these two predicates "from these orientations, with their basic closure properties", as the indexing sets of Artin's and Brauer's induction theorems.

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

def TauCeti.IsPElementary (p : ℕ) (G : Type u_1) [Group G] : Prop

A group G is p-elementary when it is the internal direct product of a cyclic subgroup of order prime to p and a p-subgroup: there are subgroups C and P of G with C cyclic of order prime to p, P a p-group, every element of C commuting with every element of P, and C a complement of P.

def TauCeti.IsPHyperelementary (p : ℕ) (G : Type u_1) [Group G] : Prop

A group G is p-hyperelementary when it has a cyclic normal subgroup C of order prime to p whose quotient G ⧸ C is a p-group. The condition on the quotient is spelled elementwise, as ∀ g, ∃ k, g ^ p ^ k ∈ C; see TauCeti.isPGroup_quotient_of_forall_exists_pow_mem for the identification with IsPGroup p (G ⧸ C).

def TauCeti.IsElementary (G : Type u_1) [Group G] : Prop

A group is elementary when it is p-elementary for some prime p.

def TauCeti.IsHyperelementary (G : Type u_1) [Group G] : Prop

A group is hyperelementary when it is p-hyperelementary for some prime p.

Restating the definitions

The four definitions above are public but not @[expose], so downstream modules see their statements and not their bodies: neither unfold IsPElementary nor simp only [IsPElementary] is available there. The Iff.rfl lemmas in this section are therefore the only way to eliminate the predicates outside this file, as Subgroup.isComplement'_def is for Subgroup.IsComplement' and isPrimePow_def is for IsPrimePow.

theorem TauCeti.isPElementary_def {p : ℕ} {G : Type u_1} [Group G] : IsPElementary p G ↔ ∃ (C : Subgroup G) (P : Subgroup G), IsCyclic ↥C ∧ ¬p ∣ Nat.card ↥C ∧ IsPGroup p ↥P ∧ (∀ c ∈ C, ∀ x ∈ P, Commute c x) ∧ C.IsComplement' P

TauCeti.IsPElementary p G unfolded: a decomposition of G into a cyclic subgroup of order prime to p and a complementary p-subgroup commuting with it elementwise.

theorem TauCeti.isPHyperelementary_def {p : ℕ} {G : Type u_1} [Group G] : IsPHyperelementary p G ↔ ∃ (C : Subgroup G), C.Normal ∧ IsCyclic ↥C ∧ ¬p ∣ Nat.card ↥C ∧ ∀ (g : G), ∃ (k : ℕ), g ^ p ^ k ∈ C

TauCeti.IsPHyperelementary p G unfolded: a cyclic normal subgroup of order prime to p such that every element of G has a p-power inside it. See TauCeti.isPHyperelementary_iff_isPGroup_quotient for the quotient reading of the last clause.

theorem TauCeti.isElementary_def {G : Type u_1} [Group G] : IsElementary G ↔ ∃ (q : ℕ), Nat.Prime q ∧ IsPElementary q G

TauCeti.IsElementary G unfolded: p-elementarity for some prime p.

theorem TauCeti.isHyperelementary_def {G : Type u_1} [Group G] : IsHyperelementary G ↔ ∃ (q : ℕ), Nat.Prime q ∧ IsPHyperelementary q G

TauCeti.IsHyperelementary G unfolded: p-hyperelementarity for some prime p.

The quotient form of hyperelementarity

theorem TauCeti.isPGroup_quotient_of_forall_exists_pow_mem {p : ℕ} {G : Type u_1} [Group G] {C : Subgroup G} [C.Normal] (h : ∀ (g : G), ∃ (k : ℕ), g ^ p ^ k ∈ C) : IsPGroup p (G ⧸ C)

If every element of G has a p-power lying in a normal subgroup C, the quotient G ⧸ C is a p-group. This is the quotient reading of the last clause of TauCeti.IsPHyperelementary.

theorem TauCeti.isPHyperelementary_of_isPGroup_quotient {p : ℕ} {G : Type u_1} [Group G] (C : Subgroup G) [hC : C.Normal] (h₁ : IsCyclic ↥C) (h₂ : ¬p ∣ Nat.card ↥C) (h₃ : IsPGroup p (G ⧸ C)) : IsPHyperelementary p G

A cyclic normal subgroup of order prime to p with p-group quotient exhibits G as p-hyperelementary.

theorem TauCeti.isPHyperelementary_iff_isPGroup_quotient {p : ℕ} {G : Type u_1} [Group G] : IsPHyperelementary p G ↔ ∃ (C : Subgroup G) (hC : C.Normal), IsCyclic ↥C ∧ ¬p ∣ Nat.card ↥C ∧ IsPGroup p (G ⧸ C)

G is p-hyperelementary exactly when it has a cyclic normal subgroup C of order prime to p with IsPGroup p (G ⧸ C). This is the quotient form of the definition, with the normality witness packaged so that it supplies the group structure on G ⧸ C.

Elementary groups are hyperelementary

theorem TauCeti.normal_of_commute_of_isComplement' {G : Type u_1} [Group G] {C P : Subgroup G} (hcomm : ∀ c ∈ C, ∀ x ∈ P, Commute c x) (hcompl : C.IsComplement' P) : C.Normal

A subgroup centralised elementwise by a complement is normal: the complement form of TauCeti.normal_of_commute_of_sup_eq_top, matching the shape in which TauCeti.IsPElementary records its decomposition.

theorem TauCeti.exists_pow_mem_of_isComplement' {p : ℕ} {G : Type u_1} [Group G] {C P : Subgroup G} (hP : IsPGroup p ↥P) (hcomm : ∀ c ∈ C, ∀ x ∈ P, Commute c x) (hcompl : C.IsComplement' P) (g : G) : ∃ (k : ℕ), g ^ p ^ k ∈ C

If C and a p-subgroup P are complements centralising each other, every element of G has a p-power in C: write it as a * b with a ∈ C, b ∈ P, and kill b.

theorem TauCeti.IsPElementary.isPHyperelementary {p : ℕ} {G : Type u_1} [Group G] (h : IsPElementary p G) : IsPHyperelementary p G

A p-elementary group is p-hyperelementary: the cyclic factor is normal, and the quotient by it is the p-group factor.

theorem TauCeti.IsElementary.isHyperelementary {G : Type u_1} [Group G] (h : IsElementary G) : IsHyperelementary G

An elementary group is hyperelementary.

Basic examples

theorem TauCeti.isPElementary_of_isPGroup {p : ℕ} {G : Type u_1} [Group G] (hp : p ≠ 1) (h : IsPGroup p G) : IsPElementary p G

A p-group is p-elementary, with trivial cyclic factor.

theorem TauCeti.isPElementary_of_isCyclic {G : Type u_1} [Group G] [Finite G] [IsCyclic G] (p : ℕ) [Fact (Nat.Prime p)] : IsPElementary p G

A finite cyclic group is p-elementary for every prime p: writing Nat.card G as p ^ a * m with p ∤ m and taking a generator g, the subgroup generated by g ^ (p ^ a) is cyclic of order m and the subgroup generated by g ^ m is a p-group of order p ^ a, and the two are complementary because their orders are coprime.

So the elementary subgroups of a finite group include all its cyclic subgroups: Brauer's induction theorem, indexed by elementary subgroups, refines Artin's, indexed by cyclic ones.

theorem TauCeti.isElementary_of_isCyclic {G : Type u_1} [Group G] [Finite G] [IsCyclic G] : IsElementary G

A finite cyclic group is elementary.

theorem TauCeti.isHyperelementary_of_isCyclic {G : Type u_1} [Group G] [Finite G] [IsCyclic G] : IsHyperelementary G

A finite cyclic group is hyperelementary.

Closure under subgroups

theorem TauCeti.IsPHyperelementary.of_injective {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [Group H] (h : IsPHyperelementary p G) (f : H →* G) (hf : Function.Injective ⇑f) : IsPHyperelementary p H

p-hyperelementarity passes to subgroups, in the form of an injective homomorphism into the group.

theorem TauCeti.IsPElementary.of_injective {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Fact (Nat.Prime p)] (h : IsPElementary p G) (f : H →* G) (hf : Function.Injective ⇑f) : IsPElementary p H

p-elementarity passes to subgroups, in the form of an injective homomorphism into the group.

The decomposition of a subgroup is inherited factor by factor: the crux is that the subgroup is still the product of the two intersections, which follows via TauCeti.exists_zpow_mul_zpow_eq_of_coprime from a Bézout identity between the orders of the two factors, coprime because one is prime to p and the other is a power of p.

theorem TauCeti.IsPHyperelementary.subgroup {p : ℕ} {G : Type u_1} [Group G] (h : IsPHyperelementary p G) (K : Subgroup G) : IsPHyperelementary p ↥K

p-hyperelementarity passes to subgroups.

theorem TauCeti.IsPElementary.subgroup {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] (h : IsPElementary p G) (K : Subgroup G) : IsPElementary p ↥K

p-elementarity passes to subgroups.

theorem TauCeti.IsHyperelementary.subgroup {G : Type u_1} [Group G] (h : IsHyperelementary G) (K : Subgroup G) : IsHyperelementary ↥K

Hyperelementarity passes to subgroups.

theorem TauCeti.IsElementary.subgroup {G : Type u_1} [Group G] (h : IsElementary G) (K : Subgroup G) : IsElementary ↥K

Elementarity passes to subgroups.

Solvability

theorem TauCeti.IsPHyperelementary.isSolvable {p : ℕ} {G : Type u_1} [Group G] [Finite G] [Fact (Nat.Prime p)] (h : IsPHyperelementary p G) : Group.IsSolvable G

A finite p-hyperelementary group is solvable: the cyclic normal subgroup C supplied by the definition is abelian, hence solvable, and the quotient G ⧸ C is a p-group, hence nilpotent and so solvable too.

theorem TauCeti.IsHyperelementary.isSolvable {G : Type u_1} [Group G] [Finite G] (h : IsHyperelementary G) : Group.IsSolvable G

A finite hyperelementary group is solvable.

theorem TauCeti.IsElementary.isSolvable {G : Type u_1} [Group G] [Finite G] (h : IsElementary G) : Group.IsSolvable G

A finite elementary group is solvable.

theorem TauCeti.IsPElementary.isNilpotent {p : ℕ} {G : Type u_1} [Group G] [Finite G] [Fact (Nat.Prime p)] (h : IsPElementary p G) : Group.IsNilpotent G

A finite p-elementary group is nilpotent: the cyclic factor C is central, being commutative and centralised by the p-group factor, and G ⧸ C is a p-group.

theorem TauCeti.IsElementary.isNilpotent {G : Type u_1} [Group G] [Finite G] (h : IsElementary G) : Group.IsNilpotent G

A finite elementary group is nilpotent.

theorem TauCeti.not_isHyperelementary_perm_fin_5 : ¬IsHyperelementary (Equiv.Perm (Fin 5))

The symmetric group on five letters is not hyperelementary, since it is not solvable. Together with TauCeti.isElementary_of_isCyclic this pins the two predicates between the cyclic groups and the solvable ones.

theorem TauCeti.not_isElementary_perm_fin_5 : ¬IsElementary (Equiv.Perm (Fin 5))

The symmetric group on five letters is not elementary.

p-elementary subgroups built from a Sylow subgroup of a centraliser

The cyclic subgroups of a finite group are already elementary, so they witness nothing beyond TauCeti.isPElementary_of_isCyclic. What Brauer's induction theorem needs is a large elementary subgroup attached to an element: for x : G with p-free part s, some suitable Sylow p-subgroup of the centraliser of s yields a join with ⟨s⟩ that contains x. Every such join is p-elementary, and as soon as the Sylow subgroup has finite index in that centraliser the join has relative index prime to p there, which is the arithmetic the induction theorem runs on.

theorem TauCeti.isPElementary_sup_of_commute {p : ℕ} {G : Type u_1} [Group G] {C Q : Subgroup G} (hC : IsCyclic ↥C) (hCp : ¬p ∣ Nat.card ↥C) (hQ : IsPGroup p ↥Q) (hdisj : Disjoint C Q) (hcomm : ∀ c ∈ C, ∀ y ∈ Q, Commute c y) : IsPElementary p ↥(C ⊔ Q)

Two subgroups centralising one another, one cyclic of order prime to p and one a p-group, generate a p-elementary subgroup.

noncomputable def TauCeti.pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) : Subgroup G

The p-elementary subgroup attached to an element s of order prime to p together with a Sylow p-subgroup P of the centraliser of s: the join of the cyclic group generated by s with P. It is p-elementary by TauCeti.isPElementary_pElementaryOfSylow, and, when P has finite index in the centraliser, its relative index there is prime to p by TauCeti.not_dvd_relIndex_pElementaryOfSylow.

theorem TauCeti.zpowers_le_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) : Subgroup.zpowers s ≤ pElementaryOfSylow s P

theorem TauCeti.self_mem_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) : s ∈ pElementaryOfSylow s P

theorem TauCeti.map_sylow_le_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) : Subgroup.map (Subgroup.centralizer {s}).subtype ↑P ≤ pElementaryOfSylow s P

@[simp]

theorem TauCeti.pElementaryOfSylow_le_iff {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) {K : Subgroup G} : pElementaryOfSylow s P ≤ K ↔ s ∈ K ∧ Subgroup.map (Subgroup.centralizer {s}).subtype ↑P ≤ K

theorem TauCeti.pElementaryOfSylow_le_centralizer {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) : pElementaryOfSylow s P ≤ Subgroup.centralizer {s}

theorem TauCeti.commute_of_mem_zpowers_of_mem_centralizer {G : Type u_1} [Group G] (s : G) {c y : G} (hc : c ∈ Subgroup.zpowers s) (hy : y ∈ Subgroup.centralizer {s}) : Commute c y

Every element of ⟨s⟩ commutes with every element centralising s.

theorem TauCeti.isPElementary_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) : IsPElementary p ↥(pElementaryOfSylow s P)

The subgroup attached to a p-regular element and a Sylow p-subgroup of its centraliser is indeed p-elementary.

theorem TauCeti.not_dvd_relIndex_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) [Fact (Nat.Prime p)] [(↑P).FiniteIndex] : ¬p ∣ (pElementaryOfSylow s P).relIndex (Subgroup.centralizer {s})

The subgroup attached to a p-regular element s and a Sylow p-subgroup P of finite index in its centraliser has index prime to p inside that centraliser: it contains a full Sylow p-subgroup.

theorem TauCeti.exists_mul_eq_of_mem_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) {x : G} (hx : x ∈ pElementaryOfSylow s P) : ∃ c ∈ Subgroup.zpowers s, ∃ y ∈ Subgroup.map (Subgroup.centralizer {s}).subtype ↑P, Commute c y ∧ c * y = x

An element of the subgroup attached to s and P factors through the Sylow subgroup. Every element of TauCeti.pElementaryOfSylow s P is a power of s times an element of the image of P, and the two factors commute.

theorem TauCeti.pPart_mem_map_sylow_of_mem_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) {x : G} (hx : x ∈ pElementaryOfSylow s P) : pPart p x ∈ Subgroup.map (Subgroup.centralizer {s}).subtype ↑P

The p-part of an element of TauCeti.pElementaryOfSylow s P lies in its Sylow factor. The factorisation of TauCeti.exists_mul_eq_of_mem_pElementaryOfSylow splits the element into a factor of order prime to p and a p-element, so it is the factorisation of TauCeti.eq_pPart.

theorem TauCeti.pFreePart_mem_zpowers_of_mem_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) {x : G} (hx : x ∈ pElementaryOfSylow s P) : pFreePart p x ∈ Subgroup.zpowers s

The p-free part of an element of TauCeti.pElementaryOfSylow s P lies in its cyclic factor ⟨s⟩. This is the other half of the factorisation TauCeti.exists_mul_eq_of_mem_pElementaryOfSylow, read through TauCeti.eq_pFreePart.

theorem TauCeti.pFreePart_mul_of_mem_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) (hs : ¬p ∣ orderOf s) {x y : G} (hx : x ∈ pElementaryOfSylow s P) (hy : y ∈ pElementaryOfSylow s P) : pFreePart p (x * y) = pFreePart p x * pFreePart p y

The p-free part is multiplicative on TauCeti.pElementaryOfSylow s P. The cyclic factor is central in the subgroup, so the product of two elements factors as the product of their p-free parts times the product of their p-parts, and that is again a commuting factorisation of the kind TauCeti.eq_pFreePart recognises.

noncomputable def TauCeti.pFreePartHom {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) : ↥(pElementaryOfSylow s P) →* ↥(Subgroup.zpowers s)

The p-free part as a homomorphism from TauCeti.pElementaryOfSylow s P onto its cyclic factor ⟨s⟩. It is the projection of the direct product ⟨s⟩ × P onto its first factor, the one along which class functions of ⟨s⟩ are pulled back to the p-elementary subgroup.

@[simp]

theorem TauCeti.coe_pFreePartHom_apply {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) (x : ↥(pElementaryOfSylow s P)) : ↑((pFreePartHom s P hs) x) = pFreePart p ↑x

@[simp]

theorem TauCeti.pFreePartHom_inclusion_apply {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) (c : ↥(Subgroup.zpowers s)) : (pFreePartHom s P hs) ((Subgroup.inclusion ⋯) c) = c

The p-free-part projection is the identity on the cyclic factor.

theorem TauCeti.pFreePartHom_surjective {p : ℕ} {G : Type u_1} [Group G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) : Function.Surjective ⇑(pFreePartHom s P hs)

The p-free-part projection maps onto the cyclic factor.

Membership of an element

Every element lies in the p-elementary subgroup built from its p-free part.

theorem TauCeti.exists_mem_pElementaryOfSylow {p : ℕ} {G : Type u_1} [Group G] (x : G) : ∃ (P : Sylow p ↥(Subgroup.centralizer {pFreePart p x})), x ∈ pElementaryOfSylow (pFreePart p x) P

For every p and every element x, some Sylow p-subgroup of the centraliser of the p-free part of x produces, by TauCeti.pElementaryOfSylow, a subgroup containing x. When p is prime and x has finite order, so that p does not divide the order of TauCeti.pFreePart p x, that subgroup is p-elementary by TauCeti.isPElementary_pElementaryOfSylow, and when moreover the Sylow subgroup has finite index in the centraliser, which is not asserted here, TauCeti.not_dvd_relIndex_pElementaryOfSylow gives the subgroup index prime to p there. For p not prime or x of infinite order the p-free part is x itself and any Sylow subgroup works, with no p-elementary conclusion.