Documentation

Mathlib.GroupTheory.Sylow

Sylow theorems #

The Sylow theorems are the following results for every finite group G and every prime number p.

Main definitions #

Main statements #

structure Sylow (p : ) (G : Type u_1) [Group G] extends Subgroup :
Type u_1

A Sylow p-subgroup is a maximal p-subgroup.

  • carrier : Set G
  • mul_mem' : ∀ {a b : G}, a (self).carrierb (self).carriera * b (self).carrier
  • one_mem' : 1 (self).carrier
  • inv_mem' : ∀ {x : G}, x (self).carrierx⁻¹ (self).carrier
  • isPGroup' : IsPGroup p self
  • is_maximal' : ∀ {Q : Subgroup G}, IsPGroup p Qself QQ = self
Instances For
    theorem Sylow.isPGroup' {p : } {G : Type u_1} [Group G] (self : Sylow p G) :
    IsPGroup p self
    theorem Sylow.is_maximal' {p : } {G : Type u_1} [Group G] (self : Sylow p G) {Q : Subgroup G} :
    IsPGroup p Qself QQ = self
    instance Sylow.instCoeOutSubgroup {p : } {G : Type u_1} [Group G] :
    Equations
    • Sylow.instCoeOutSubgroup = { coe := Sylow.toSubgroup }
    theorem Sylow.ext {p : } {G : Type u_1} [Group G] {P : Sylow p G} {Q : Sylow p G} (h : P = Q) :
    P = Q
    theorem Sylow.ext_iff {p : } {G : Type u_1} [Group G] {P : Sylow p G} {Q : Sylow p G} :
    P = Q P = Q
    instance Sylow.instSetLike {p : } {G : Type u_1} [Group G] :
    SetLike (Sylow p G) G
    Equations
    • Sylow.instSetLike = { coe := fun (x : Sylow p G) => x, coe_injective' := }
    instance Sylow.instSubgroupClass {p : } {G : Type u_1} [Group G] :
    Equations
    • =
    instance Sylow.mulActionLeft {p : } {G : Type u_1} [Group G] (P : Sylow p G) {α : Type u_2} [MulAction G α] :
    MulAction (P) α

    The action by a Sylow subgroup is the action by the underlying group.

    Equations
    def Sylow.comapOfKerIsPGroup {p : } {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : IsPGroup p ϕ.ker) (h : P ϕ.range) :
    Sylow p K

    The preimage of a Sylow subgroup under a p-group-kernel homomorphism is a Sylow subgroup.

    Equations
    • P.comapOfKerIsPGroup ϕ h = let __src := Subgroup.comap ϕ P; { toSubgroup := __src, isPGroup' := , is_maximal' := }
    Instances For
      @[simp]
      theorem Sylow.coe_comapOfKerIsPGroup {p : } {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : IsPGroup p ϕ.ker) (h : P ϕ.range) :
      (P.comapOfKerIsPGroup ϕ h) = Subgroup.comap ϕ P
      def Sylow.comapOfInjective {p : } {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : Function.Injective ϕ) (h : P ϕ.range) :
      Sylow p K

      The preimage of a Sylow subgroup under an injective homomorphism is a Sylow subgroup.

      Equations
      • P.comapOfInjective ϕ h = P.comapOfKerIsPGroup ϕ h
      Instances For
        @[simp]
        theorem Sylow.coe_comapOfInjective {p : } {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : Function.Injective ϕ) (h : P ϕ.range) :
        (P.comapOfInjective ϕ h) = Subgroup.comap ϕ P
        def Sylow.subtype {p : } {G : Type u_1} [Group G] (P : Sylow p G) {N : Subgroup G} (h : P N) :
        Sylow p N

        A sylow subgroup of G is also a sylow subgroup of a subgroup of G.

        Equations
        • P.subtype h = P.comapOfInjective N.subtype
        Instances For
          @[simp]
          theorem Sylow.coe_subtype {p : } {G : Type u_1} [Group G] (P : Sylow p G) {N : Subgroup G} (h : P N) :
          (P.subtype h) = (P).subgroupOf N
          theorem Sylow.subtype_injective {p : } {G : Type u_1} [Group G] {N : Subgroup G} {P : Sylow p G} {Q : Sylow p G} {hP : P N} {hQ : Q N} (h : P.subtype hP = Q.subtype hQ) :
          P = Q
          theorem IsPGroup.exists_le_sylow {p : } {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup p P) :
          ∃ (Q : Sylow p G), P Q

          A generalization of Sylow's first theorem. Every p-subgroup is contained in a Sylow p-subgroup.

          instance Sylow.nonempty {p : } {G : Type u_1} [Group G] :
          Equations
          • =
          noncomputable instance Sylow.inhabited {p : } {G : Type u_1} [Group G] :
          Equations
          theorem Sylow.exists_comap_eq_of_ker_isPGroup {p : } {G : Type u_1} [Group G] {H : Type u_2} [Group H] (P : Sylow p H) {f : H →* G} (hf : IsPGroup p f.ker) :
          ∃ (Q : Sylow p G), Subgroup.comap f Q = P
          theorem Sylow.exists_comap_eq_of_injective {p : } {G : Type u_1} [Group G] {H : Type u_2} [Group H] (P : Sylow p H) {f : H →* G} (hf : Function.Injective f) :
          ∃ (Q : Sylow p G), Subgroup.comap f Q = P
          theorem Sylow.exists_comap_subtype_eq {p : } {G : Type u_1} [Group G] {H : Subgroup G} (P : Sylow p H) :
          ∃ (Q : Sylow p G), Subgroup.comap H.subtype Q = P
          theorem Sylow.finite_of_ker_is_pGroup {p : } {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : H →* G} (hf : IsPGroup p f.ker) [Finite (Sylow p G)] :

          If the kernel of f : H →* G is a p-group, then Finite (Sylow p G) implies Finite (Sylow p H).

          theorem Sylow.finite_of_injective {p : } {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : H →* G} (hf : Function.Injective f) [Finite (Sylow p G)] :

          If f : H →* G is injective, then Finite (Sylow p G) implies Finite (Sylow p H).

          instance instFiniteSylowSubtypeMemSubgroup {p : } {G : Type u_1} [Group G] (H : Subgroup G) [Finite (Sylow p G)] :
          Finite (Sylow p H)

          If H is a subgroup of G, then Finite (Sylow p G) implies Finite (Sylow p H).

          Equations
          • =
          instance Sylow.pointwiseMulAction {p : } {G : Type u_1} [Group G] {α : Type u_2} [Group α] [MulDistribMulAction α G] :
          MulAction α (Sylow p G)

          Subgroup.pointwiseMulAction preserves Sylow subgroups.

          Equations
          theorem Sylow.pointwise_smul_def {p : } {G : Type u_1} [Group G] {α : Type u_2} [Group α] [MulDistribMulAction α G] {g : α} {P : Sylow p G} :
          (g P) = g P
          instance Sylow.mulAction {p : } {G : Type u_1} [Group G] :
          Equations
          theorem Sylow.smul_def {p : } {G : Type u_1} [Group G] {g : G} {P : Sylow p G} :
          g P = MulAut.conj g P
          theorem Sylow.coe_subgroup_smul {p : } {G : Type u_1} [Group G] {g : G} {P : Sylow p G} :
          (g P) = MulAut.conj g P
          theorem Sylow.coe_smul {p : } {G : Type u_1} [Group G] {g : G} {P : Sylow p G} :
          (g P) = MulAut.conj g P
          theorem Sylow.smul_le {p : } {G : Type u_1} [Group G] {P : Sylow p G} {H : Subgroup G} (hP : P H) (h : H) :
          (h P) H
          theorem Sylow.smul_subtype {p : } {G : Type u_1} [Group G] {P : Sylow p G} {H : Subgroup G} (hP : P H) (h : H) :
          h P.subtype hP = (h P).subtype
          theorem Sylow.smul_eq_iff_mem_normalizer {p : } {G : Type u_1} [Group G] {g : G} {P : Sylow p G} :
          g P = P g (P).normalizer
          theorem Sylow.smul_eq_of_normal {p : } {G : Type u_1} [Group G] {g : G} {P : Sylow p G} [h : (P).Normal] :
          g P = P
          theorem Subgroup.sylow_mem_fixedPoints_iff {p : } {G : Type u_1} [Group G] (H : Subgroup G) {P : Sylow p G} :
          P MulAction.fixedPoints (H) (Sylow p G) H (P).normalizer
          theorem IsPGroup.inf_normalizer_sylow {p : } {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup p P) (Q : Sylow p G) :
          P (Q).normalizer = P Q
          theorem IsPGroup.sylow_mem_fixedPoints_iff {p : } {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup p P) {Q : Sylow p G} :
          Q MulAction.fixedPoints (P) (Sylow p G) P Q

          A generalization of Sylow's second theorem. If the number of Sylow p-subgroups is finite, then all Sylow p-subgroups are conjugate.

          Equations
          • =
          theorem card_sylow_modEq_one (p : ) (G : Type u_1) [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] :

          A generalization of Sylow's third theorem. If the number of Sylow p-subgroups is finite, then it is congruent to 1 modulo p.

          theorem not_dvd_card_sylow (p : ) (G : Type u_1) [Group G] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] :
          def Sylow.equivSMul {p : } {G : Type u_1} [Group G] (P : Sylow p G) (g : G) :
          P ≃* (g P)

          Sylow subgroups are isomorphic

          Equations
          Instances For
            noncomputable def Sylow.equiv {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (Q : Sylow p G) :
            P ≃* Q

            Sylow subgroups are isomorphic

            Equations
            Instances For
              @[simp]
              theorem Sylow.orbit_eq_top {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
              theorem Sylow.stabilizer_eq_normalizer {p : } {G : Type u_1} [Group G] (P : Sylow p G) :
              MulAction.stabilizer G P = (P).normalizer
              theorem Sylow.conj_eq_normalizer_conj_of_mem_centralizer {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (x : G) (g : G) (hx : x Subgroup.centralizer P) (hy : g⁻¹ * x * g Subgroup.centralizer P) :
              n(P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
              theorem Sylow.conj_eq_normalizer_conj_of_mem {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) [_hP : (P).IsCommutative] (x : G) (g : G) (hx : x P) (hy : g⁻¹ * x * g P) :
              n(P).normalizer, g⁻¹ * x * g = n⁻¹ * x * n
              noncomputable def Sylow.equivQuotientNormalizer {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
              Sylow p G G (P).normalizer

              Sylow p-subgroups are in bijection with cosets of the normalizer of a Sylow p-subgroup

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                instance instFiniteQuotientSubgroupNormalizerOfFactPrimeOfSylow {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
                Finite (G (P).normalizer)
                Equations
                • =
                theorem card_sylow_eq_card_quotient_normalizer {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
                Nat.card (Sylow p G) = Nat.card (G (P).normalizer)
                theorem card_sylow_eq_index_normalizer {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
                Nat.card (Sylow p G) = (P).normalizer.index
                theorem card_sylow_dvd_index {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
                Nat.card (Sylow p G) (P).index
                theorem not_dvd_index_sylow' {p : } {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] (P : Sylow p G) [(P).Normal] [fP : (P).FiniteIndex] :
                ¬p (P).index
                theorem not_dvd_index_sylow {p : } {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (hP : (P).relindex (P).normalizer 0) :
                ¬p (P).index
                theorem Sylow.normalizer_sup_eq_top {G : Type u_1} [Group G] {p : } [Fact (Nat.Prime p)] {N : Subgroup G} [N.Normal] [Finite (Sylow p N)] (P : Sylow p N) :
                (Subgroup.map N.subtype P).normalizer N =

                Frattini's Argument: If N is a normal subgroup of G, and if P is a Sylow p-subgroup of N, then N_G(P) ⊔ N = G.

                theorem Sylow.normalizer_sup_eq_top' {G : Type u_1} [Group G] {p : } [Fact (Nat.Prime p)] {N : Subgroup G} [N.Normal] [Finite (Sylow p N)] (P : Sylow p G) (hP : P N) :
                (P).normalizer N =

                Frattini's Argument: If N is a normal subgroup of G, and if P is a Sylow p-subgroup of N, then N_G(P) ⊔ N = G.

                theorem QuotientGroup.card_preimage_mk {G : Type u} [Group G] (s : Subgroup G) (t : Set (G s)) :
                Nat.card (QuotientGroup.mk ⁻¹' t) = Nat.card s * Nat.card t
                theorem Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {G : Type u} [Group G] {H : Subgroup G} [Finite H] {x : G} :
                x MulAction.fixedPoints (H) (G H) x H.normalizer
                def Sylow.fixedPointsMulLeftCosetsEquivQuotient {G : Type u} [Group G] (H : Subgroup G) [Finite H] :
                (MulAction.fixedPoints (H) (G H)) H.normalizer Subgroup.comap H.normalizer.subtype H

                The fixed points of the action of H on its cosets correspond to normalizer H / H.

                Equations
                Instances For
                  theorem Sylow.card_quotient_normalizer_modEq_card_quotient {G : Type u} [Group G] [Finite G] {p : } {n : } [hp : Fact (Nat.Prime p)] {H : Subgroup G} (hH : Nat.card H = p ^ n) :
                  Nat.card (H.normalizer Subgroup.comap H.normalizer.subtype H) Nat.card (G H) [MOD p]

                  If H is a p-subgroup of G, then the index of H inside its normalizer is congruent mod p to the index of H.

                  theorem Sylow.card_normalizer_modEq_card {G : Type u} [Group G] [Finite G] {p : } {n : } [hp : Fact (Nat.Prime p)] {H : Subgroup G} (hH : Nat.card H = p ^ n) :
                  Nat.card H.normalizer Nat.card G [MOD p ^ (n + 1)]

                  If H is a subgroup of G of cardinality p ^ n, then the cardinality of the normalizer of H is congruent mod p ^ (n + 1) to the cardinality of G.

                  theorem Sylow.prime_dvd_card_quotient_normalizer {G : Type u} [Group G] [Finite G] {p : } {n : } [hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) Nat.card G) {H : Subgroup G} (hH : Nat.card H = p ^ n) :
                  p Nat.card (H.normalizer Subgroup.comap H.normalizer.subtype H)

                  If H is a p-subgroup but not a Sylow p-subgroup, then p divides the index of H inside its normalizer.

                  theorem Sylow.prime_pow_dvd_card_normalizer {G : Type u} [Group G] [Finite G] {p : } {n : } [_hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) Nat.card G) {H : Subgroup G} (hH : Nat.card H = p ^ n) :
                  p ^ (n + 1) Nat.card H.normalizer

                  If H is a p-subgroup but not a Sylow p-subgroup of cardinality p ^ n, then p ^ (n + 1) divides the cardinality of the normalizer of H.

                  theorem Sylow.exists_subgroup_card_pow_succ {G : Type u} [Group G] [Finite G] {p : } {n : } [hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) Nat.card G) {H : Subgroup G} (hH : Nat.card H = p ^ n) :
                  ∃ (K : Subgroup G), Nat.card K = p ^ (n + 1) H K

                  If H is a subgroup of G of cardinality p ^ n, then H is contained in a subgroup of cardinality p ^ (n + 1) if p ^ (n + 1) divides the cardinality of G

                  @[irreducible]
                  theorem Sylow.exists_subgroup_card_pow_prime_le {G : Type u} [Group G] [Finite G] (p : ) {n : } {m : } [_hp : Fact (Nat.Prime p)] (_hdvd : p ^ m Nat.card G) (H : Subgroup G) (_hH : Nat.card H = p ^ n) (_hnm : n m) :
                  ∃ (K : Subgroup G), Nat.card K = p ^ m H K

                  If H is a subgroup of G of cardinality p ^ n, then H is contained in a subgroup of cardinality p ^ m if n ≤ m and p ^ m divides the cardinality of G

                  theorem Sylow.exists_subgroup_card_pow_prime {G : Type u} [Group G] [Finite G] (p : ) {n : } [Fact (Nat.Prime p)] (hdvd : p ^ n Nat.card G) :
                  ∃ (K : Subgroup G), Nat.card K = p ^ n

                  A generalisation of Sylow's first theorem. If p ^ n divides the cardinality of G, then there is a subgroup of cardinality p ^ n

                  theorem Sylow.exists_subgroup_card_pow_prime_of_le_card {G : Type u} [Group G] {n : } {p : } (hp : Nat.Prime p) (h : IsPGroup p G) (hn : p ^ n Nat.card G) :
                  ∃ (H : Subgroup G), Nat.card H = p ^ n

                  A special case of Sylow's first theorem. If G is a p-group of size at least p ^ n then there is a subgroup of cardinality p ^ n.

                  theorem Sylow.exists_subgroup_le_card_pow_prime_of_le_card {G : Type u} [Group G] {n : } {p : } (hp : Nat.Prime p) (h : IsPGroup p G) {H : Subgroup G} (hn : p ^ n Nat.card H) :
                  H'H, Nat.card H' = p ^ n

                  A special case of Sylow's first theorem. If G is a p-group and H a subgroup of size at least p ^ n then there is a subgroup of H of cardinality p ^ n.

                  theorem Sylow.exists_subgroup_le_card_le {G : Type u} [Group G] {k : } {p : } (hp : Nat.Prime p) (h : IsPGroup p G) {H : Subgroup G} (hk : k Nat.card H) (hk₀ : k 0) :
                  H'H, Nat.card H' k k < p * Nat.card H'

                  A special case of Sylow's first theorem. If G is a p-group and H a subgroup of size at least k then there is a subgroup of H of cardinality between k / p and k.

                  theorem Sylow.pow_dvd_card_of_pow_dvd_card {G : Type u} [Group G] [Finite G] {p : } {n : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p ^ n Nat.card G) :
                  p ^ n Nat.card P
                  theorem Sylow.dvd_card_of_dvd_card {G : Type u} [Group G] [Finite G] {p : } [Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p Nat.card G) :
                  p Nat.card P
                  theorem Sylow.card_coprime_index {G : Type u} [Group G] [Finite G] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) :
                  (Nat.card P).Coprime (P).index

                  Sylow subgroups are Hall subgroups.

                  theorem Sylow.ne_bot_of_dvd_card {G : Type u} [Group G] [Finite G] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p Nat.card G) :
                  P
                  theorem Sylow.card_eq_multiplicity {G : Type u} [Group G] [Finite G] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) :
                  Nat.card P = p ^ (Nat.card G).factorization p

                  The cardinality of a Sylow subgroup is p ^ n where n is the multiplicity of p in the group order.

                  def Sylow.ofCard {G : Type u} [Group G] [Finite G] {p : } [Fact (Nat.Prime p)] (H : Subgroup G) (card_eq : Nat.card H = p ^ (Nat.card G).factorization p) :
                  Sylow p G

                  A subgroup with cardinality p ^ n is a Sylow subgroup where n is the multiplicity of p in the group order.

                  Equations
                  • Sylow.ofCard H card_eq = { toSubgroup := H, isPGroup' := , is_maximal' := }
                  Instances For
                    @[simp]
                    theorem Sylow.coe_ofCard {G : Type u} [Group G] [Finite G] {p : } [Fact (Nat.Prime p)] (H : Subgroup G) (card_eq : Nat.card H = p ^ (Nat.card G).factorization p) :
                    (Sylow.ofCard H card_eq) = H
                    noncomputable def Sylow.unique_of_normal {G : Type u} [Group G] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (h : (P).Normal) :

                    If G has a normal Sylow p-subgroup, then it is the only Sylow p-subgroup.

                    Equations
                    • P.unique_of_normal h = { toInhabited := Sylow.inhabited, uniq := }
                    Instances For
                      theorem Sylow.characteristic_of_normal {G : Type u} [Group G] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (h : (P).Normal) :
                      (P).Characteristic
                      theorem Sylow.normal_of_normalizer_normal {G : Type u} [Group G] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (hn : (P).normalizer.Normal) :
                      (P).Normal
                      @[simp]
                      theorem Sylow.normalizer_normalizer {G : Type u} [Group G] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
                      (P).normalizer.normalizer = (P).normalizer
                      theorem Sylow.normal_of_all_max_subgroups_normal {G : Type u} [Group G] [Finite G] (hnc : ∀ (H : Subgroup G), IsCoatom HH.Normal) {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
                      (P).Normal
                      theorem Sylow.normal_of_normalizerCondition {G : Type u} [Group G] (hnc : NormalizerCondition G) {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
                      (P).Normal
                      noncomputable def Sylow.directProductOfNormal {G : Type u} [Group G] [Finite G] (hn : ∀ {p : } [inst : Fact (Nat.Prime p)] (P : Sylow p G), (P).Normal) :
                      ((p : { x : // x (Nat.card G).primeFactors }) → (P : Sylow (p) G) → P) ≃* G

                      If all its Sylow subgroups are normal, then a finite group is isomorphic to the direct product of these Sylow subgroups.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For