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.
theorem
is_p_group.of_card
{p : ℕ}
{G : Type u_1}
[group G]
[fintype G]
{n : ℕ}
(hG : fintype.card G = p ^ n) :
is_p_group p 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 ⇑ϕ) :
is_p_group p H
theorem
is_p_group.to_subgroup
{p : ℕ}
{G : Type u_1}
[group G]
(hG : is_p_group p G)
(H : subgroup G) :
is_p_group p ↥H
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 ⇑ϕ) :
is_p_group p H
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) :
is_p_group p 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.
@[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
- hG.pow_equiv' hn = hG.pow_equiv _
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)] :
∃ (n : ℕ), fintype.card ↥(mul_action.orbit G a) = p ^ n
theorem
is_p_group.card_modeq_card_fixed_points
{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 α]
[fintype ↥(mul_action.fixed_points G α)] :
fintype.card α ≡ fintype.card ↥(mul_action.fixed_points 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
is_p_group.nonempty_fixed_point_of_prime_not_dvd_card
{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 α)
[finite ↥(mul_action.fixed_points G α)] :
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 α) :
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) :
is_p_group p ↥H
theorem
is_p_group.to_inf_left
{p : ℕ}
{G : Type u_1}
[group G]
{H K : subgroup G}
(hH : is_p_group p ↥H) :
is_p_group p ↥(H ⊓ K)
theorem
is_p_group.to_inf_right
{p : ℕ}
{G : Type u_1}
[group G]
{H K : subgroup G}
(hK : is_p_group p ↥K) :
is_p_group p ↥(H ⊓ 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) :
is_p_group p ↥(subgroup.map ϕ H)
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)) :
is_p_group p ↥(subgroup.comap ϕ H)
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 ⇑ϕ) :
is_p_group p ↥(ϕ.ker)
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 ⇑ϕ) :
is_p_group p ↥(subgroup.comap ϕ H)
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} :
is_p_group p ↥(subgroup.comap K.subtype H)
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] :
is_p_group p ↥(H ⊔ K)
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] :
is_p_group p ↥(H ⊔ K)
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) :
is_p_group p ↥(H ⊔ K)
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) :
is_p_group p ↥(H ⊔ K)
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₂) :
(fintype.card ↥H₁).coprime (fintype.card ↥H₂)
finite p-groups with different p have coprime orders
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.
theorem
is_p_group.cyclic_center_quotient_of_card_eq_prime_sq
{p : ℕ}
{G : Type u_1}
[group G]
[fintype G]
[fact (nat.prime p)]
(hG : fintype.card G = p ^ 2) :
is_cyclic (G ⧸ subgroup.center G)
The quotient by the center of a group of cardinality p ^ 2 is cyclic.
def
is_p_group.comm_group_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 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
- is_p_group.comm_group_of_card_eq_prime_sq hG = comm_group_of_cycle_center_quotient (quotient_group.mk' (subgroup.center G)) is_p_group.comm_group_of_card_eq_prime_sq._proof_3
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 group of order p ^ 2 is commutative. See also is_p_group.comm_group_of_card_eq_prime_sq
for the comm_group instance.