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
  • carrier : Set G
  • mul_mem' : ∀ {a b : G}, a s.carrierb s.carriera * b s.carrier
  • one_mem' : 1 s.carrier
  • inv_mem' : ∀ {x : G}, x s.carrierx⁻¹ s.carrier
  • isPGroup' : IsPGroup p { x // x s }
  • is_maximal' : ∀ {Q : Subgroup G}, IsPGroup p { x // x Q }s QQ = s

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

Instances For
    instance Sylow.instCoeOutSylowSubgroup {p : } {G : Type u_1} [Group G] :
    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.instSetLikeSylow {p : } {G : Type u_1} [Group G] :
    SetLike (Sylow p G) G
    instance Sylow.mulActionLeft {p : } {G : Type u_1} [Group G] (P : Sylow p G) {α : Type u_2} [MulAction G α] :
    MulAction { x // x P } α

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

    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 { x // x MonoidHom.ker ϕ }) (h : P MonoidHom.range ϕ) :
    Sylow p K

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

    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 { x // x MonoidHom.ker ϕ }) (h : P MonoidHom.range ϕ) :
      ↑(Sylow.comapOfKerIsPGroup P ϕ 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 MonoidHom.range ϕ) :
      Sylow p K

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

      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 MonoidHom.range ϕ) :
        ↑(Sylow.comapOfInjective P ϕ 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 { x // x N }

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

        Instances For
          @[simp]
          theorem Sylow.coe_subtype {p : } {G : Type u_1} [Group G] (P : Sylow p G) {N : Subgroup G} (h : P 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 : Sylow.subtype P hP = Sylow.subtype Q hQ) :
          P = Q
          theorem IsPGroup.exists_le_sylow {p : } {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup p { x // x P }) :
          Q, 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] :
          noncomputable instance Sylow.inhabited {p : } {G : Type u_1} [Group G] :
          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 { x // x MonoidHom.ker f }) :
          Q, 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, Subgroup.comap f Q = P
          theorem Sylow.exists_comap_subtype_eq {p : } {G : Type u_1} [Group G] {H : Subgroup G} (P : Sylow p { x // x H }) :
          Q, Subgroup.comap (Subgroup.subtype H) Q = P
          noncomputable def Sylow.fintypeOfKerIsPGroup {p : } {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : H →* G} (hf : IsPGroup p { x // x MonoidHom.ker f }) [Fintype (Sylow p G)] :

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

          Instances For
            noncomputable def Sylow.fintypeOfInjective {p : } {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : H →* G} (hf : Function.Injective f) [Fintype (Sylow p G)] :

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

            Instances For
              noncomputable instance instFintypeSylowSubtypeMemSubgroupInstMembershipInstSetLikeSubgroupToGroup {p : } {G : Type u_1} [Group G] (H : Subgroup G) [Fintype (Sylow p G)] :
              Fintype (Sylow p { x // x H })

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

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

              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.

              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] :
              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 : { x // x 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 : { x // x H }) :
              h Sylow.subtype P hP = Sylow.subtype (h P) (_ : ↑(h P) H)
              theorem Sylow.smul_eq_iff_mem_normalizer {p : } {G : Type u_1} [Group G] {g : G} {P : Sylow p G} :
              theorem Sylow.smul_eq_of_normal {p : } {G : Type u_1} [Group G] {g : G} {P : Sylow p G} [h : Subgroup.Normal P] :
              g P = P
              theorem Subgroup.sylow_mem_fixedPoints_iff {p : } {G : Type u_1} [Group G] (H : Subgroup G) {P : Sylow p G} :
              theorem IsPGroup.inf_normalizer_sylow {p : } {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup p { x // x P }) (Q : Sylow p G) :
              theorem IsPGroup.sylow_mem_fixedPoints_iff {p : } {G : Type u_1} [Group G] {P : Subgroup G} (hP : IsPGroup p { x // x P }) {Q : Sylow p G} :
              Q MulAction.fixedPoints { x // x 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.

              theorem card_sylow_modEq_one (p : ) (G : Type u_1) [Group G] [Fact (Nat.Prime p)] [Fintype (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)] [Fintype (Sylow p G)] :
              def Sylow.equivSMul {p : } {G : Type u_1} [Group G] (P : Sylow p G) (g : G) :
              { x // x P } ≃* { x // x ↑(g P) }

              Sylow subgroups are isomorphic

              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) :
                { x // x P } ≃* { x // x Q }

                Sylow subgroups are isomorphic

                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.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, n Subgroup.normalizer P 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 : Subgroup.IsCommutative P] (x : G) (g : G) (hx : x P) (hy : g⁻¹ * x * g P) :
                  n, n Subgroup.normalizer P g⁻¹ * x * g = n⁻¹ * x * n
                  noncomputable def Sylow.equivQuotientNormalizer {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Fintype (Sylow p G)] (P : Sylow p G) :

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

                  Instances For
                    theorem card_sylow_dvd_index {p : } {G : Type u_1} [Group G] [Fact (Nat.Prime p)] [Fintype (Sylow p G)] (P : Sylow p G) :
                    theorem not_dvd_index_sylow' {p : } {G : Type u_1} [Group G] [hp : Fact (Nat.Prime p)] (P : Sylow p G) [Subgroup.Normal P] [fP : Subgroup.FiniteIndex P] :
                    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 : Subgroup.relindex (P) (Subgroup.normalizer P) 0) :
                    theorem Sylow.normalizer_sup_eq_top {G : Type u_1} [Group G] {p : } [Fact (Nat.Prime p)] {N : Subgroup G} [Subgroup.Normal N] [Finite (Sylow p { x // x N })] (P : Sylow p { x // x 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} [Subgroup.Normal N] [Finite (Sylow p { x // x N })] (P : Sylow p G) (hP : P 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] [Fintype G] (s : Subgroup G) (t : Set (G s)) :
                    Fintype.card ↑(QuotientGroup.mk ⁻¹' t) = Fintype.card { x // x s } * Fintype.card t

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

                    Instances For

                      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] [Fintype G] {p : } {n : } [hp : Fact (Nat.Prime p)] {H : Subgroup G} (hH : Fintype.card { x // x H } = p ^ n) :

                      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] [Fintype G] {p : } {n : } [hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) Fintype.card G) {H : Subgroup G} (hH : Fintype.card { x // x H } = p ^ n) :

                      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] [Fintype G] {p : } {n : } [_hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) Fintype.card G) {H : Subgroup G} (hH : Fintype.card { x // x H } = p ^ n) :
                      p ^ (n + 1) Fintype.card { x // x Subgroup.normalizer H }

                      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] [Fintype G] {p : } {n : } [hp : Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) Fintype.card G) {H : Subgroup G} (hH : Fintype.card { x // x H } = p ^ n) :
                      K, Fintype.card { x // x 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

                      theorem Sylow.exists_subgroup_card_pow_prime_le {G : Type u} [Group G] [Fintype G] (p : ) {n : } {m : } [_hp : Fact (Nat.Prime p)] (_hdvd : p ^ m Fintype.card G) (H : Subgroup G) (_hH : Fintype.card { x // x H } = p ^ n) (_hnm : n m) :
                      K, Fintype.card { x // x 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] [Fintype G] (p : ) {n : } [Fact (Nat.Prime p)] (hdvd : p ^ n Fintype.card G) :
                      K, Fintype.card { x // x 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.pow_dvd_card_of_pow_dvd_card {G : Type u} [Group G] [Fintype G] {p : } {n : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p ^ n Fintype.card G) :
                      p ^ n Fintype.card { x // x P }
                      theorem Sylow.dvd_card_of_dvd_card {G : Type u} [Group G] [Fintype G] {p : } [Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p Fintype.card G) :
                      p Fintype.card { x // x P }
                      theorem Sylow.card_coprime_index {G : Type u} [Group G] [Fintype G] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) :
                      Nat.Coprime (Fintype.card { x // x P }) (Subgroup.index P)

                      Sylow subgroups are Hall subgroups.

                      theorem Sylow.ne_bot_of_dvd_card {G : Type u} [Group G] [Fintype G] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) (hdvd : p Fintype.card G) :
                      P
                      theorem Sylow.card_eq_multiplicity {G : Type u} [Group G] [Fintype G] {p : } [hp : Fact (Nat.Prime p)] (P : Sylow p G) :
                      Fintype.card { x // x P } = p ^ ↑(Nat.factorization (Fintype.card G)) 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] [Fintype G] {p : } [Fact (Nat.Prime p)] (H : Subgroup G) [Fintype { x // x H }] (card_eq : Fintype.card { x // x H } = p ^ ↑(Nat.factorization (Fintype.card G)) 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.

                      Instances For
                        @[simp]
                        theorem Sylow.coe_ofCard {G : Type u} [Group G] [Fintype G] {p : } [Fact (Nat.Prime p)] (H : Subgroup G) [Fintype { x // x H }] (card_eq : Fintype.card { x // x H } = p ^ ↑(Nat.factorization (Fintype.card G)) p) :
                        ↑(Sylow.ofCard H card_eq) = H
                        theorem Sylow.subsingleton_of_normal {G : Type u} [Group G] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (h : Subgroup.Normal P) :
                        theorem Sylow.characteristic_of_normal {G : Type u} [Group G] {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) (h : Subgroup.Normal P) :
                        theorem Sylow.normal_of_all_max_subgroups_normal {G : Type u} [Group G] [Finite G] (hnc : ∀ (H : Subgroup G), IsCoatom HSubgroup.Normal H) {p : } [Fact (Nat.Prime p)] [Finite (Sylow p G)] (P : Sylow p G) :
                        noncomputable def Sylow.directProductOfNormal {G : Type u} [Group G] [Fintype G] (hn : ∀ {p : } [inst : Fact (Nat.Prime p)] (P : Sylow p G), Subgroup.Normal P) :
                        ((p : { x // x (Nat.factorization (Fintype.card G)).support }) → (P : Sylow (p) G) → { x // x P }) ≃* G

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

                        Instances For