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.
theorem
IsPGroup.exists_card_eq
{p : ℕ}
{G : Type u_1}
[Group G]
[Fact (Nat.Prime p)]
[Fintype G]
:
IsPGroup p G → ∃ (n : ℕ), Fintype.card G = p ^ n
Alias of the forward direction of IsPGroup.iff_card.
theorem
IsPGroup.to_quotient
{p : ℕ}
{G : Type u_1}
[Group G]
(hG : IsPGroup p G)
(H : Subgroup G)
[Subgroup.Normal H]
:
theorem
IsPGroup.orderOf_coprime
{p : ℕ}
{G : Type u_1}
[Group G]
(hG : IsPGroup p G)
{n : ℕ}
(hn : Nat.Coprime p n)
(g : G)
:
Nat.Coprime (orderOf g) n
noncomputable def
IsPGroup.powEquiv
{p : ℕ}
{G : Type u_1}
[Group G]
(hG : IsPGroup p G)
{n : ℕ}
(hn : Nat.Coprime p n)
:
G ≃ G
If gcd(p,n) = 1, then the nth power map is a bijection.
Equations
- IsPGroup.powEquiv hG hn = let h := ⋯; { toFun := fun (x : G) => x ^ n, invFun := fun (g : G) => ↑((powCoprime ⋯).symm { val := g, property := ⋯ }), left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
theorem
IsPGroup.powEquiv_apply
{p : ℕ}
{G : Type u_1}
[Group G]
(hG : IsPGroup p G)
{n : ℕ}
(hn : Nat.Coprime p n)
(g : G)
:
(IsPGroup.powEquiv hG hn) g = g ^ n
@[simp]
theorem
IsPGroup.powEquiv_symm_apply
{p : ℕ}
{G : Type u_1}
[Group G]
(hG : IsPGroup p G)
{n : ℕ}
(hn : Nat.Coprime p n)
(g : G)
:
(IsPGroup.powEquiv hG hn).symm g = g ^ Nat.gcdB (orderOf g) n
@[reducible]
noncomputable def
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
- IsPGroup.powEquiv' hG hn = IsPGroup.powEquiv hG ⋯
Instances For
theorem
IsPGroup.index
{p : ℕ}
{G : Type u_1}
[Group G]
(hG : IsPGroup p G)
[hp : Fact (Nat.Prime p)]
(H : Subgroup G)
[Subgroup.FiniteIndex H]
:
∃ (n : ℕ), Subgroup.index H = p ^ n
theorem
IsPGroup.nontrivial_iff_card
{p : ℕ}
{G : Type u_1}
[Group G]
(hG : IsPGroup p G)
[hp : Fact (Nat.Prime p)]
[Fintype G]
:
Nontrivial G ↔ ∃ n > 0, Fintype.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 : α)
[Fintype ↑(MulAction.orbit G a)]
:
∃ (n : ℕ), Fintype.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 α]
[Fintype α]
[Fintype ↑(MulAction.fixedPoints G α)]
:
Fintype.card α ≡ Fintype.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_2)
[MulAction G α]
[Fintype α]
(hpα : ¬p ∣ Fintype.card α)
[Finite ↑(MulAction.fixedPoints 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
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 α]
[Fintype α]
(hpα : p ∣ Fintype.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]
:
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]
:
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 ↥(MonoidHom.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 ↥(MonoidHom.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 (Subgroup.subtype K) H)
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₂)
[Fintype ↥H₁]
[Fintype ↥H₂]
(hH₁ : IsPGroup p₁ ↥H₁)
(hH₂ : IsPGroup p₂ ↥H₂)
:
Nat.Coprime (Fintype.card ↥H₁) (Fintype.card ↥H₂)
finite p-groups with different p have coprime orders
theorem
IsPGroup.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 > 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
IsPGroup.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)
:
IsCyclic (G ⧸ Subgroup.center G)
The quotient by the center of a group of cardinality p ^ 2 is cyclic.
def
IsPGroup.commGroupOfCardEqPrimeSq
{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 IsPGroup.commutative_of_card_eq_prime_sq
for just the proof that ∀ a b, a * b = b * a