# Documentation

Mathlib.GroupTheory.PGroup

# 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) [] :

A p-group is a group in which every element has prime power order

Instances For
theorem IsPGroup.iff_orderOf {p : } {G : Type u_1} [] [hp : Fact ()] :
IsPGroup p G ∀ (g : G), k, = p ^ k
theorem IsPGroup.of_card {p : } {G : Type u_1} [] [] {n : } (hG : = p ^ n) :
theorem IsPGroup.of_bot {p : } {G : Type u_1} [] :
IsPGroup p { x // x }
theorem IsPGroup.iff_card {p : } {G : Type u_1} [] [Fact ()] [] :
IsPGroup p G n, = p ^ n
theorem IsPGroup.of_injective {p : } {G : Type u_1} [] (hG : IsPGroup p G) {H : Type u_2} [] (ϕ : H →* G) (hϕ : ) :
theorem IsPGroup.to_subgroup {p : } {G : Type u_1} [] (hG : IsPGroup p G) (H : ) :
IsPGroup p { x // x H }
theorem IsPGroup.of_surjective {p : } {G : Type u_1} [] (hG : IsPGroup p G) {H : Type u_2} [] (ϕ : G →* H) (hϕ : ) :
theorem IsPGroup.to_quotient {p : } {G : Type u_1} [] (hG : IsPGroup p G) (H : ) [] :
IsPGroup p (G H)
theorem IsPGroup.of_equiv {p : } {G : Type u_1} [] (hG : IsPGroup p G) {H : Type u_2} [] (ϕ : G ≃* H) :
theorem IsPGroup.orderOf_coprime {p : } {G : Type u_1} [] (hG : IsPGroup p G) {n : } (hn : ) (g : G) :
noncomputable def IsPGroup.powEquiv {p : } {G : Type u_1} [] (hG : IsPGroup p G) {n : } (hn : ) :
G G

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

Instances For
@[simp]
theorem IsPGroup.powEquiv_apply {p : } {G : Type u_1} [] (hG : IsPGroup p G) {n : } (hn : ) (g : G) :
↑() g = g ^ n
@[simp]
theorem IsPGroup.powEquiv_symm_apply {p : } {G : Type u_1} [] (hG : IsPGroup p G) {n : } (hn : ) (g : G) :
().symm g = g ^ Nat.gcdB () n
@[reducible]
noncomputable def IsPGroup.powEquiv' {p : } {G : Type u_1} [] (hG : IsPGroup p G) [hp : Fact ()] {n : } (hn : ¬p n) :
G G

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

Instances For
theorem IsPGroup.index {p : } {G : Type u_1} [] (hG : IsPGroup p G) [hp : Fact ()] (H : ) :
n, = p ^ n
theorem IsPGroup.card_eq_or_dvd {p : } {G : Type u_1} [] (hG : IsPGroup p G) [hp : Fact ()] :
= 1 p
theorem IsPGroup.nontrivial_iff_card {p : } {G : Type u_1} [] (hG : IsPGroup p G) [hp : Fact ()] [] :
n, n > 0 = p ^ n
theorem IsPGroup.card_orbit {p : } {G : Type u_1} [] (hG : IsPGroup p G) [hp : Fact ()] {α : Type u_2} [] (a : α) [Fintype ↑()] :
n, Fintype.card ↑() = p ^ n
theorem IsPGroup.card_modEq_card_fixedPoints {p : } {G : Type u_1} [] (hG : IsPGroup p G) [hp : Fact ()] (α : Type u_2) [] [] [Fintype ↑()] :

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} [] (hG : IsPGroup p G) [hp : Fact ()] (α : Type u_2) [] [] (hpα : ¬) [Finite ↑()] :

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} [] (hG : IsPGroup p G) [hp : Fact ()] (α : Type u_2) [] [] (hpα : ) {a : α} (ha : ) :
b, 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} [] (hG : IsPGroup p G) [hp : Fact ()] [] [] :
Nontrivial { x // }
theorem IsPGroup.bot_lt_center {p : } {G : Type u_1} [] (hG : IsPGroup p G) [hp : Fact ()] [] [] :
theorem IsPGroup.to_le {p : } {G : Type u_1} [] {H : } {K : } (hK : IsPGroup p { x // x K }) (hHK : H K) :
IsPGroup p { x // x H }
theorem IsPGroup.to_inf_left {p : } {G : Type u_1} [] {H : } {K : } (hH : IsPGroup p { x // x H }) :
IsPGroup p { x // x H K }
theorem IsPGroup.to_inf_right {p : } {G : Type u_1} [] {H : } {K : } (hK : IsPGroup p { x // x K }) :
IsPGroup p { x // x H K }
theorem IsPGroup.map {p : } {G : Type u_1} [] {H : } (hH : IsPGroup p { x // x H }) {K : Type u_2} [] (ϕ : G →* K) :
IsPGroup p { x // x }
theorem IsPGroup.comap_of_ker_isPGroup {p : } {G : Type u_1} [] {H : } (hH : IsPGroup p { x // x H }) {K : Type u_2} [] (ϕ : K →* G) (hϕ : IsPGroup p { x // }) :
IsPGroup p { x // x }
theorem IsPGroup.ker_isPGroup_of_injective {p : } {G : Type u_1} [] {K : Type u_2} [] {ϕ : K →* G} (hϕ : ) :
IsPGroup p { x // }
theorem IsPGroup.comap_of_injective {p : } {G : Type u_1} [] {H : } (hH : IsPGroup p { x // x H }) {K : Type u_2} [] (ϕ : K →* G) (hϕ : ) :
IsPGroup p { x // x }
theorem IsPGroup.comap_subtype {p : } {G : Type u_1} [] {H : } (hH : IsPGroup p { x // x H }) {K : } :
IsPGroup p { x // x }
theorem IsPGroup.to_sup_of_normal_right {p : } {G : Type u_1} [] {H : } {K : } (hH : IsPGroup p { x // x H }) (hK : IsPGroup p { x // x K }) [] :
IsPGroup p { x // x H K }
theorem IsPGroup.to_sup_of_normal_left {p : } {G : Type u_1} [] {H : } {K : } (hH : IsPGroup p { x // x H }) (hK : IsPGroup p { x // x K }) [] :
IsPGroup p { x // x H K }
theorem IsPGroup.to_sup_of_normal_right' {p : } {G : Type u_1} [] {H : } {K : } (hH : IsPGroup p { x // x H }) (hK : IsPGroup p { x // x K }) (hHK : ) :
IsPGroup p { x // x H K }
theorem IsPGroup.to_sup_of_normal_left' {p : } {G : Type u_1} [] {H : } {K : } (hH : IsPGroup p { x // x H }) (hK : IsPGroup p { x // x K }) (hHK : ) :
IsPGroup p { x // x H K }
theorem IsPGroup.coprime_card_of_ne {G : Type u_1} [] {G₂ : Type u_2} [Group G₂] (p₁ : ) (p₂ : ) [hp₁ : Fact ()] [hp₂ : Fact ()] (hne : p₁ p₂) (H₁ : ) (H₂ : Subgroup G₂) [Fintype { x // x H₁ }] [Fintype { x // x H₂ }] (hH₁ : IsPGroup p₁ { x // x H₁ }) (hH₂ : IsPGroup p₂ { x // x H₂ }) :
Nat.Coprime (Fintype.card { x // x H₁ }) (Fintype.card { x // x H₂ })

finite p-groups with different p have coprime orders

theorem IsPGroup.disjoint_of_ne {G : Type u_1} [] (p₁ : ) (p₂ : ) [hp₁ : Fact ()] [hp₂ : Fact ()] (hne : p₁ p₂) (H₁ : ) (H₂ : ) (hH₁ : IsPGroup p₁ { x // x H₁ }) (hH₂ : IsPGroup p₂ { x // x H₂ }) :
Disjoint H₁ H₂

p-groups with different p are disjoint

theorem IsPGroup.card_center_eq_prime_pow {p : } {G : Type u_1} [] [] [Fact ()] {n : } (hGpn : = p ^ n) (hn : 0 < n) [Fintype { x // }] :
k, k > 0 Fintype.card { x // } = 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} [] [] [Fact ()] (hG : = p ^ 2) :

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

def IsPGroup.commGroupOfCardEqPrimeSq {p : } {G : Type u_1} [] [] [Fact ()] (hG : = p ^ 2) :

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

Instances For
theorem IsPGroup.commutative_of_card_eq_prime_sq {p : } {G : Type u_1} [] [] [Fact ()] (hG : = p ^ 2) (a : G) (b : G) :
a * b = b * a

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