mathlib3 documentation

group_theory.p_group

p-groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 is_p_group (p : ) (G : Type u_1) [group G] :
Prop

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

Equations
theorem is_p_group.iff_order_of {p : } {G : Type u_1} [group G] [hp : fact (nat.prime p)] :
is_p_group p G (g : G), (k : ), order_of g = p ^ k
theorem is_p_group.of_card {p : } {G : Type u_1} [group G] [fintype G] {n : } (hG : fintype.card G = p ^ n) :
theorem is_p_group.of_bot {p : } {G : Type u_1} [group G] :
theorem is_p_group.iff_card {p : } {G : Type u_1} [group G] [fact (nat.prime p)] [fintype G] :
theorem is_p_group.of_injective {p : } {G : Type u_1} [group G] (hG : is_p_group p G) {H : Type u_2} [group H] (ϕ : H →* G) (hϕ : function.injective ϕ) :
theorem is_p_group.to_subgroup {p : } {G : Type u_1} [group G] (hG : is_p_group p G) (H : subgroup G) :
theorem is_p_group.of_surjective {p : } {G : Type u_1} [group G] (hG : is_p_group p G) {H : Type u_2} [group H] (ϕ : G →* H) (hϕ : function.surjective ϕ) :
theorem is_p_group.to_quotient {p : } {G : Type u_1} [group G] (hG : is_p_group p G) (H : subgroup G) [H.normal] :
is_p_group p (G H)
theorem is_p_group.of_equiv {p : } {G : Type u_1} [group G] (hG : is_p_group p G) {H : Type u_2} [group H] (ϕ : G ≃* H) :
theorem is_p_group.order_of_coprime {p : } {G : Type u_1} [group G] (hG : is_p_group p G) {n : } (hn : p.coprime n) (g : G) :
noncomputable def is_p_group.pow_equiv {p : } {G : Type u_1} [group G] (hG : is_p_group p G) {n : } (hn : p.coprime n) :
G G

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

Equations
@[simp]
theorem is_p_group.pow_equiv_apply {p : } {G : Type u_1} [group G] (hG : is_p_group p G) {n : } (hn : p.coprime n) (g : G) :
(hG.pow_equiv hn) g = g ^ n
@[simp]
theorem is_p_group.pow_equiv_symm_apply {p : } {G : Type u_1} [group G] (hG : is_p_group p G) {n : } (hn : p.coprime n) (g : G) :
((hG.pow_equiv hn).symm) g = g ^ (order_of g).gcd_b n
@[reducible]
noncomputable def is_p_group.pow_equiv' {p : } {G : Type u_1} [group G] (hG : is_p_group 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
theorem is_p_group.index {p : } {G : Type u_1} [group G] (hG : is_p_group p G) [hp : fact (nat.prime p)] (H : subgroup G) [H.finite_index] :
(n : ), H.index = p ^ n
theorem is_p_group.card_eq_or_dvd {p : } {G : Type u_1} [group G] (hG : is_p_group p G) [hp : fact (nat.prime p)] :
theorem is_p_group.nontrivial_iff_card {p : } {G : Type u_1} [group G] (hG : is_p_group p G) [hp : fact (nat.prime p)] [fintype G] :
nontrivial G (n : ) (H : n > 0), fintype.card G = p ^ n
theorem is_p_group.card_orbit {p : } {G : Type u_1} [group G] (hG : is_p_group p G) [hp : fact (nat.prime p)] {α : Type u_2} [mul_action G α] (a : α) [fintype (mul_action.orbit G a)] :

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 α

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

theorem is_p_group.exists_fixed_point_of_prime_dvd_card_of_fixed_point {p : } {G : Type u_1} [group G] (hG : is_p_group p G) [hp : fact (nat.prime p)] (α : Type u_2) [mul_action G α] [fintype α] (hpα : p fintype.card α) {a : α} (ha : a mul_action.fixed_points G α) :
(b : α), b mul_action.fixed_points 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 is_p_group.center_nontrivial {p : } {G : Type u_1} [group G] (hG : is_p_group p G) [hp : fact (nat.prime p)] [nontrivial G] [finite G] :
theorem is_p_group.bot_lt_center {p : } {G : Type u_1} [group G] (hG : is_p_group p G) [hp : fact (nat.prime p)] [nontrivial G] [finite G] :
theorem is_p_group.to_le {p : } {G : Type u_1} [group G] {H K : subgroup G} (hK : is_p_group p K) (hHK : H K) :
theorem is_p_group.to_inf_left {p : } {G : Type u_1} [group G] {H K : subgroup G} (hH : is_p_group p H) :
theorem is_p_group.to_inf_right {p : } {G : Type u_1} [group G] {H K : subgroup G} (hK : is_p_group p K) :
theorem is_p_group.map {p : } {G : Type u_1} [group G] {H : subgroup G} (hH : is_p_group p H) {K : Type u_2} [group K] (ϕ : G →* K) :
theorem is_p_group.comap_of_ker_is_p_group {p : } {G : Type u_1} [group G] {H : subgroup G} (hH : is_p_group p H) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : is_p_group p (ϕ.ker)) :
theorem is_p_group.ker_is_p_group_of_injective {p : } {G : Type u_1} [group G] {K : Type u_2} [group K] {ϕ : K →* G} (hϕ : function.injective ϕ) :
theorem is_p_group.comap_of_injective {p : } {G : Type u_1} [group G] {H : subgroup G} (hH : is_p_group p H) {K : Type u_2} [group K] (ϕ : K →* G) (hϕ : function.injective ϕ) :
theorem is_p_group.comap_subtype {p : } {G : Type u_1} [group G] {H : subgroup G} (hH : is_p_group p H) {K : subgroup G} :
theorem is_p_group.to_sup_of_normal_right {p : } {G : Type u_1} [group G] {H K : subgroup G} (hH : is_p_group p H) (hK : is_p_group p K) [K.normal] :
theorem is_p_group.to_sup_of_normal_left {p : } {G : Type u_1} [group G] {H K : subgroup G} (hH : is_p_group p H) (hK : is_p_group p K) [H.normal] :
theorem is_p_group.to_sup_of_normal_right' {p : } {G : Type u_1} [group G] {H K : subgroup G} (hH : is_p_group p H) (hK : is_p_group p K) (hHK : H K.normalizer) :
theorem is_p_group.to_sup_of_normal_left' {p : } {G : Type u_1} [group G] {H K : subgroup G} (hH : is_p_group p H) (hK : is_p_group p K) (hHK : K H.normalizer) :
theorem is_p_group.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₂) [fintype H₁] [fintype H₂] (hH₁ : is_p_group p₁ H₁) (hH₂ : is_p_group p₂ H₂) :

finite p-groups with different p have coprime orders

theorem is_p_group.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₁ : is_p_group p₁ H₁) (hH₂ : is_p_group p₂ H₂) :
disjoint H₁ H₂

p-groups with different p are disjoint

theorem is_p_group.card_center_eq_prime_pow {p : } {G : Type u_1} [group G] [fintype G] [fact (nat.prime p)] {n : } (hGpn : fintype.card G = p ^ n) (hn : 0 < n) [fintype (subgroup.center G)] :
(k : ) (H : k > 0), fintype.card (subgroup.center G) = p ^ k

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

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

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

Equations
theorem is_p_group.commutative_of_card_eq_prime_sq {p : } {G : Type u_1} [group G] [fintype G] [fact (nat.prime p)] (hG : fintype.card G = p ^ 2) (a b : G) :
a * b = b * a

A group of order p ^ 2 is commutative. See also is_p_group.comm_group_of_card_eq_prime_sq for the comm_group instance.