p-groups

This file contains a proof that if G is a p-group acting on a finite set α, then the number of fixed points of the action is congruent mod p to the cardinality of α. It also contains proofs of some corollaries of this lemma about existence of fixed points.

def IsPGroup (p : ℕ) (G : Type u_1) [Group G] : Prop

A p-group is a group in which the order of every element is a power of p.

Equations

• IsPGroup p G = ∀ (g : G), ∃ (k : ℕ), g ^ p ^ k = 1

theorem isPGroup_iff_pow_pow_eq_one {p : ℕ} {G : Type u_1} [Group G] : IsPGroup p G ↔ ∀ (g : G), ∃ (k : ℕ), g ^ p ^ k = 1

theorem IsPGroup.exists_pow_pow_eq_one {p : ℕ} {G : Type u_1} [Group G] : IsPGroup p G → ∀ (g : G), ∃ (k : ℕ), g ^ p ^ k = 1

Alias of the forward direction of isPGroup_iff_pow_pow_eq_one.

theorem isPGroup_iff_orderOf_dvd_pow {p : ℕ} {G : Type u_1} [Group G] : IsPGroup p G ↔ ∀ (g : G), ∃ (k : ℕ), orderOf g ∣ p ^ k

theorem IsPGroup.exists_orderOf_dvd_pow {p : ℕ} {G : Type u_1} [Group G] : IsPGroup p G → ∀ (g : G), ∃ (k : ℕ), orderOf g ∣ p ^ k

Alias of the forward direction of isPGroup_iff_orderOf_dvd_pow.

theorem IsPGroup.iff_orderOf {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] : IsPGroup p G ↔ ∀ (g : G), ∃ (k : ℕ), orderOf g = p ^ k

theorem IsPGroup.exists_orderOf_eq_pow {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] : IsPGroup p G → ∀ (g : G), ∃ (k : ℕ), orderOf g = p ^ k

Alias of the forward direction of IsPGroup.iff_orderOf.

theorem IsPGroup.of_card_dvd_pow {p : ℕ} {G : Type u_1} [Group G] {n : ℕ} (hG : Nat.card G ∣ p ^ n) : IsPGroup p G

theorem isPGroup_iff_card_dvd_pow {p : ℕ} {G : Type u_1} [Group G] [Finite G] : IsPGroup p G ↔ ∃ (n : ℕ), Nat.card G ∣ p ^ n

theorem IsPGroup.exists_card_dvd_pow {p : ℕ} {G : Type u_1} [Group G] [Finite G] : IsPGroup p G → ∃ (n : ℕ), Nat.card G ∣ p ^ n

Alias of the forward direction of isPGroup_iff_card_dvd_pow.

theorem IsPGroup.dvd_orderOf {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] (hG : IsPGroup p G) {g : G} (hg : g ≠ 1) : p ∣ orderOf g

theorem IsPGroup.of_card {p : ℕ} {G : Type u_1} [Group G] {n : ℕ} (hG : Nat.card G = p ^ n) : IsPGroup p G

theorem IsPGroup.of_subsingleton (p : ℕ) (G : Type u_1) [Group G] [Subsingleton G] : IsPGroup p G

theorem IsPGroup.of_bot {p : ℕ} {G : Type u_1} [Group G] : IsPGroup p ↥⊥

@[simp]

theorem IsPGroup.zero (G : Type u_1) [Group G] : IsPGroup 0 G

@[simp]

theorem isPGroup_one_iff_subsingleton {G : Type u_1} [Group G] : IsPGroup 1 G ↔ Subsingleton G

theorem IsPGroup.card {G : Type u_1} [Group G] : IsPGroup (Nat.card G) G

theorem IsPGroup.mono {p : ℕ} {G : Type u_1} [Group G] {q : ℕ} (hpq : p ∣ q) (hp : IsPGroup p G) : IsPGroup q G

theorem IsPGroup.of_pow {p : ℕ} {G : Type u_1} [Group G] {n : ℕ} (h : IsPGroup (p ^ n) G) : IsPGroup p G

theorem IsPGroup.iff_card {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite G] : IsPGroup p G ↔ ∃ (n : ℕ), Nat.card G = p ^ n

theorem IsPGroup.exists_card_eq {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite G] : IsPGroup p G → ∃ (n : ℕ), Nat.card G = p ^ n

Alias of the forward direction of IsPGroup.iff_card.

theorem isPGroup_iff_exists_orderOf_dvd_pow {p : ℕ} {G : Type u_1} [Group G] [Finite G] : IsPGroup p G ↔ ∃ (k : ℕ), ∀ (g : G), orderOf g ∣ p ^ k

theorem isPGroup_iff_exists_pow_pow_eq_one {p : ℕ} {G : Type u_1} [Group G] [Finite G] : IsPGroup p G ↔ ∃ (k : ℕ), ∀ (g : G), g ^ p ^ k = 1

theorem IsPGroup.of_exponent_dvd_pow {p : ℕ} {G : Type u_1} [Group G] {n : ℕ} (h : Monoid.exponent G ∣ p ^ n) : IsPGroup p G

theorem isPGroup_iff_exponent_dvd_pow {p : ℕ} {G : Type u_1} [Group G] [Finite G] : IsPGroup p G ↔ ∃ (n : ℕ), Monoid.exponent G ∣ p ^ n

theorem IsPGroup.exists_exponent_dvd_pow {p : ℕ} {G : Type u_1} [Group G] [Finite G] : IsPGroup p G → ∃ (n : ℕ), Monoid.exponent G ∣ p ^ n

Alias of the forward direction of isPGroup_iff_exponent_dvd_pow.

theorem isPGroup_iff_exponent_eq_pow {p : ℕ} {G : Type u_1} [Group G] [Finite G] [Fact (Nat.Prime p)] : IsPGroup p G ↔ ∃ (n : ℕ), Monoid.exponent G = p ^ n

theorem IsPGroup.exists_exponent_eq_pow {p : ℕ} {G : Type u_1} [Group G] [Finite G] [Fact (Nat.Prime p)] : IsPGroup p G → ∃ (n : ℕ), Monoid.exponent G = p ^ n

Alias of the forward direction of isPGroup_iff_exponent_eq_pow.

theorem isPGroup_iff_isPGroup_prod_primeFactors {p : ℕ} {G : Type u_1} [Group G] (h : p ≠ 0) : IsPGroup p G ↔ IsPGroup (p.primeFactors.prod id) G

theorem isPGroup_iff_primeFactors_card_subset {p : ℕ} {G : Type u_1} [Group G] [Finite G] (h : p ≠ 0) : IsPGroup p G ↔ (Nat.card G).primeFactors ⊆ p.primeFactors

theorem IsPGroup.of_injective {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) {H : Type u_2} [Group H] (ϕ : H →* G) (hϕ : Function.Injective ⇑ϕ) : IsPGroup p H

theorem IsPGroup.to_subgroup {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) (H : Subgroup G) : IsPGroup p ↥H

theorem IsPGroup.of_surjective {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) {H : Type u_2} [Group H] (ϕ : G →* H) (hϕ : Function.Surjective ⇑ϕ) : IsPGroup p H

theorem IsPGroup.to_quotient {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) (H : Subgroup G) [H.Normal] : IsPGroup p (G ⧸ H)

theorem IsPGroup.of_equiv {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) {H : Type u_2} [Group H] (ϕ : G ≃* H) : IsPGroup p H

theorem IsPGroup.isOfFinOrder {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) (hp : p ≠ 0) (g : G) : IsOfFinOrder g

theorem IsPGroup.orderOf_coprime {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) {n : ℕ} (hn : p.Coprime n) (g : G) : (orderOf g).Coprime n

noncomputable def IsPGroup.powEquiv {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) {n : ℕ} (hn : p.Coprime n) : G ≃ G

If gcd(p,n) = 1, then the nth power map is a bijection.

Equations

• hG.powEquiv hn = { toFun := fun (x : G) => x ^ n, invFun := fun (g : G) => ↑((powCoprime ⋯).symm ⟨g, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem IsPGroup.powEquiv_apply {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) {n : ℕ} (hn : p.Coprime n) (g : G) : (hG.powEquiv hn) g = g ^ n

@[simp]

theorem IsPGroup.powEquiv_symm_apply {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) {n : ℕ} (hn : p.Coprime n) (g : G) : (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n

@[reducible, inline]

noncomputable abbrev IsPGroup.powEquiv' {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : ¬p ∣ n) : G ≃ G

If p ∤ n, then the nth power map is a bijection.

Equations

• hG.powEquiv' hn = hG.powEquiv ⋯

theorem IsPGroup.index {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] (H : Subgroup G) [H.FiniteIndex] : ∃ (n : ℕ), H.index = p ^ n

theorem IsPGroup.card_eq_or_dvd {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] : Nat.card G = 1 ∨ p ∣ Nat.card G

theorem IsPGroup.nontrivial_iff_card {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] [Finite G] : Nontrivial G ↔ ∃ n > 0, Nat.card G = p ^ n

theorem IsPGroup.card_orbit {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] {α : Type u_2} [MulAction G α] (a : α) [Finite ↑(MulAction.orbit G a)] : ∃ (n : ℕ), Nat.card ↑(MulAction.orbit G a) = p ^ n

theorem IsPGroup.card_modEq_card_fixedPoints {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] (α : Type u_2) [MulAction G α] [Finite α] : Nat.card α ≡ Nat.card ↑(MulAction.fixedPoints G α) [MOD p]

If G is a p-group acting on a finite set α, then the number of fixed points of the action is congruent mod p to the cardinality of α

theorem IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] (α : Type u_3) [MulAction G α] (hpα : ¬p ∣ Nat.card α) : (MulAction.fixedPoints G α).Nonempty

If a p-group acts on α and the cardinality of α is not a multiple of p then the action has a fixed point.

theorem IsPGroup.exists_fixed_point_of_prime_dvd_card_of_fixed_point {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] (α : Type u_2) [MulAction G α] [Finite α] (hpα : p ∣ Nat.card α) {a : α} (ha : a ∈ MulAction.fixedPoints G α) : ∃ b ∈ MulAction.fixedPoints G α, a ≠ b

If a p-group acts on α and the cardinality of α is a multiple of p, and the action has one fixed point, then it has another fixed point.

theorem IsPGroup.center_nontrivial {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] [Nontrivial G] [Finite G] : Nontrivial ↥(Subgroup.center G)

theorem IsPGroup.bot_lt_center {p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] [Nontrivial G] [Finite G] : ⊥ < Subgroup.center G

theorem IsPGroup.to_le {p : ℕ} {G : Type u_1} [Group G] {H K : Subgroup G} (hK : IsPGroup p ↥K) (hHK : H ≤ K) : IsPGroup p ↥H

theorem IsPGroup.to_inf_left {p : ℕ} {G : Type u_1} [Group G] {H K : Subgroup G} (hH : IsPGroup p ↥H) : IsPGroup p ↥(H ⊓ K)

theorem IsPGroup.to_inf_right {p : ℕ} {G : Type u_1} [Group G] {H K : Subgroup G} (hK : IsPGroup p ↥K) : IsPGroup p ↥(H ⊓ K)

theorem IsPGroup.map {p : ℕ} {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsPGroup p ↥H) {K : Type u_2} [Group K] (ϕ : G →* K) : IsPGroup p ↥(Subgroup.map ϕ H)

theorem IsPGroup.comap_of_ker_isPGroup {p : ℕ} {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsPGroup p ↥H) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : IsPGroup p ↥ϕ.ker) : IsPGroup p ↥(Subgroup.comap ϕ H)

theorem IsPGroup.ker_isPGroup_of_injective {p : ℕ} {G : Type u_1} [Group G] {K : Type u_2} [Group K] {ϕ : K →* G} (hϕ : Function.Injective ⇑ϕ) : IsPGroup p ↥ϕ.ker

theorem IsPGroup.comap_of_injective {p : ℕ} {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsPGroup p ↥H) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : Function.Injective ⇑ϕ) : IsPGroup p ↥(Subgroup.comap ϕ H)

theorem IsPGroup.comap_subtype {p : ℕ} {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsPGroup p ↥H) {K : Subgroup G} : IsPGroup p ↥(Subgroup.comap K.subtype H)

theorem IsPGroup.to_sup_of_normal_right {p : ℕ} {G : Type u_1} [Group G] {H K : Subgroup G} (hH : IsPGroup p ↥H) (hK : IsPGroup p ↥K) [K.Normal] : IsPGroup p ↥(H ⊔ K)

theorem IsPGroup.to_sup_of_normal_left {p : ℕ} {G : Type u_1} [Group G] {H K : Subgroup G} (hH : IsPGroup p ↥H) (hK : IsPGroup p ↥K) [H.Normal] : IsPGroup p ↥(H ⊔ K)

theorem IsPGroup.to_sup_of_normal_right' {p : ℕ} {G : Type u_1} [Group G] {H K : Subgroup G} (hH : IsPGroup p ↥H) (hK : IsPGroup p ↥K) (hHK : H ≤ Subgroup.normalizer ↑K) : IsPGroup p ↥(H ⊔ K)

theorem IsPGroup.to_sup_of_normal_left' {p : ℕ} {G : Type u_1} [Group G] {H K : Subgroup G} (hH : IsPGroup p ↥H) (hK : IsPGroup p ↥K) (hHK : K ≤ Subgroup.normalizer ↑H) : IsPGroup p ↥(H ⊔ K)

theorem IsPGroup.coprime_card_of_ne {G : Type u_1} [Group G] {G₂ : Type u_2} [Group G₂] (p₁ p₂ : ℕ) [hp₁ : Fact (Nat.Prime p₁)] [hp₂ : Fact (Nat.Prime p₂)] (hne : p₁ ≠ p₂) (H₁ : Subgroup G) (H₂ : Subgroup G₂) [Finite ↥H₁] [Finite ↥H₂] (hH₁ : IsPGroup p₁ ↥H₁) (hH₂ : IsPGroup p₂ ↥H₂) : (Nat.card ↥H₁).Coprime (Nat.card ↥H₂)

finite p-groups with different p have coprime orders

theorem IsPGroup.disjoint_of_coprime {G : Type u_1} [Group G] {p₁ p₂ : ℕ} {H₁ H₂ : Subgroup G} (hH₁ : IsPGroup p₁ ↥H₁) (hH₂ : IsPGroup p₂ ↥H₂) (h : p₁.Coprime p₂) : Disjoint H₁ H₂

theorem IsPGroup.disjoint_of_ne {G : Type u_1} [Group G] (p₁ p₂ : ℕ) [hp₁ : Fact (Nat.Prime p₁)] [hp₂ : Fact (Nat.Prime p₂)] (hne : p₁ ≠ p₂) (H₁ H₂ : Subgroup G) (hH₁ : IsPGroup p₁ ↥H₁) (hH₂ : IsPGroup p₂ ↥H₂) : Disjoint H₁ H₂

p-groups with different p are disjoint

theorem IsPGroup.le_or_disjoint_of_coprime {p : ℕ} {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] {P : Subgroup G} (hP : IsPGroup p ↥P) {H : Subgroup G} [H.Normal] (h_cop : (Nat.card ↥H).Coprime H.index) : P ≤ H ∨ Disjoint H P

theorem IsPGroup.card_center_eq_prime_pow {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] {n : ℕ} (hGpn : Nat.card G = p ^ n) (hn : 0 < n) : ∃ k > 0, Nat.card ↥(Subgroup.center G) = p ^ k

The cardinality of the center of a p-group is p ^ k where k is positive.

theorem IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] (hG : Nat.card G = p ^ 2) : IsCyclic (G ⧸ Subgroup.center G)

The quotient by the center of a group of cardinality p ^ 2 is cyclic.

theorem IsPGroup.isMulCommutative_of_card_eq_prime_sq {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] (hG : Nat.card G = p ^ 2) : IsMulCommutative G

A group of order p ^ 2 is commutative. See also IsPGroup.commGroupOfCardEqPrimeSq for the CommGroup instance.

@[instance_reducible]

def IsPGroup.commGroupOfCardEqPrimeSq {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] (hG : Nat.card G = p ^ 2) : CommGroup G

A group of order p ^ 2 is commutative. See also IsPGroup.commutative_of_card_eq_prime_sq for just the proof that ∀ a b, a * b = b * a

Equations

• IsPGroup.commGroupOfCardEqPrimeSq hG = commGroupOfCyclicCenterQuotient (QuotientGroup.mk' (Subgroup.center G)) ⋯

@[deprecated IsPGroup.isMulCommutative_of_card_eq_prime_sq (since := "2026-05-26")]

theorem IsPGroup.commutative_of_card_eq_prime_sq {p : ℕ} {G : Type u_1} [Group G] [Fact (Nat.Prime p)] (hG : Nat.card G = p ^ 2) (a b : G) : a * b = b * a

theorem ZModModule.isPGroup_multiplicative {n : ℕ} {G : Type u_2} [AddCommGroup G] [Module (ZMod n) G] : IsPGroup n (Multiplicative G)