Grace/Cumulus/Algebra/Group/Sylow.g17

Open in Workbench Download source

Imports

Translation · PrimeBinomial · NumberTheory.GCDMore

Declarations

Source

1-- Sylow's theorems: p-subgroups and Sylow p-subgroups of a finite group of2-- order p ^ k * m with p prime not dividing m; a group of prime-power order3-- moves a number of points divisible by p; a subgroup of order p ^ k4-- exists, every p-subgroup lies in a conjugate of it, any two Sylow5-- p-subgroups are conjugate, and their number divides m and is 1 modulo p6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Algebra.Group.Sylow12import Translation13import PrimeBinomial14import NumberTheory.GCDMore1516-- A p-subgroup is a subgroup of order a power of p; a Sylow p-subgroup is17-- a subgroup of order the full power of p in the order of the group.18predicate PSubgroup (P G : Set, p : Nat) :=19  Subgroup(P, G) ∧ ∃ j, Nat(j) ∧ cardinality(P) = p ^ j2021predicate SylowSubgroup (P G : Set, p : Nat) :=22  Subgroup(P, G) ∧ ∃ k, Nat(k) ∧ ∃ m, Nat(m) ∧ ¬(p ∣ m) ∧23    order(G) = p ^ k * m ∧ cardinality(P) = p ^ k2425def sylowSubgroups (G : Set, p : Nat) : Set :=26  { P ∈ 𝒫(G.carrier) | SylowSubgroup(P, G, p) }2728theorem sylowSubgroups.subset_powerset (G : Set, p : Nat)29  shows sylowSubgroups(G, p) ⊆ 𝒫(G.carrier)30proof31  intros P hP32  have parts := sylowSubgroups.membership.forward with hP33  exact parts.left3435theorem SylowSubgroup.subgroup (P G : Set, p : Nat)36  requires sylow : SylowSubgroup(P, G, p)37  shows Subgroup(P, G)38proof39  obtain ⟨subgroup, rest⟩ := sylow40  exact subgroup4142theorem SylowSubgroup.p_subgroup (P G : Set, p : Nat)43  requires sylow : SylowSubgroup(P, G, p)44  shows PSubgroup(P, G, p)45proof46  obtain ⟨subgroup, k, kNat, m, mNat, notDivides, count, size⟩ := sylow47  unfold PSubgroup48  exact ⟨subgroup, k, kNat, size⟩4950-- A divisor of a prime power other than one is divisible by the prime.51theorem Prime.divides_of_divides_pow (p d j : Nat)52  requires prime : Prime(p)53  requires divides : d ∣ p ^ j54  requires nontrivial : d ≠ 155  shows p ∣ d56proof57  by_contra notDivides58  have base := Prime.gcd_of_not_divides with prime, notDivides59  have coprime := coprime.pow_left at p, d, j with base60  have scaled : d ∣ p ^ j * 161    rw mul.right_unit62    exact divides63  have one := coprime.cancel at p ^ j, d, 1 with coprime, scaled64  have dNat : Nat(d) by typecheck65  exact nontrivial with (divides.one_only with dNat, one)6667section PrimePowerActions68variable (G : Set)69hypothesis group : Group(G)7071theorem Subgroup.cardinality_ne_zero (H : Set)72  requires subgroup : Subgroup(H, G)73  requires finite : Finite(G)74  shows cardinality(H) ≠ 075proof76  intro zero77  have finiteH := Subgroup.finite with *78  have correct := cardinality.correct with finiteH79  rw zero at correct80  have empty := HasCardinality.empty_of_zero at H with correct81  have unitIn : G.one ∈ H := Subgroup.one_mem with *82  rw empty at unitIn83  exact set.empty with unitIn8485-- A group of order p ^ j acting on a finite set moves a number of points86-- divisible by p: every orbit outside the fixed points has more than one87-- point and a size dividing p ^ j.88theorem Action.prime_power_moved (act X : Set) (p j : Nat)89  requires action : act : G ↷ X90  requires finite : Finite(X)91  requires finiteGroup : Finite(G)92  requires prime : Prime(p)93  requires count : order(G) = p ^ j94  shows p ∣ cardinality(X ∖ fixedPoints(act, G, X))95proof96  apply fixedPoints.difference_dvd with action, finite97  intros x hx notFixed98  have orbitDivides := orbit.cardinality_dvd with action, hx, finiteGroup99  rw count at orbitDivides100  have nontrivial : cardinality(orbit(x)) ≠ 1101    intro one102    apply notFixed103    apply fixedPoints.of_orbit with action, hx104    by_contra different105    have included : {x} ⊆ orbit(x)106      intros y hy107      have equal := singleton.membership.forward with hy108      rw equal109      exact orbit.self with *110    have differentSides : {x} ≠ orbit(x)111      intro equal112      apply different113      symm114      exact equal115    have finiteOrbit := orbit.finite at act, G, X, x with action, finite116    have strict := cardinality.strict_of_ne with117      finiteOrbit, included, differentSides118    rw [cardinality.singleton, one] at strict119    exact Less.irreflexive at 1 with strict120  exact Prime.divides_of_divides_pow with prime, orbitDivides, nontrivial121122-- When p does not divide the size of a finite set acted on, some orbit has123-- size prime to p: otherwise no point is fixed, and p would divide the124-- number of points.125theorem Action.exists_orbit_not_dvd (act X : Set) (p : Nat)126  requires action : act : G ↷ X127  requires finite : Finite(X)128  requires prime : Prime(p)129  requires notDivides : ¬(p ∣ cardinality(X))130  shows ∃ x ∈ X, ¬(p ∣ cardinality(orbit(x)))131proof132  by_contra allDivisible133  apply notDivides134  have orbitsDivisible : ∀ x ∈ X, p ∣ cardinality(orbit(x))135    intros x hx136    by_contra orbitPrime137    exact allDivisible with ⟨x, hx, orbitPrime⟩138  have moved : ∀ x ∈ X, ¬x ∈ fixedPoints(act, G, X) → p ∣ cardinality(orbit(x))139    intros x hx notFixed140    exact orbitsDivisible with x, hx141  have noFixed : ∀ x ∈ X, ¬x ∈ fixedPoints(act, G, X)142    intros x hx fixed143    have single : orbit(x) = {x} := fixedPoints.orbit with *144    have divides := orbitsDivisible with x, hx145    rw [single, cardinality.singleton] at divides146    have one := divides.one_only with assumption, divides147    have above := Prime.greater_than_one with prime148    rw one at above149    exact Less.irreflexive at 1 with above150  have divides := fixedPoints.difference_dvd with action, finite, moved151  have same : X ∖ fixedPoints(act, G, X) = X152    ext x153    constructor154    . intro hx155      obtain ⟨xIn, notFixed⟩ := difference.membership.forward with hx156      exact xIn157    . intro hx158      exact difference.membership.backward with ⟨hx, (noFixed with x, hx)⟩159  rw same at divides160  exact divides161162end PrimePowerActions163164section SylowExistence165variable (G : Set)166hypothesis group : Group(G)167168-- Sylow's first theorem: a finite group of order p ^ k * m, with p prime169-- not dividing m, has a subgroup of order p ^ k. The group acts by170-- translation on its subsets of size p ^ k; there are171-- (p ^ k * m) choose (p ^ k) of them, a number prime to p, so some orbit172-- has size prime to p, and the stabilizer of a subset in that orbit has173-- order divisible by p ^ k and at most p ^ k.174theorem sylow.exists_subgroup (p k m : Nat)175  requires finite : Finite(G)176  requires prime : Prime(p)177  requires notDivides : ¬(p ∣ m)178  requires count : order(G) = p ^ k * m179  shows ∃ P, Subgroup(P, G) ∧ cardinality(P) = p ^ k180proof181  have bounded := subsetsOfSize.subset_powerset at G.carrier, p ^ k182  have closed := subsetsOfSize.translation_closed at G, p ^ k with *183  have action := translation.action with group, bounded, closed184  have finiteFamily := subsetsOfSize.finite at G.carrier, p ^ k with finite185  have familyCount : cardinality(subsetsOfSize(G.carrier, p ^ k)) = (p ^ k * m) choose (p ^ k)186    have counted := combinations.count at G.carrier, p ^ k with finite187    rw [counted, ← order.value, count]188    rfl189  have familyPrime : ¬(p ∣ cardinality(subsetsOfSize(G.carrier, p ^ k)))190    rw familyCount191    exact choose.prime_power_not_divides with *192  have powerNonzero := pow.ne_zero at p, k with (Prime.nonzero with prime)193  have someOrbit := Action.exists_orbit_not_dvd with194    action, finiteFamily, prime, familyPrime195  obtain ⟨S, hS, orbitPrime⟩ := someOrbit196  obtain ⟨boundS, countedS⟩ := subsetsOfSize.membership.forward with hS197  have sizeS := cardinality.eq_of_has with countedS198  have subgroup := stabilizer.subgroup with action, hS199  have finiteStabilizer := Subgroup.finite with group, subgroup, finite200  have stabilizerNat := cardinality.nat with finiteStabilizer201  have finiteOrbit := orbit.finite_of_group with action, hS, finite202  have orbitNat := cardinality.nat with finiteOrbit203  have product := orbit_stabilizer with action, hS, finite204  rw count at product205  -- p ^ k divides the order of the stabilizer, which is at most p ^ k.206  have base := Prime.gcd_of_not_divides with prime, orbitPrime207  have swapped := coprime.symmetric at p, cardinality(orbit(S)) with base208  have coprime := coprime.pow_right at cardinality(orbit(S)), p, k with swapped209  have dividesProduct : p ^ k ∣ cardinality(orbit(S)) * cardinality(stabilizer(S))210    rw product211    exact divides.mul_left_self at p ^ k, m212  have dividesStabilizer := coprime.cancel at213    cardinality(orbit(S)), p ^ k, cardinality(stabilizer(S)) with214    coprime, dividesProduct215  have inhabited := subsetsOfSize.nonempty with hS, powerNonzero216  have upper := translation.stabilizer_card_le with217    group, bounded, closed, finite, hS, inhabited218  rw sizeS at upper219  have nonzero := Subgroup.cardinality_ne_zero with subgroup, finite220  have lower := divides.le with dividesStabilizer, nonzero221  have equal := LessEqual.antisymmetric with upper, lower222  refine ⟨stabilizer(S), subgroup, equal⟩223224theorem SylowSubgroup.exists (p k m : Nat)225  requires finite : Finite(G)226  requires prime : Prime(p)227  requires notDivides : ¬(p ∣ m)228  requires count : order(G) = p ^ k * m229  shows ∃ P, SylowSubgroup(P, G, p)230proof231  obtain ⟨P, subgroup, size⟩ := sylow.exists_subgroup with *232  witness P233  unfold SylowSubgroup234  refine ⟨subgroup, k, assumption, m, assumption, notDivides, count, size⟩235236end SylowExistence237238-- The exponent of p in p ^ j * a with p not dividing a is determined.239theorem Prime.divides_of_pow_mul_lt (p a b j i : Nat)240  requires prime : Prime(p)241  requires below : j < i242  requires equal : p ^ j * a = p ^ i * b243  shows p ∣ a244proof245  have pNonzero := Prime.nonzero with prime246  obtain ⟨d, dNat, shape⟩ := below247  have baseNat : Nat(p ^ j) by typecheck248  have restNat : Nat(p ^ d) by typecheck249  have split : p ^ i = p ^ j * (p * p ^ d)250    rw [← shape, pow.add, pow.succ]251    ring252  have shuffle : p ^ j * (p * p ^ d) * b = p ^ j * (p * p ^ d * b) by ring253  rw [split, shuffle] at equal254  have nonzero := pow.ne_zero at p, j with pNonzero255  have cancelled := mul.left_cancel_positive at a, p * p ^ d * b, p ^ j with256    nonzero, equal257  have divides : p ∣ p * p ^ d * b :=258    divides.multiply_right at p, p * p ^ d, b with (divides.mul_left_self at p, p ^ d)259  rwa ← cancelled at divides260261theorem Prime.pow_mul_exponent (p a b j i : Nat)262  requires prime : Prime(p)263  requires notA : ¬(p ∣ a)264  requires notB : ¬(p ∣ b)265  requires equal : p ^ j * a = p ^ i * b266  shows j = i267proof268  have jNat : Nat(j) by typecheck269  have iNat : Nat(i) by typecheck270  have comparison := Less.trichotomy at j, i with jNat, iNat271  rcases comparison with below | same | above272  . exfalso273    exact notA with (Prime.divides_of_pow_mul_lt with prime, below, equal)274  . exact same275  . exfalso276    symm at equal277    exact notB with (Prime.divides_of_pow_mul_lt with prime, above, equal)278279theorem SylowSubgroup.cardinality_eq (P Q G : Set, p : Nat)280  requires prime : Prime(p)281  requires sylowP : SylowSubgroup(P, G, p)282  requires sylowQ : SylowSubgroup(Q, G, p)283  shows cardinality(P) = cardinality(Q)284proof285  obtain ⟨subgroupP, k, kNat, m, mNat, notDividesM, countP, sizeP⟩ := sylowP286  obtain ⟨subgroupQ, i, iNat, n, nNat, notDividesN, countQ, sizeQ⟩ := sylowQ287  have equal : p ^ k * m = p ^ i * n by cc288  have exponent := Prime.pow_mul_exponent with prime, notDividesM, notDividesN, equal289  rw [sizeP, sizeQ, exponent]290  rfl291292-- The group on a subgroup: its order, its finiteness, the subgroups of G293-- inside it, and its conjugates, read back in G.294section SubgroupGroups295variable (G : Set)296hypothesis group : Group(G)297298theorem subgroupGroup.order (H : Set)299  shows order(subgroupGroup(G, H)) = cardinality(H)300proof301  rw [order.value, subgroupGroup.carrierOf]302  rfl303304theorem subgroupGroup.finite (H : Set)305  requires finite : Finite(H)306  shows Finite(Group.carrier(subgroupGroup(G, H)))307proof308  rw subgroupGroup.carrierOf309  exact finite310311theorem Subgroup.of_subgroupGroup (S H : Set)312  requires subgroupS : Subgroup(S, G)313  requires subgroupH : Subgroup(H, G)314  requires included : S ⊆ H315  shows Subgroup(S, subgroupGroup(G, H))316proof317  have groupH := subgroupGroup.group with group, subgroupH318  have bounded : S ⊆ Group.carrier(subgroupGroup(G, H))319    rw subgroupGroup.carrierOf320    exact included321  have unitIn : Group.one(subgroupGroup(G, H)) ∈ S322    rw subgroupGroup.unit323    exact Subgroup.one_mem with subgroupS324  apply Subgroup.mk with groupH, bounded, unitIn325  . intros x hx y hy326    have xH := included with x, hx327    have yH := included with y, hy328    have restricted : Group.mul(subgroupGroup(G, H))(x, y) = G.mul(x, y) :=329      subgroupGroup.mul with group, subgroupH, xH, yH330    rw restricted331    exact Subgroup.mul_mem with subgroupS, hx, hy332  . intros x hx333    have xH := included with x, hx334    have restricted : Group.inv(subgroupGroup(G, H))(x) = G.inv(x) :=335      subgroupGroup.inverse_value with group, subgroupH, xH336    rw restricted337    exact Subgroup.inv_mem with subgroupS, hx338339theorem subgroupGroup.conjugate (H n q : Set)340  requires subgroup : Subgroup(H, G)341  requires hn : n ∈ H342  requires hq : q ∈ H343  shows conjugate(subgroupGroup(G, H), n, q) = conjugate(G, n, q)344proof345  have product : G.mul(n, q) ∈ H := Subgroup.mul_mem with *346  have inverse : G.inv(n) ∈ H := Subgroup.inv_mem with *347  have mulValue : Group.mul(subgroupGroup(G, H))(n, q) = G.mul(n, q) :=348    subgroupGroup.mul with *349  have invValue : Group.inv(subgroupGroup(G, H))(n) = G.inv(n) :=350    subgroupGroup.inverse_value with *351  have outer : Group.mul(subgroupGroup(G, H))(G.mul(n, q), G.inv(n)) =352      G.mul(G.mul(n, q), G.inv(n)) := subgroupGroup.mul with *353  rw [conjugate.value, conjugate.value, mulValue, invValue, outer]354  rfl355356theorem subgroupGroup.conjugateSet (H n S : Set)357  requires subgroup : Subgroup(H, G)358  requires hn : n ∈ H359  requires bounded : S ⊆ H360  shows conjugateSet(subgroupGroup(G, H), n, S) = conjugateSet(G, n, S)361proof362  have nIn : n ∈ G := Subgroup.mem_carrier with *363  ext y364  constructor365  . intro hy366    obtain ⟨yIn, s, hs, yEq⟩ := conjugateSet.membership.forward with hy367    rw subgroupGroup.carrierOf at yIn368    have sH := bounded with s, hs369    have same := subgroupGroup.conjugate with group, subgroup, hn, sH370    have yG : y ∈ G := Subgroup.mem_carrier with subgroup, yIn371    apply conjugateSet.membership.backward372    refine ⟨yG, s, hs, ?_⟩373    rw [yEq, same]374    rfl375  . intro hy376    obtain ⟨yIn, s, hs, yEq⟩ := conjugateSet.membership.forward with hy377    have sH := bounded with s, hs378    have same := subgroupGroup.conjugate with group, subgroup, hn, sH379    have inH : conjugate(G, n, s) ∈ H380      rw conjugate.value381      typecheck382    have yH : y ∈ Group.carrier(subgroupGroup(G, H))383      rw [subgroupGroup.carrierOf, yEq]384      exact inH385    apply conjugateSet.membership.backward386    refine ⟨yH, s, hs, ?_⟩387    rw [yEq, same]388    rfl389390end SubgroupGroups391392section SylowConjugacy393variable (G : Set)394hypothesis group : Group(G)395396-- Conjugates of Sylow subgroups are Sylow subgroups.397theorem SylowSubgroup.conjugate (P : Set) (g : G) (p : Nat)398  requires finite : Finite(G)399  requires sylow : SylowSubgroup(P, G, p)400  shows SylowSubgroup(conjugateSet(G, g, P), G, p)401proof402  obtain ⟨subgroup, k, kNat, m, mNat, notDivides, count, size⟩ := sylow403  have bounded := Subgroup.subset with subgroup404  have finiteP := Subgroup.finite with *405  have conjugateSubgroup := conjugateSet.subgroup with *406  have gIn : g ∈ G by assumption407  have same := conjugateSet.cardinality with group, gIn, bounded, finiteP408  unfold SylowSubgroup409  refine ⟨conjugateSubgroup, k, kNat, m, mNat, notDivides, count, ?_⟩410  rw same411  exact size412413-- A subgroup of order p ^ k in a group of order p ^ k * m has index m.414theorem Subgroup.index_of_order (P : Set) (p k m : Nat)415  requires finite : Finite(G)416  requires prime : Prime(p)417  requires subgroup : Subgroup(P, G)418  requires count : order(G) = p ^ k * m419  requires size : cardinality(P) = p ^ k420  shows index(G, P) = m421proof422  have lagrangeP := lagrange with *423  have indexNat := index.nat with *424  have powerNat : Nat(p ^ k) by typecheck425  have commuted : index(G, P) * p ^ k = p ^ k * index(G, P) :=426    mul.commutative with *427  rw [count, size, commuted] at lagrangeP428  have nonzero := pow.ne_zero at p, k with (Prime.nonzero with prime)429  have cancelled := mul.left_cancel_positive at m, index(G, P), p ^ k with430    nonzero, lagrangeP431  symm432  exact cancelled433434-- Sylow's second theorem: every p-subgroup lies in a conjugate of a Sylow435-- p-subgroup P. The p-subgroup Q acts by translation on the cosets of P,436-- whose number is prime to p, so it fixes some coset g • P, and then437-- g⁻¹ * q * g ∈ P for every q ∈ Q.438theorem sylow.subset_conjugate (P Q : Set) (p : Nat)439  requires finite : Finite(G)440  requires prime : Prime(p)441  requires sylow : SylowSubgroup(P, G, p)442  requires pSubgroup : PSubgroup(Q, G, p)443  shows ∃ g ∈ G, Q ⊆ conjugateSet(G, g, P)444proof445  obtain ⟨subgroupP, k, kNat, m, mNat, notDivides, count, sizeP⟩ := sylow446  obtain ⟨subgroupQ, j, jNat, sizeQ⟩ := pSubgroup447  have boundedP := Subgroup.subset with subgroupP448  have closed := leftCosets.translation_closed with group, subgroupP449  have cosetAction := leftCosets.action with group, subgroupP450  have action := Action.restrict with cosetAction, subgroupQ451  have groupQ := subgroupGroup.group with group, subgroupQ452  have finiteCosets := leftCosets.finite with group, subgroupP, finite453  have finiteQ := Subgroup.finite with group, subgroupQ, finite454  have finiteQGroup := subgroupGroup.finite at G, Q with group, finiteQ455  have orderQ : order(subgroupGroup(G, Q)) = p ^ j456    rw subgroupGroup.order457    exact sizeQ458  have moved := Action.prime_power_moved at subgroupGroup(G, Q), restrict(translation(G, leftCosets(G, P)), Q × leftCosets(G, P)), leftCosets(G, P), p, j with groupQ, action, finiteCosets, finiteQGroup, prime, orderQ459  have indexEq := Subgroup.index_of_order with460    group, finite, prime, subgroupP, count, sizeP461  -- The number of cosets is m, so some coset is fixed by Q.462  have someFixed : ∃ C, C ∈ fixedPoints(restrict(translation(G, leftCosets(G, P)), Q × leftCosets(G, P)), subgroupGroup(G, Q), leftCosets(G, P))463    by_contra none464    apply notDivides465    have same : leftCosets(G, P) ∖ fixedPoints(restrict(translation(G, leftCosets(G, P)), Q × leftCosets(G, P)), subgroupGroup(G, Q), leftCosets(G, P)) = leftCosets(G, P)466      ext C467      constructor468      . intro hC469        obtain ⟨inCosets, notFixed⟩ := difference.membership.forward with hC470        exact inCosets471      . intro hC472        have notFixed : ¬C ∈ fixedPoints(restrict(translation(G, leftCosets(G, P)), Q × leftCosets(G, P)), subgroupGroup(G, Q), leftCosets(G, P))473          intro fixed474          exact none with ⟨C, fixed⟩475        exact difference.membership.backward with ⟨hC, notFixed⟩476    rw [same, ← index.value, indexEq] at moved477    exact moved478  obtain ⟨C, hC⟩ := someFixed479  have criterion := Action.restrict_fixed_points at translation(G, leftCosets(G, P)), G, leftCosets(G, P), Q, C with cosetAction, subgroupQ480  obtain ⟨cosetIn, fixes⟩ := criterion.forward with hC481  obtain ⟨bound, g, hg, CEq⟩ := leftCosets.membership.forward with cosetIn482  witness g483  constructor484  . exact hg485  . intros q hq486    have qIn : q ∈ G := Subgroup.mem_carrier with subgroupQ, hq487    have fixed := fixes with q, hq488    have value := translation.value with group, closed, qIn, cosetIn489    have translated : q • C = C by cc490    rw CEq at translated491    have merged : q • (g • P) = (q * g) • P := leftCoset.mul_of_subset with *492    rw merged at translated493    symm at translated494    have criterion2 : g • P = (q * g) • P ↔ g⁻¹ * (q * g) ∈ P :=495      leftCoset.eq_iff with *496    have member := criterion2.forward with translated497    have shape : conjugate(G, g⁻¹, q) = g⁻¹ * (q * g)498      rw [conjugate.value, inv_inv, mul_assoc]499      rfl500    have conjugateIn : conjugate(G, g⁻¹, q) ∈ P by rwa shape501    have criterion3 := conjugateSet.mem_iff at G, g, P, q with group, boundedP, qIn502    exact criterion3.backward with conjugateIn503504-- Any two Sylow p-subgroups are conjugate.505theorem sylow.conjugate (P Q : Set) (p : Nat)506  requires finite : Finite(G)507  requires prime : Prime(p)508  requires sylowP : SylowSubgroup(P, G, p)509  requires sylowQ : SylowSubgroup(Q, G, p)510  shows ∃ g ∈ G, Q = conjugateSet(G, g, P)511proof512  have pSubgroup := SylowSubgroup.p_subgroup with sylowQ513  obtain ⟨g, hg, included⟩ := sylow.subset_conjugate at G, P, Q, p with514    group, finite, prime, sylowP, pSubgroup515  have sameSize := SylowSubgroup.cardinality_eq with prime, sylowP, sylowQ516  have subgroupP := SylowSubgroup.subgroup with sylowP517  have boundedP := Subgroup.subset with subgroupP518  have finiteP := Subgroup.finite with group, subgroupP, finite519  have conjugateSize := conjugateSet.cardinality with group, hg, boundedP, finiteP520  have finiteConjugate := conjugateSet.finite with group, hg, boundedP, finiteP521  have equalSize : cardinality(Q) = cardinality(conjugateSet(G, g, P)) by cc522  witness g523  constructor524  . exact hg525  . exact cardinality.eq_subset with finiteConjugate, included, equalSize526527-- A Sylow p-subgroup normalized by another is that one: in the normalizer528-- of Q, the subgroup Q is a normal Sylow p-subgroup and P a p-subgroup,529-- so P lies in a conjugate of Q, which is Q itself.530theorem SylowSubgroup.eq_of_normalizes (P Q : Set) (p : Nat)531  requires finite : Finite(G)532  requires prime : Prime(p)533  requires sylowP : SylowSubgroup(P, G, p)534  requires sylowQ : SylowSubgroup(Q, G, p)535  requires normalizes : P ⊆ normalizer(G, Q)536  shows P = Q537proof538  have sizeP := SylowSubgroup.cardinality_eq with prime, sylowP, sylowQ539  have subgroupP := SylowSubgroup.subgroup with sylowP540  obtain ⟨subgroupQ, k, kNat, m, mNat, notDivides, count, sizeQ⟩ := sylowQ541  have boundedQ := Subgroup.subset with subgroupQ542  have normalizerSubgroup := normalizer.subgroup with group, boundedQ543  have containedQ := normalizer.contains with group, subgroupQ544  have groupN := subgroupGroup.group with group, normalizerSubgroup545  have finiteN := Subgroup.finite with group, normalizerSubgroup, finite546  have finiteNGroup := subgroupGroup.finite at G, normalizer(G, Q) with547    group, finiteN548  have subgroupQN := Subgroup.of_subgroupGroup with549    group, subgroupQ, normalizerSubgroup, containedQ550  have subgroupPN := Subgroup.of_subgroupGroup with551    group, subgroupP, normalizerSubgroup, normalizes552  -- The order of the normalizer is p ^ k times a number prime to p.553  have dividesN := lagrange.theorem at subgroupGroup(G, normalizer(G, Q)), Q with554    groupN, subgroupQN, finiteNGroup555  rw [subgroupGroup.order, sizeQ] at dividesN556  obtain ⟨t, tNat, NEq⟩ := dividesN557  have dividesG := lagrange.theorem with group, normalizerSubgroup, finite558  rw [count, ← NEq] at dividesG559  have nonzero := pow.ne_zero at p, k with (Prime.nonzero with prime)560  have cancel := divides.mul_cancel_left at p ^ k, t, m with nonzero561  have tDividesM := cancel.forward with dividesG562  have tPrime : ¬(p ∣ t)563    intro pt564    exact notDivides with (divides.transitive with pt, tDividesM)565  have sylowQN : SylowSubgroup(Q, subgroupGroup(G, normalizer(G, Q)), p)566    unfold SylowSubgroup567    refine ⟨subgroupQN, k, kNat, t, tNat, tPrime, ?_, sizeQ⟩568    rw subgroupGroup.order569    symm570    exact NEq571  have pSubgroupPN : PSubgroup(P, subgroupGroup(G, normalizer(G, Q)), p)572    unfold PSubgroup573    refine ⟨subgroupPN, k, kNat, ?_⟩574    rw sizeP575    exact sizeQ576  obtain ⟨n, hn, included⟩ := sylow.subset_conjugate at577    subgroupGroup(G, normalizer(G, Q)), Q, P, p with578    groupN, finiteNGroup, prime, sylowQN, pSubgroupPN579  rw subgroupGroup.carrierOf at hn580  have same := subgroupGroup.conjugateSet at G, normalizer(G, Q), n, Q with581    group, normalizerSubgroup, hn, containedQ582  obtain ⟨nIn, fixedQ⟩ := normalizer.membership.forward with hn583  rw [same, fixedQ] at included584  have finiteQ := Subgroup.finite with group, subgroupQ, finite585  exact cardinality.eq_subset with finiteQ, included, sizeP586587end SylowConjugacy588589section SylowCount590variable (G : Set)591hypothesis group : Group(G)592593-- The Sylow p-subgroups are the conjugates of any one of them, so their594-- number is the index of its normalizer.595theorem sylowSubgroups.eq_conjugates (P : Set) (p : Nat)596  requires finite : Finite(G)597  requires prime : Prime(p)598  requires sylow : SylowSubgroup(P, G, p)599  shows sylowSubgroups(G, p) = conjugates(G, P)600proof601  have subgroupP := SylowSubgroup.subgroup with sylow602  have boundedP := Subgroup.subset with subgroupP603  ext Q604  constructor605  . intro hQ606    obtain ⟨bound, sylowQ⟩ := sylowSubgroups.membership.forward with hQ607    obtain ⟨g, hg, QEq⟩ := sylow.conjugate at G, P, Q, p with608      group, finite, prime, sylow, sylowQ609    have criterion := conjugates.membership at G, P, Q with group, boundedP610    exact criterion.backward with ⟨g, hg, QEq⟩611  . intro hQ612    have criterion := conjugates.membership at G, P, Q with group, boundedP613    obtain ⟨g, hg, QEq⟩ := criterion.forward with hQ614    have sylowQ : SylowSubgroup(Q, G, p)615      rw QEq616      exact SylowSubgroup.conjugate at G, P, g, p with group, finite, sylow617    have boundQ := powerset.membership_iff.backward with618      (Subgroup.subset with (SylowSubgroup.subgroup with sylowQ))619    exact sylowSubgroups.membership.backward with ⟨boundQ, sylowQ⟩620621theorem sylow.count_eq_index (P : Set) (p : Nat)622  requires finite : Finite(G)623  requires prime : Prime(p)624  requires sylow : SylowSubgroup(P, G, p)625  shows cardinality(sylowSubgroups(G, p)) = index(G, normalizer(G, P))626proof627  have boundedP := Subgroup.subset with (SylowSubgroup.subgroup with sylow)628  have same := sylowSubgroups.eq_conjugates with *629  rw same630  exact conjugates.cardinality_eq_index with group, boundedP, finite631632-- Sylow's third theorem, first half: the number of Sylow p-subgroups633-- divides m, since it is the index of a normalizer whose order is a634-- multiple of p ^ k.635theorem sylow.count_dvd (p k m : Nat)636  requires finite : Finite(G)637  requires prime : Prime(p)638  requires notDivides : ¬(p ∣ m)639  requires count : order(G) = p ^ k * m640  shows cardinality(sylowSubgroups(G, p)) ∣ m641proof642  obtain ⟨P, subgroupP, sizeP⟩ := sylow.exists_subgroup with *643  have sylow : SylowSubgroup(P, G, p)644    unfold SylowSubgroup645    refine ⟨subgroupP, k, assumption, m, assumption, notDivides, count, sizeP⟩646  have boundedP := Subgroup.subset with subgroupP647  have normalizerSubgroup := normalizer.subgroup with group, boundedP648  have contained := normalizer.contains with group, subgroupP649  have countIndex := sylow.count_eq_index with group, finite, prime, sylow650  have lagrangeN := lagrange with group, normalizerSubgroup, finite651  have groupN := subgroupGroup.group with group, normalizerSubgroup652  have finiteN := Subgroup.finite with group, normalizerSubgroup, finite653  have finiteNGroup := subgroupGroup.finite at G, normalizer(G, P) with654    group, finiteN655  have subgroupPN := Subgroup.of_subgroupGroup with656    group, subgroupP, normalizerSubgroup, contained657  have dividesN := lagrange.theorem at subgroupGroup(G, normalizer(G, P)), P with658    groupN, subgroupPN, finiteNGroup659  rw [subgroupGroup.order, sizeP] at dividesN660  obtain ⟨t, tNat, NEq⟩ := dividesN661  have indexNat := index.nat with group, normalizerSubgroup, finite662  have powerNat : Nat(p ^ k) by typecheck663  have shuffle : index(G, normalizer(G, P)) * (p ^ k * t) =664      p ^ k * (index(G, normalizer(G, P)) * t) by ring665  rw [count, ← NEq, shuffle] at lagrangeN666  have nonzero := pow.ne_zero at p, k with (Prime.nonzero with prime)667  have cancelled := mul.left_cancel_positive at668    m, index(G, normalizer(G, P)) * t, p ^ k with nonzero, lagrangeN669  have finiteSyl := Finite.subset with670    (Finite.powerset with finite), (sylowSubgroups.subset_powerset at G, p)671  have sylNat := cardinality.nat with finiteSyl672  witness t673  rw countIndex674  symm675  exact cancelled676677end SylowCount678679-- The action of a Sylow p-subgroup P on the Sylow p-subgroups by680-- conjugation: the conjugation action of G on its subsets, restricted to681-- the Sylow p-subgroups and to P.682def sylowConjugation (G P : Set, p : Nat) : Set :=683  restrict(restrict(subsetConjugation(G), G.carrier × sylowSubgroups(G, p)),684    P × sylowSubgroups(G, p))685686theorem sylowConjugation.value (G P : Set, p : Nat)687  shows sylowConjugation(G, P, p) =688    restrict(restrict(subsetConjugation(G), G.carrier × sylowSubgroups(G, p)),689      P × sylowSubgroups(G, p))690proof691  simp [sylowConjugation]692693section SylowModulo694variable (G : Set)695hypothesis group : Group(G)696697theorem sylowSubgroups.conjugation_closed (p : Nat)698  requires finite : Finite(G)699  shows ∀ g ∈ G.carrier, ∀ Q ∈ sylowSubgroups(G, p),700    subsetConjugation(G)(g, Q) ∈ sylowSubgroups(G, p)701proof702  intros g hg Q hQ703  obtain ⟨boundQ, sylowQ⟩ := sylowSubgroups.membership.forward with hQ704  have value := subsetConjugation.value with group, hg, boundQ705  rw value706  have sylowConjugate := SylowSubgroup.conjugate at G, Q, g, p with707    group, finite, sylowQ708  have boundConjugate := powerset.membership_iff.backward with709    (conjugateSet.subset at G, g, Q)710  exact sylowSubgroups.membership.backward with ⟨boundConjugate, sylowConjugate⟩711712theorem sylowConjugation.action (P : Set) (p : Nat)713  requires finite : Finite(G)714  requires subgroup : Subgroup(P, G)715  shows sylowConjugation(G, P, p) : subgroupGroup(G, P) ↷ sylowSubgroups(G, p)716proof717  have action := subsetConjugation.action with group718  have bounded := sylowSubgroups.subset_powerset at G, p719  have closed := sylowSubgroups.conjugation_closed at G, p with group, finite720  have restricted := Action.restrict_subset with action, bounded, closed721  rw sylowConjugation.value722  exact Action.restrict with restricted, subgroup723724-- A Sylow p-subgroup is fixed by P exactly when P normalizes it.725theorem sylowConjugation.fixed_iff (P Q : Set) (p : Nat)726  requires finite : Finite(G)727  requires subgroup : Subgroup(P, G)728  shows Q ∈ fixedPoints(sylowConjugation(G, P, p), subgroupGroup(G, P), sylowSubgroups(G, p)) ↔729    Q ∈ sylowSubgroups(G, p) ∧ P ⊆ normalizer(G, Q)730proof731  have action := subsetConjugation.action with group732  have bounded := sylowSubgroups.subset_powerset at G, p733  have closed := sylowSubgroups.conjugation_closed at G, p with group, finite734  have restricted := Action.restrict_subset with action, bounded, closed735  have criterion := Action.restrict_fixed_points at restrict(subsetConjugation(G), G.carrier × sylowSubgroups(G, p)), G, sylowSubgroups(G, p), P, Q with restricted, subgroup736  rw sylowConjugation.value737  constructor738  . intro fixed739    obtain ⟨QIn, fixes⟩ := criterion.forward with fixed740    refine ⟨QIn, ?_⟩741    intros x hx742    have xIn : x ∈ G := Subgroup.mem_carrier with subgroup, hx743    have value := Action.restrict_subset_value at subsetConjugation(G), G, 𝒫(G.carrier), sylowSubgroups(G, p), x, Q with action, bounded, closed, QIn744    have conjugated := subsetConjugation.value with group, xIn, (bounded with Q, QIn)745    have fixedX := fixes with x, hx746    have same : conjugateSet(G, x, Q) = Q by cc747    exact normalizer.membership.backward with ⟨xIn, same⟩748  . intro normalizes749    obtain ⟨QIn, included⟩ := normalizes750    apply criterion.backward751    refine ⟨QIn, ?_⟩752    intros x hx753    have xIn : x ∈ G := Subgroup.mem_carrier with subgroup, hx754    have value := Action.restrict_subset_value at subsetConjugation(G), G, 𝒫(G.carrier), sylowSubgroups(G, p), x, Q with action, bounded, closed, QIn755    have conjugated := subsetConjugation.value with group, xIn, (bounded with Q, QIn)756    obtain ⟨xG, same⟩ := normalizer.membership.forward with (included with x, hx)757    cc758759-- The only Sylow p-subgroup fixed by P is P itself.760theorem sylowConjugation.fixed_points (P : Set) (p : Nat)761  requires finite : Finite(G)762  requires prime : Prime(p)763  requires sylowP : SylowSubgroup(P, G, p)764  shows fixedPoints(sylowConjugation(G, P, p), subgroupGroup(G, P), sylowSubgroups(G, p)) = {P}765proof766  have subgroupP := SylowSubgroup.subgroup with sylowP767  have boundedP := Subgroup.subset with subgroupP768  have PIn : P ∈ sylowSubgroups(G, p) :=769    sylowSubgroups.membership.backward with770      ⟨(powerset.membership_iff.backward with boundedP), sylowP⟩771  ext Q772  have criterion := sylowConjugation.fixed_iff at G, P, Q, p with group, finite, subgroupP773  constructor774  . intro hQ775    obtain ⟨QIn, normalizes⟩ := criterion.forward with hQ776    obtain ⟨boundQ, sylowQ⟩ := sylowSubgroups.membership.forward with QIn777    have equal := SylowSubgroup.eq_of_normalizes with778      group, finite, prime, sylowP, sylowQ, normalizes779    rw ← equal780    exact singleton.self781  . intro hQ782    have equal := singleton.membership.forward with hQ783    have criterionP := sylowConjugation.fixed_iff at G, P, P, p with group, finite, subgroupP784    rw equal785    apply criterionP.backward786    exact ⟨PIn, (normalizer.contains with group, subgroupP)⟩787788-- Sylow's third theorem, second half: the number of Sylow p-subgroups is789-- 1 modulo p. Under the conjugation action of a Sylow p-subgroup P the790-- only fixed point is P, so p divides the number of the others.791theorem sylow.count_mod (p k m : Nat)792  requires finite : Finite(G)793  requires prime : Prime(p)794  requires notDivides : ¬(p ∣ m)795  requires count : order(G) = p ^ k * m796  shows cardinality(sylowSubgroups(G, p)) % p = 1797proof798  obtain ⟨P, subgroupP, sizeP⟩ := sylow.exists_subgroup with *799  have sylowP : SylowSubgroup(P, G, p)800    unfold SylowSubgroup801    refine ⟨subgroupP, k, assumption, m, assumption, notDivides, count, sizeP⟩802  have finiteP := Subgroup.finite with group, subgroupP, finite803  have action := sylowConjugation.action at G, P, p with group, finite, subgroupP804  have groupP := subgroupGroup.group with group, subgroupP805  have finitePGroup := subgroupGroup.finite at G, P with group, finiteP806  have finiteSyl := Finite.subset with807    (Finite.powerset with finite), (sylowSubgroups.subset_powerset at G, p)808  have orderP : order(subgroupGroup(G, P)) = p ^ k809    rw subgroupGroup.order810    exact sizeP811  have moved := Action.prime_power_moved at subgroupGroup(G, P), sylowConjugation(G, P, p), sylowSubgroups(G, p), p, k with groupP, action, finiteSyl, finitePGroup, prime, orderP812  have fixedEq := sylowConjugation.fixed_points at G, P, p with group, finite, prime, sylowP813  rw fixedEq at moved814  -- The Sylow p-subgroups are P and a multiple of p others.815  have fixedSubset := fixedPoints.subset at sylowConjugation(G, P, p), subgroupGroup(G, P), sylowSubgroups(G, p)816  have split := difference.union2_of_subset with fixedSubset817  have finiteFixed := Finite.subset with finiteSyl, fixedSubset818  have finiteRest := Finite.subset with finiteSyl, (difference.subset_left at sylowSubgroups(G, p), fixedPoints(sylowConjugation(G, P, p), subgroupGroup(G, P), sylowSubgroups(G, p)))819  have disjoint := Disjoint.symmetric with (difference.disjoint at sylowSubgroups(G, p), fixedPoints(sylowConjugation(G, P, p), subgroupGroup(G, P), sylowSubgroups(G, p)))820  have total := cardinality.union_disjoint with finiteFixed, finiteRest, disjoint821  rw [split, fixedEq, cardinality.singleton] at total822  obtain ⟨s, sNat, restEq⟩ := moved823  rw [total, ← restEq]824  have wrap := mod.add_multiple at p, 1, s with (Prime.nonzero with prime)825  rw wrap826  exact mod.of_less with (Prime.greater_than_one with prime)827828end SylowModulo829