Documentation

Mathlib.GroupTheory.PGroup

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.

def IsPGroup (p : ) (G : Type u_1) [Group G] :

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

Equations
Instances For
    theorem IsPGroup.iff_orderOf {p : } {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] :
    IsPGroup p G ∀ (g : G), ∃ (k : ), orderOf g = p ^ k
    theorem IsPGroup.of_card {p : } {G : Type u_1} [Group G] [Fintype G] {n : } (hG : Fintype.card G = p ^ n) :
    theorem IsPGroup.of_bot {p : } {G : Type u_1} [Group G] :
    theorem IsPGroup.iff_card {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Fintype G] :
    IsPGroup p G ∃ (n : ), Fintype.card G = p ^ n
    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.of_injective {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) {H : Type u_2} [Group H] (ϕ : H →* G) (hϕ : Function.Injective ϕ) :
    theorem IsPGroup.to_subgroup {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) (H : Subgroup G) :
    IsPGroup p H
    theorem IsPGroup.of_surjective {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) {H : Type u_2} [Group H] (ϕ : G →* H) (hϕ : Function.Surjective ϕ) :
    theorem IsPGroup.to_quotient {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) (H : Subgroup G) [H.Normal] :
    IsPGroup p (G H)
    theorem IsPGroup.of_equiv {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) {H : Type u_2} [Group H] (ϕ : G ≃* H) :
    theorem IsPGroup.orderOf_coprime {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) {n : } (hn : p.Coprime n) (g : G) :
    (orderOf g).Coprime n
    noncomputable def IsPGroup.powEquiv {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) {n : } (hn : p.Coprime n) :
    G G

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

    Equations
    • hG.powEquiv hn = let h := ; { toFun := fun (x : G) => x ^ n, invFun := fun (g : G) => ((powCoprime ).symm g, ), left_inv := , right_inv := }
    Instances For
      @[simp]
      theorem IsPGroup.powEquiv_apply {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) {n : } (hn : p.Coprime n) (g : G) :
      (hG.powEquiv hn) g = g ^ n
      @[simp]
      theorem IsPGroup.powEquiv_symm_apply {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) {n : } (hn : p.Coprime n) (g : G) :
      (hG.powEquiv hn).symm g = g ^ (orderOf g).gcdB n
      @[reducible, inline]
      noncomputable abbrev 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
      • hG.powEquiv' hn = hG.powEquiv
      Instances For
        theorem IsPGroup.index {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] (H : Subgroup G) [H.FiniteIndex] :
        ∃ (n : ), H.index = p ^ n
        theorem IsPGroup.card_eq_or_dvd {p : } {G : Type u_1} [Group G] (hG : IsPGroup p G) [hp : Fact (Nat.Prime p)] :
        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 α)] :

        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 α)] :
        (MulAction.fixedPoints G α).Nonempty

        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 α) :
        bMulAction.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.to_le {p : } {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hK : IsPGroup p K) (hHK : H K) :
        IsPGroup p H
        theorem IsPGroup.to_inf_left {p : } {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hH : IsPGroup p H) :
        IsPGroup p (H K)
        theorem IsPGroup.to_inf_right {p : } {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hK : IsPGroup p K) :
        IsPGroup p (H K)
        theorem IsPGroup.map {p : } {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsPGroup p H) {K : Type u_2} [Group K] (ϕ : G →* K) :
        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 ϕ.ker) :
        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 ϕ.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 ϕ) :
        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 K.subtype H)
        theorem IsPGroup.to_sup_of_normal_right {p : } {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hH : IsPGroup p H) (hK : IsPGroup p K) [K.Normal] :
        IsPGroup p (H K)
        theorem IsPGroup.to_sup_of_normal_left {p : } {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hH : IsPGroup p H) (hK : IsPGroup p K) [H.Normal] :
        IsPGroup p (H K)
        theorem IsPGroup.to_sup_of_normal_right' {p : } {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hH : IsPGroup p H) (hK : IsPGroup p K) (hHK : H K.normalizer) :
        IsPGroup p (H K)
        theorem IsPGroup.to_sup_of_normal_left' {p : } {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} (hH : IsPGroup p H) (hK : IsPGroup p K) (hHK : K H.normalizer) :
        IsPGroup p (H K)
        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₂) :
        (Fintype.card H₁).Coprime (Fintype.card 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₁ H₁) (hH₂ : IsPGroup p₂ 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 (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.

        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

        Equations
        Instances For
          theorem IsPGroup.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 : G) (b : G) :
          a * b = b * a

          A group of order p ^ 2 is commutative. See also IsPGroup.commGroupOfCardEqPrimeSq for the CommGroup instance.