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.
A p-group is a group in which every element has prime power order
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.iff_card
{p : ℕ}
{G : Type u_1}
[group G]
[fact (nat.prime p)]
[fintype G] :
is_p_group p G ↔ ∃ (n : ℕ), fintype.card G = p ^ n
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.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 α]
[fintype ↥(mul_action.fixed_points G α)]
(hpα : ¬p ∣ fintype.card α) :
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 α]
[fintype ↥(mul_action.fixed_points G α)]
(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]
[fintype 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]
[fintype 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.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