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.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
- One or more equations did not get rendered due to their size.
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 (_ : Nat.Coprime p n)
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.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, 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]
:
Nontrivial { x // x ∈ Subgroup.center 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.ker_isPGroup_of_injective
{p : ℕ}
{G : Type u_1}
[Group G]
{K : Type u_2}
[Group K]
{ϕ : K →* G}
(hϕ : Function.Injective ↑ϕ)
:
IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
theorem
IsPGroup.comap_of_injective
{p : ℕ}
{G : Type u_1}
[Group G]
{H : Subgroup G}
(hH : IsPGroup p { x // x ∈ H })
{K : Type u_2}
[Group K]
(ϕ : K →* G)
(hϕ : Function.Injective ↑ϕ)
:
IsPGroup p { x // x ∈ Subgroup.comap ϕ H }
theorem
IsPGroup.comap_subtype
{p : ℕ}
{G : Type u_1}
[Group G]
{H : Subgroup G}
(hH : IsPGroup p { x // x ∈ H })
{K : Subgroup G}
:
IsPGroup p { x // x ∈ 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 { 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}
[Group G]
(p₁ : ℕ)
(p₂ : ℕ)
[hp₁ : Fact (Nat.Prime p₁)]
[hp₂ : Fact (Nat.Prime p₂)]
(hne : p₁ ≠ p₂)
(H₁ : Subgroup G)
(H₂ : Subgroup G)
(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}
[Group G]
[Fintype G]
[Fact (Nat.Prime p)]
{n : ℕ}
(hGpn : Fintype.card G = p ^ n)
(hn : 0 < n)
[Fintype { x // x ∈ Subgroup.center G }]
:
∃ k, k > 0 ∧ Fintype.card { x // x ∈ 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