Grace/Cumulus/Algebra/Group/Conjugation.g17

Open in Workbench Download source

Imports

Action · Center · Restricted

Declarations

Source

1-- Conjugation as a group action: the action of G on itself by conjugation,2-- whose orbits are the conjugacy classes, stabilizers the centralizers,3-- and fixed points the center, so the class equation; the action of G on4-- its subsets by conjugation, conjugate subgroups, and the normalizer of a5-- subgroup6-- 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.Conjugation12import Action13import Center14import Restricted1516-- The action of G on its carrier by conjugation, as a graph on pairs.17def conjugationAction (G : Set) : Set :=18  { p ∈ (G.carrier × G.carrier) × G.carrier |19    ∃ g ∈ G.carrier, ∃ x ∈ G.carrier, p = ((g, x) ↦ conjugate(G, g, x)) }2021-- The conjugacy class of x.22def conjugacyClass (G x : Set) : Set :=23  { y ∈ G.carrier | ∃ g ∈ G.carrier, y = conjugate(G, g, x) }2425theorem conjugacyClass.subset (G x : Set)26  shows conjugacyClass(G, x) ⊆ G.carrier27proof28  intros y hy29  have parts := conjugacyClass.membership.forward with hy30  exact parts.left3132section ConjugationAction33variable (G : Set)34hypothesis group : Group(G)3536theorem conjugationAction.relates (g x : G)37  shows relates(conjugationAction(G), (g, x), conjugate(G, g, x))38proof39  have gIn : g ∈ G by assumption40  have xIn : x ∈ G by assumption41  have output : conjugate(G, g, x) ∈ G := conjugate.mem with *42  have pair := product.pair at g, x, G.carrier, G.carrier with *43  have bounded := product.pair at (g, x), conjugate(G, g, x),44    G.carrier × G.carrier, G.carrier with *45  unfold relates46  apply conjugationAction.membership.backward47  refine ⟨bounded, g, gIn, x, xIn, rfl⟩4849theorem conjugationAction.function50  shows conjugationAction(G) : G.carrier × G.carrier → G.carrier51proof52  unfold FunctionBetween53  refine ⟨?_, ?_, ?_⟩54  . intros p hp55    have parts := conjugationAction.membership.forward with hp56    exact parts.left57  . intros p y edge z edge258    unfold relates at edge59    unfold relates at edge260    obtain ⟨bounded, g, gIn, x, xIn, shape⟩ :=61      conjugationAction.membership.forward with edge62    obtain ⟨bounded2, g2, gIn2, x2, xIn2, shape2⟩ :=63      conjugationAction.membership.forward with edge264    have outer := orderedPair.injective with shape65    have outer2 := orderedPair.injective with shape266    have inputs : (g, x) = (g2, x2) by cc67    have halves := orderedPair.injective with inputs68    cc69  . intros p hp70    obtain ⟨bound, g, gIn, x, xIn, shape⟩ :=71      product.membership.forward with hp72    have output : conjugate(G, g, x) ∈ G := conjugate.mem with *73    have edge := conjugationAction.relates at G, g, x with *74    refine ⟨conjugate(G, g, x), output, ?_⟩75    rw shape76    exact edge7778theorem conjugationAction.value (g x : G)79  shows conjugationAction(G)(g, x) = conjugate(G, g, x)80proof81  have function := conjugationAction.function with group82  have edge := conjugationAction.relates at G, g, x with *83  have input := product.pair at g, x, G.carrier, G.carrier with *84  have value := FunctionBetween.apply_value with function, input, edge85  have called : conjugationAction(G)(g, x) = conjugationAction(G)((g, x))86    unfold call287    rfl88  rw called89  exact value9091theorem conjugationAction.action92  shows conjugationAction(G) : G ↷ G.carrier93proof94  have function := conjugationAction.function with group95  apply Action.mk with group, function96  . intros x hx97    have value := conjugationAction.value at G, G.one, x with *98    have fixed : conjugate(G, G.one, x) = x := conjugate.by_one with *99    rw [value, fixed]100    rfl101  . intros g hg h hh x hx102    have closed : g * h ∈ G by typecheck103    have first := conjugationAction.value at G, g * h, x with *104    have inner := conjugationAction.value at G, h, x with *105    have innerIn : conjugate(G, h, x) ∈ G := conjugate.mem with *106    have outer := conjugationAction.value at G, g, conjugate(G, h, x) with *107    have merged : conjugate(G, g, conjugate(G, h, x)) =108        conjugate(G, g * h, x) := conjugate.conjugate with *109    rw [first, inner, outer, merged]110    rfl111112-- The conjugacy class of x is its orbit, its stabilizer the centralizer113-- of x, and the fixed points form the center.114theorem conjugacyClass.self (x : G)115  shows x ∈ conjugacyClass(G, x)116proof117  have xIn : x ∈ G by assumption118  have unitIn : G.one ∈ G := Group.one_mem with *119  have fixed : conjugate(G, G.one, x) = x := conjugate.by_one with *120  apply conjugacyClass.membership.backward121  refine ⟨xIn, G.one, unitIn, ?_⟩122  symm123  exact fixed124125theorem conjugacyClass.eq_orbit (x : G)126  shows conjugacyClass(G, x) = orbit(conjugationAction(G), G, G.carrier, x)127proof128  have action := conjugationAction.action with group129  ext y130  constructor131  . intro hy132    obtain ⟨yIn, g, gIn, yEq⟩ := conjugacyClass.membership.forward with hy133    have value := conjugationAction.value at G, g, x with *134    apply orbit.membership.backward135    refine ⟨yIn, g, gIn, ?_⟩136    rw [yEq, value]137    rfl138  . intro hy139    obtain ⟨yIn, g, gIn, yEq⟩ := orbit.membership.forward with hy140    have value := conjugationAction.value at G, g, x with *141    apply conjugacyClass.membership.backward142    refine ⟨yIn, g, gIn, ?_⟩143    rw [yEq, value]144    rfl145146theorem conjugationAction.stabilizer_eq (x : G)147  shows stabilizer(conjugationAction(G), G, G.carrier, x) = centralizer(G, {x})148proof149  have action := conjugationAction.action with group150  ext g151  constructor152  . intro hg153    obtain ⟨gIn, fixed⟩ := stabilizer.membership.forward with hg154    have value := conjugationAction.value at G, g, x with *155    have fixedConjugate : conjugate(G, g, x) = x by cc156    have commute : g * x = x * g := conjugate.commute_of_fixed with *157    apply centralizer.membership.backward158    refine ⟨gIn, ?_⟩159    intros y hy160    have equal := singleton.membership.forward with hy161    rw equal162    exact commute163  . intro hg164    obtain ⟨gIn, commutes⟩ := centralizer.membership.forward with hg165    have selfIn := singleton.self at x166    have commute := commutes with x, selfIn167    have fixed : conjugate(G, g, x) = x := conjugate.of_commute with *168    have value := conjugationAction.value at G, g, x with *169    apply stabilizer.membership.backward170    refine ⟨gIn, ?_⟩171    rw value172    exact fixed173174theorem conjugationAction.fixed_points175  shows fixedPoints(conjugationAction(G), G, G.carrier) = center(G)176proof177  ext x178  constructor179  . intro hx180    obtain ⟨xIn, fixed⟩ := fixedPoints.membership.forward with hx181    apply center.membership.backward182    refine ⟨xIn, ?_⟩183    intros g gIn184    have value := conjugationAction.value at G, g, x with *185    have fixedG := fixed with g, gIn186    have fixedConjugate : conjugate(G, g, x) = x by cc187    have commute : g * x = x * g := conjugate.commute_of_fixed with *188    symm189    exact commute190  . intro hx191    obtain ⟨xIn, commutes⟩ := center.membership.forward with hx192    apply fixedPoints.membership.backward193    refine ⟨xIn, ?_⟩194    intros g gIn195    have commute := commutes with g, gIn196    have swapped : g * x = x * g by cc197    have fixed : conjugate(G, g, x) = x := conjugate.of_commute with *198    have value := conjugationAction.value at G, g, x with *199    rw value200    exact fixed201202theorem conjugacyClass.cardinality_eq_index (x : G)203  requires finite : Finite(G)204  shows cardinality(conjugacyClass(G, x)) = index(G, centralizer(G, {x}))205proof206  have action := conjugationAction.action with group207  have xIn : x ∈ G by assumption208  have same := orbit.cardinality_eq_index with action, xIn, finite209  rw [conjugacyClass.eq_orbit, ← conjugationAction.stabilizer_eq]210  exact same211212theorem conjugacyClass.cardinality_dvd (x : G)213  requires finite : Finite(G)214  shows cardinality(conjugacyClass(G, x)) ∣ order(G)215proof216  have action := conjugationAction.action with group217  have xIn : x ∈ G by assumption218  have divides := orbit.cardinality_dvd with action, xIn, finite219  rw conjugacyClass.eq_orbit220  exact divides221222end ConjugationAction223224-- The conjugacy classes, and those not inside the center.225def conjugacyClasses (G : Set) : Set :=226  { C ∈ 𝒫(G.carrier) | ∃ x ∈ G.carrier, C = conjugacyClass(G, x) }227def noncentralClasses (G : Set) : Set :=228  { C ∈ conjugacyClasses(G) | ¬(C ⊆ center(G)) }229230section ClassEquation231variable (G : Set)232hypothesis group : Group(G)233234theorem conjugacyClasses.eq_orbits235  shows conjugacyClasses(G) = orbits(conjugationAction(G), G, G.carrier)236proof237  ext C238  constructor239  . intro hC240    obtain ⟨bound, x, hx, CEq⟩ :=241      conjugacyClasses.membership.forward with hC242    have same : conjugacyClass(G, x) =243        orbit(conjugationAction(G), G, G.carrier, x) :=244      conjugacyClass.eq_orbit with *245    apply orbits.membership.backward246    refine ⟨bound, x, hx, ?_⟩247    rw [CEq, same]248    rfl249  . intro hC250    obtain ⟨bound, x, hx, CEq⟩ := orbits.membership.forward with hC251    have same : conjugacyClass(G, x) =252        orbit(conjugationAction(G), G, G.carrier, x) :=253      conjugacyClass.eq_orbit with *254    apply conjugacyClasses.membership.backward255    refine ⟨bound, x, hx, ?_⟩256    rw [CEq, same]257    rfl258259theorem noncentralClasses.eq_moved260  shows noncentralClasses(G) = movedOrbits(conjugationAction(G), G, G.carrier)261proof262  have classes := conjugacyClasses.eq_orbits with group263  have fixed := conjugationAction.fixed_points with group264  ext C265  constructor266  . intro hC267    obtain ⟨inClasses, notCentral⟩ :=268      noncentralClasses.membership.forward with hC269    rw classes at inClasses270    rw ← fixed at notCentral271    exact movedOrbits.membership.backward at272      conjugationAction(G), G, G.carrier, C with ⟨inClasses, notCentral⟩273  . intro hC274    obtain ⟨inOrbits, notFixed⟩ := movedOrbits.membership.forward with hC275    rw ← classes at inOrbits276    rw fixed at notFixed277    exact noncentralClasses.membership.backward with ⟨inOrbits, notFixed⟩278279theorem noncentralClasses.representative (C : Set)280  requires hC : C ∈ noncentralClasses(G)281  shows ∃ x ∈ G, ¬x ∈ center(G) ∧ C = conjugacyClass(G, x)282proof283  obtain ⟨inClasses, notCentral⟩ :=284    noncentralClasses.membership.forward with hC285  obtain ⟨bound, x, hx, CEq⟩ :=286    conjugacyClasses.membership.forward with inClasses287  witness x288  refine ⟨hx, ?_, CEq⟩289  intro central290  apply notCentral291  rw CEq292  intros y hy293  obtain ⟨yIn, g, gIn, yEq⟩ := conjugacyClass.membership.forward with hy294  have fixed : conjugate(G, g, x) = x := center.conjugate_fixed with *295  rw [yEq, fixed]296  exact central297298-- The class equation: the order of a finite group is the size of its299-- center plus the sizes of its noncentral conjugacy classes.300theorem class_equation301  requires finite : Finite(G)302  shows order(G) = cardinality(center(G)) +303    natSum(noncentralClasses(G), sizeMap(noncentralClasses(G)))304proof305  have action := conjugationAction.action with group306  have centerSubset := center.subset at G307  have finiteCenter := Finite.subset with finite, centerSubset308  have finiteRest := Finite.subset with309    finite, (difference.subset_left at G.carrier, center(G))310  have disjoint := Disjoint.symmetric with311    (difference.disjoint at G.carrier, center(G))312  have restored := difference.union2_of_subset with centerSubset313  have split := cardinality.union_disjoint with314    finiteCenter, finiteRest, disjoint315  rw restored at split316  have cover := movedOrbits.cover with action317  have fixed := conjugationAction.fixed_points with group318  have moved := noncentralClasses.eq_moved with group319  have movedSubset := movedOrbits.subset at conjugationAction(G), G, G.carrier320  rw fixed at cover321  have finiteMoved : Finite(noncentralClasses(G))322    rw moved323    exact Finite.subset with (orbits.finite with action, finite), movedSubset324  have members : ∀ C ∈ noncentralClasses(G), Finite(C)325    intros C hC326    rw moved at hC327    exact orbits.member_finite with action, (movedSubset with C, hC), finite328  have pairwise : PairwiseDisjoint(noncentralClasses(G))329    rw moved330    exact PairwiseDisjoint.subset with331      movedSubset, (orbits.pairwise_disjoint with action)332  have count := cardinality.big_union_disjoint with333    finiteMoved, members, pairwise334  have unionEq : ⋃(noncentralClasses(G)) = G.carrier ∖ center(G)335    rw moved336    exact cover337  rw unionEq at count338  rw [order.value, split, count]339  rfl340341-- If a prime divides the order of the group and the index of every342-- noncentral centralizer, it divides the order of the center.343theorem center.dvd_of_classes (p : Nat)344  requires finite : Finite(G)345  requires dividesOrder : p ∣ order(G)346  requires dividesClasses : ∀ x ∈ G,347    ¬x ∈ center(G) → p ∣ index(G, centralizer(G, {x}))348  shows p ∣ cardinality(center(G))349proof350  have action := conjugationAction.action with group351  have fixed := conjugationAction.fixed_points with group352  have orbitsDivisible : ∀ x ∈ G.carrier,353      ¬x ∈ fixedPoints(conjugationAction(G), G, G.carrier) →354      p ∣ cardinality(orbit(conjugationAction(G), G, G.carrier, x))355    intros x hx notFixed356    rw fixed at notFixed357    have same := conjugacyClass.cardinality_eq_index with group, hx, finite358    rw [← conjugacyClass.eq_orbit, same]359    exact dividesClasses with x, hx, notFixed360  have restDivides := fixedPoints.difference_dvd with361    action, finite, orbitsDivisible362  rw fixed at restDivides363  have centerSubset := center.subset at G364  have restored := difference.union2_of_subset with centerSubset365  have finiteCenter := Finite.subset with finite, centerSubset366  have finiteRest := Finite.subset with367    finite, (difference.subset_left at G.carrier, center(G))368  have disjoint := Disjoint.symmetric with369    (difference.disjoint at G.carrier, center(G))370  have split := cardinality.union_disjoint with finiteCenter, finiteRest, disjoint371  rw restored at split372  rw [order.value, split] at dividesOrder373  have centerNat := cardinality.nat with finiteCenter374  have restNat := cardinality.nat with finiteRest375  exact divides.add_cancel_right with restDivides, dividesOrder376377end ClassEquation378379-- The conjugate g S g⁻¹ of a subset S by g.380def conjugateSet (G g S : Set) : Set :=381  { y ∈ G.carrier | ∃ s ∈ S, y = conjugate(G, g, s) }382383theorem conjugateSet.subset (G g S : Set)384  shows conjugateSet(G, g, S) ⊆ G.carrier385proof386  intros y hy387  have parts := conjugateSet.membership.forward with hy388  exact parts.left389390section ConjugateSets391variable (G : Set)392hypothesis group : Group(G)393394theorem conjugateSet.conjugate_mem (g : G) (S s : Set)395  requires bounded : S ⊆ G396  requires hs : s ∈ S397  shows conjugate(G, g, s) ∈ conjugateSet(G, g, S)398proof399  have sIn := bounded with s, hs400  have closed : conjugate(G, g, s) ∈ G := conjugate.mem with *401  exact conjugateSet.membership.backward with ⟨closed, s, hs, rfl⟩402403theorem conjugateSet.one (S : Set)404  requires bounded : S ⊆ G405  shows conjugateSet(G, G.one, S) = S406proof407  ext y408  constructor409  . intro hy410    obtain ⟨yIn, s, hs, yEq⟩ := conjugateSet.membership.forward with hy411    have sIn := bounded with s, hs412    have fixed : conjugate(G, G.one, s) = s := conjugate.by_one with *413    rw [yEq, fixed]414    exact hs415  . intro hy416    have yIn := bounded with y, hy417    have fixed : conjugate(G, G.one, y) = y := conjugate.by_one with *418    have member : conjugate(G, G.one, y) ∈ conjugateSet(G, G.one, S) :=419      conjugateSet.conjugate_mem with *420    rwa fixed at member421422theorem conjugateSet.mul (g h : G) (S : Set)423  requires bounded : S ⊆ G424  shows conjugateSet(G, g, conjugateSet(G, h, S)) = conjugateSet(G, g * h, S)425proof426  ext y427  constructor428  . intro hy429    obtain ⟨yIn, t, ht, yEq⟩ := conjugateSet.membership.forward with hy430    obtain ⟨tIn, s, hs, tEq⟩ := conjugateSet.membership.forward with ht431    have sIn := bounded with s, hs432    have merged : conjugate(G, g, conjugate(G, h, s)) =433        conjugate(G, g * h, s) := conjugate.conjugate with *434    apply conjugateSet.membership.backward435    refine ⟨yIn, s, hs, ?_⟩436    rw [yEq, tEq, merged]437    rfl438  . intro hy439    obtain ⟨yIn, s, hs, yEq⟩ := conjugateSet.membership.forward with hy440    have sIn := bounded with s, hs441    have merged : conjugate(G, g, conjugate(G, h, s)) = conjugate(G, g * h, s) :=442      conjugate.conjugate with *443    have inner : conjugate(G, h, s) ∈ conjugateSet(G, h, S) :=444      conjugateSet.conjugate_mem with *445    apply conjugateSet.membership.backward446    refine ⟨yIn, conjugate(G, h, s), inner, ?_⟩447    rw [yEq, merged]448    rfl449450theorem conjugateSet.eq_image (g : G) (S : Set)451  requires bounded : S ⊆ G452  shows conjugateSet(G, g, S) = functionImage(conjugation(G, g), S, G.carrier)453proof454  ext y455  constructor456  . intro hy457    obtain ⟨yIn, s, hs, yEq⟩ := conjugateSet.membership.forward with hy458    have sIn := bounded with s, hs459    have value := conjugation.value at G, g, s with *460    apply functionImage.membership.backward461    refine ⟨yIn, s, hs, ?_⟩462    rw [yEq, value]463    rfl464  . intro hy465    obtain ⟨yIn, s, hs, yEq⟩ := functionImage.membership.forward with hy466    have sIn := bounded with s, hs467    have value := conjugation.value at G, g, s with *468    apply conjugateSet.membership.backward469    refine ⟨yIn, s, hs, ?_⟩470    rw [yEq, value]471    rfl472473theorem conjugateSet.finite (g : G) (S : Set)474  requires bounded : S ⊆ G475  requires finite : Finite(S)476  shows Finite(conjugateSet(G, g, S))477proof478  have function := conjugation.function at G, g with *479  rw conjugateSet.eq_image480  exact Finite.function_image with function, finite, bounded481482theorem conjugateSet.cardinality (g : G) (S : Set)483  requires bounded : S ⊆ G484  requires finite : Finite(S)485  shows cardinality(conjugateSet(G, g, S)) = cardinality(S)486proof487  have injective := conjugation.injective with *488  rw conjugateSet.eq_image489  exact cardinality.injective_image with injective, bounded, finite490491theorem conjugateSet.subgroup (g : G) (H : Set)492  requires subgroup : Subgroup(H, G)493  shows Subgroup(conjugateSet(G, g, H), G)494proof495  have bounded := Subgroup.subset with subgroup496  have unitIn : G.one ∈ conjugateSet(G, g, H)497    have unitH : G.one ∈ H := Subgroup.one_mem with *498    have fixed : conjugate(G, g, G.one) = G.one := conjugate.one with *499    have member : conjugate(G, g, G.one) ∈ conjugateSet(G, g, H) :=500      conjugateSet.conjugate_mem with *501    rwa fixed at member502  apply Subgroup.mk with group, (conjugateSet.subset at G, g, H), unitIn503  . intros x hx y hy504    obtain ⟨xIn, s, hs, xEq⟩ := conjugateSet.membership.forward with hx505    obtain ⟨yIn, t, ht, yEq⟩ := conjugateSet.membership.forward with hy506    have sIn := bounded with s, hs507    have tIn := bounded with t, ht508    have product : s * t ∈ H := Subgroup.mul_mem with *509    have merged : conjugate(G, g, s * t) =510        conjugate(G, g, s) * conjugate(G, g, t) := conjugate.mul with *511    have member : conjugate(G, g, s * t) ∈ conjugateSet(G, g, H) :=512      conjugateSet.conjugate_mem with *513    rw [xEq, yEq, ← merged]514    exact member515  . intros x hx516    obtain ⟨xIn, s, hs, xEq⟩ := conjugateSet.membership.forward with hx517    have sIn := bounded with s, hs518    have inverse : s⁻¹ ∈ H := Subgroup.inv_mem with *519    have merged : conjugate(G, g, s⁻¹) = conjugate(G, g, s)⁻¹ :=520      conjugate.inv with *521    have member : conjugate(G, g, s⁻¹) ∈ conjugateSet(G, g, H) :=522      conjugateSet.conjugate_mem with *523    rw [xEq, ← merged]524    exact member525526theorem conjugateSet.mem_iff (g : G) (S y : Set)527  requires bounded : S ⊆ G528  requires hy : y ∈ G529  shows y ∈ conjugateSet(G, g, S) ↔ conjugate(G, g⁻¹, y) ∈ S530proof531  constructor532  . intro member533    obtain ⟨yIn, s, hs, yEq⟩ := conjugateSet.membership.forward with member534    have sIn := bounded with s, hs535    have cancel : conjugate(G, g⁻¹, conjugate(G, g, s)) = s :=536      conjugate.cancel with *537    rw [yEq, cancel]538    exact hs539  . intro member540    have back : conjugate(G, g⁻¹, y) ∈ G := conjugate.mem with *541    have cancel : conjugate(G, (g⁻¹)⁻¹, conjugate(G, g⁻¹, y)) = y :=542      conjugate.cancel with *543    rw inv_inv at cancel544    have image : conjugate(G, g, conjugate(G, g⁻¹, y)) ∈ conjugateSet(G, g, S) :=545      conjugateSet.conjugate_mem with *546    rwa cancel at image547548theorem NormalSubgroup.conjugateSet (g : G) (N : Set)549  requires normal : NormalSubgroup(N, G)550  shows conjugateSet(G, g, N) = N551proof552  have subgroup := NormalSubgroup.subgroup with normal553  have bounded := Subgroup.subset with subgroup554  apply Subset.antisymmetric555  . intros y hy556    obtain ⟨yIn, s, hs, yEq⟩ := conjugateSet.membership.forward with hy557    have closed : conjugate(G, g, s) ∈ N :=558      NormalSubgroup.conjugate_mem with *559    rwa yEq560  . intros y hy561    have yIn := bounded with y, hy562    have criterion : y ∈ conjugateSet(G, g, N) ↔563        conjugate(G, g⁻¹, y) ∈ N := conjugateSet.mem_iff with *564    apply criterion.backward565    exact NormalSubgroup.conjugate_mem with *566567theorem NormalSubgroup.of_conjugateSet (N : Set)568  requires subgroup : Subgroup(N, G)569  requires conjugates : ∀ g ∈ G, conjugateSet(G, g, N) = N570  shows NormalSubgroup(N, G)571proof572  have bounded := Subgroup.subset with subgroup573  apply NormalSubgroup.mk with subgroup574  intros g hg n hn575  have member : conjugate(G, g, n) ∈ conjugateSet(G, g, N) :=576    conjugateSet.conjugate_mem with *577  have same := conjugates with g, hg578  rwa same at member579580end ConjugateSets581582-- The action of G on its subsets by conjugation, as a graph on pairs.583def subsetConjugation (G : Set) : Set :=584  { p ∈ (G.carrier × 𝒫(G.carrier)) × 𝒫(G.carrier) |585    ∃ g ∈ G.carrier, ∃ S ∈ 𝒫(G.carrier), p = ((g, S) ↦ conjugateSet(G, g, S)) }586587-- The normalizer of H: the elements conjugating H onto itself. The588-- conjugates of H form its orbit under the conjugation action on subsets.589def normalizer (G H : Set) : Set :=590  { g ∈ G.carrier | conjugateSet(G, g, H) = H }591def conjugates (G H : Set) : Set :=592  orbit(subsetConjugation(G), G, 𝒫(G.carrier), H)593594theorem conjugates.eq_orbit (G H : Set)595  shows conjugates(G, H) = orbit(subsetConjugation(G), G, 𝒫(G.carrier), H)596proof597  simp [conjugates]598599theorem normalizer.subset (G H : Set)600  shows normalizer(G, H) ⊆ G.carrier601proof602  intros g hg603  have parts := normalizer.membership.forward with hg604  exact parts.left605606section SubsetConjugation607variable (G : Set)608hypothesis group : Group(G)609610theorem subsetConjugation.relates (g : G) (S : Set)611  requires hS : S ∈ 𝒫(G.carrier)612  shows relates(subsetConjugation(G), (g, S), conjugateSet(G, g, S))613proof614  have gIn : g ∈ G by assumption615  have output : conjugateSet(G, g, S) ∈ 𝒫(G.carrier) :=616    powerset.membership_iff.backward with (conjugateSet.subset at G, g, S)617  have pair := product.pair at g, S, G.carrier, 𝒫(G.carrier) with *618  have bounded := product.pair at (g, S), conjugateSet(G, g, S),619    G.carrier × 𝒫(G.carrier), 𝒫(G.carrier) with *620  unfold relates621  apply subsetConjugation.membership.backward622  refine ⟨bounded, g, gIn, S, hS, rfl⟩623624theorem subsetConjugation.function625  shows subsetConjugation(G) : G.carrier × 𝒫(G.carrier) → 𝒫(G.carrier)626proof627  unfold FunctionBetween628  refine ⟨?_, ?_, ?_⟩629  . intros p hp630    have parts := subsetConjugation.membership.forward with hp631    exact parts.left632  . intros p y edge z edge2633    unfold relates at edge634    unfold relates at edge2635    obtain ⟨bounded, g, gIn, S, SIn, shape⟩ :=636      subsetConjugation.membership.forward with edge637    obtain ⟨bounded2, g2, gIn2, S2, SIn2, shape2⟩ :=638      subsetConjugation.membership.forward with edge2639    have outer := orderedPair.injective with shape640    have outer2 := orderedPair.injective with shape2641    have inputs : (g, S) = (g2, S2) by cc642    have halves := orderedPair.injective with inputs643    cc644  . intros p hp645    obtain ⟨bound, g, gIn, S, SIn, shape⟩ :=646      product.membership.forward with hp647    have output : conjugateSet(G, g, S) ∈ 𝒫(G.carrier) :=648      powerset.membership_iff.backward with (conjugateSet.subset at G, g, S)649    have edge := subsetConjugation.relates at G, g, S with *650    refine ⟨conjugateSet(G, g, S), output, ?_⟩651    rw shape652    exact edge653654theorem subsetConjugation.value (g : G) (S : Set)655  requires hS : S ∈ 𝒫(G.carrier)656  shows subsetConjugation(G)(g, S) = conjugateSet(G, g, S)657proof658  have function := subsetConjugation.function with group659  have edge := subsetConjugation.relates at G, g, S with *660  have input := product.pair at g, S, G.carrier, 𝒫(G.carrier) with *661  have value := FunctionBetween.apply_value with function, input, edge662  have called : subsetConjugation(G)(g, S) = subsetConjugation(G)((g, S))663    unfold call2664    rfl665  rw called666  exact value667668theorem subsetConjugation.action669  shows subsetConjugation(G) : G ↷ 𝒫(G.carrier)670proof671  have function := subsetConjugation.function with group672  apply Action.mk with group, function673  . intros S hS674    have bounded := powerset.membership_iff.forward with hS675    have value := subsetConjugation.value at G, G.one, S with *676    have fixed : conjugateSet(G, G.one, S) = S := conjugateSet.one with *677    rw [value, fixed]678    rfl679  . intros g hg h hh S hS680    have bounded := powerset.membership_iff.forward with hS681    have closed : g * h ∈ G by typecheck682    have first := subsetConjugation.value at G, g * h, S with *683    have inner := subsetConjugation.value at G, h, S with *684    have innerIn : conjugateSet(G, h, S) ∈ 𝒫(G.carrier) :=685      powerset.membership_iff.backward with (conjugateSet.subset at G, h, S)686    have outer := subsetConjugation.value at G, g, conjugateSet(G, h, S) with *687    have merged : conjugateSet(G, g, conjugateSet(G, h, S)) =688        conjugateSet(G, g * h, S) := conjugateSet.mul with *689    rw [first, inner, outer, merged]690    rfl691692-- The normalizer is the stabilizer of H under conjugation, so a subgroup;693-- it contains H, and it is the whole group exactly for a normal subgroup.694theorem normalizer.eq_stabilizer (H : Set)695  requires bounded : H ⊆ G696  shows normalizer(G, H) =697    stabilizer(subsetConjugation(G), G, 𝒫(G.carrier), H)698proof699  have action := subsetConjugation.action with group700  have HIn := powerset.membership_iff.backward with bounded701  ext g702  constructor703  . intro hg704    obtain ⟨gIn, fixed⟩ := normalizer.membership.forward with hg705    have value := subsetConjugation.value at G, g, H with *706    apply stabilizer.membership.backward707    refine ⟨gIn, ?_⟩708    rw value709    exact fixed710  . intro hg711    obtain ⟨gIn, fixed⟩ := stabilizer.membership.forward with hg712    have value := subsetConjugation.value at G, g, H with *713    rw value at fixed714    exact normalizer.membership.backward with ⟨gIn, fixed⟩715716theorem normalizer.subgroup (H : Set)717  requires bounded : H ⊆ G718  shows Subgroup(normalizer(G, H), G)719proof720  have action := subsetConjugation.action with group721  have HIn := powerset.membership_iff.backward with bounded722  rw normalizer.eq_stabilizer723  exact stabilizer.subgroup with action, HIn724725theorem normalizer.contains (H : Set)726  requires subgroup : Subgroup(H, G)727  shows H ⊆ normalizer(G, H)728proof729  have bounded := Subgroup.subset with subgroup730  intros h hh731  have hIn := bounded with h, hh732  have fixed : conjugateSet(G, h, H) = H733    apply Subset.antisymmetric734    . intros y hy735      obtain ⟨yIn, s, hs, yEq⟩ := conjugateSet.membership.forward with hy736      have closed : conjugate(G, h, s) ∈ H737        rw conjugate.value738        typecheck739      rwa yEq740    . intros y hy741      have yIn := bounded with y, hy742      have criterion : y ∈ conjugateSet(G, h, H) ↔743          conjugate(G, h⁻¹, y) ∈ H := conjugateSet.mem_iff with *744      apply criterion.backward745      rw conjugate.value746      typecheck747  exact normalizer.membership.backward with ⟨hIn, fixed⟩748749theorem normalizer.conjugate_mem (H g h : Set)750  requires bounded : H ⊆ G751  requires hg : g ∈ normalizer(G, H)752  requires hh : h ∈ H753  shows conjugate(G, g, h) ∈ H754proof755  obtain ⟨gIn, fixed⟩ := normalizer.membership.forward with hg756  have member : conjugate(G, g, h) ∈ conjugateSet(G, g, H) :=757    conjugateSet.conjugate_mem with *758  rwa fixed at member759760theorem normalizer.whole_of_normal (N : Set)761  requires normal : NormalSubgroup(N, G)762  shows normalizer(G, N) = G.carrier763proof764  apply Subset.antisymmetric with (normalizer.subset at G, N)765  intros g hg766  have fixed : conjugateSet(G, g, N) = N := NormalSubgroup.conjugateSet with *767  exact normalizer.membership.backward with ⟨hg, fixed⟩768769-- A subgroup is normal in its normalizer.770theorem normalizer.normal (H : Set)771  requires subgroup : Subgroup(H, G)772  shows NormalSubgroup(H, subgroupGroup(G, normalizer(G, H)))773proof774  have bounded := Subgroup.subset with subgroup775  have normalizerSubgroup := normalizer.subgroup with group, bounded776  have contained := normalizer.contains with group, subgroup777  have inner := subgroupGroup.group with group, normalizerSubgroup778  have innerSubgroup : Subgroup(H, subgroupGroup(G, normalizer(G, H)))779    have innerBounded : H ⊆ Group.carrier(subgroupGroup(G, normalizer(G, H)))780      rw subgroupGroup.carrierOf781      exact contained782    have unitIn : Group.one(subgroupGroup(G, normalizer(G, H))) ∈ H783      rw subgroupGroup.unit784      exact Subgroup.one_mem with *785    apply Subgroup.mk with inner, innerBounded, unitIn786    . intros x hx y hy787      have xN := contained with x, hx788      have yN := contained with y, hy789      have value : Group.mul(subgroupGroup(G, normalizer(G, H)))(x, y) =790          G.mul(x, y) := subgroupGroup.mul with *791      rw value792      exact Subgroup.mul_mem with *793    . intros x hx794      have xN := contained with x, hx795      have value : Group.inv(subgroupGroup(G, normalizer(G, H)))(x) =796          G.inv(x) := subgroupGroup.inverse_value with *797      rw value798      exact Subgroup.inv_mem with *799  apply NormalSubgroup.mk with innerSubgroup800  intros g hg n hn801  rw subgroupGroup.carrierOf at hg802  have gIn := normalizer.subset at G, H with g, hg803  have nIn := bounded with n, hn804  have nN := contained with n, hn805  have product : G.mul(g, n) ∈ normalizer(G, H) := Subgroup.mul_mem with *806  have inverseN : G.inv(g) ∈ normalizer(G, H) := Subgroup.inv_mem with *807  have inverseValue : Group.inv(subgroupGroup(G, normalizer(G, H)))(g) =808      G.inv(g) := subgroupGroup.inverse_value with *809  have mulValue : Group.mul(subgroupGroup(G, normalizer(G, H)))(g, n) =810      G.mul(g, n) := subgroupGroup.mul with *811  have mulValue2 : Group.mul(subgroupGroup(G, normalizer(G, H)))(G.mul(g, n), G.inv(g)) =812      G.mul(G.mul(g, n), G.inv(g)) := subgroupGroup.mul with *813  have same : conjugate(subgroupGroup(G, normalizer(G, H)), g, n) =814      conjugate(G, g, n)815    rw [conjugate.value, conjugate.value, inverseValue, mulValue, mulValue2]816    rfl817  rw same818  exact normalizer.conjugate_mem with *819820theorem conjugates.membership (H S : Set)821  requires bounded : H ⊆ G822  shows S ∈ conjugates(G, H) ↔823    ∃ g ∈ G.carrier, S = conjugateSet(G, g, H)824proof825  have action := subsetConjugation.action with group826  have HIn := powerset.membership_iff.backward with bounded827  rw conjugates.eq_orbit828  constructor829  . intro hS830    obtain ⟨SIn, g, gIn, SEq⟩ := orbit.membership.forward with hS831    have value := subsetConjugation.value at G, g, H with *832    witness g833    refine ⟨gIn, ?_⟩834    rw [SEq, value]835    rfl836  . intro given837    obtain ⟨g, gIn, SEq⟩ := given838    have value := subsetConjugation.value at G, g, H with *839    have SIn : S ∈ 𝒫(G.carrier)840      rw SEq841      exact powerset.membership_iff.backward with842        (conjugateSet.subset at G, g, H)843    apply orbit.membership.backward844    refine ⟨SIn, g, gIn, ?_⟩845    rw [SEq, value]846    rfl847848theorem conjugates.self (H : Set)849  requires bounded : H ⊆ G850  shows H ∈ conjugates(G, H)851proof852  have unitIn : G.one ∈ G := Group.one_mem with *853  have fixed : conjugateSet(G, G.one, H) = H := conjugateSet.one with *854  have criterion := conjugates.membership at G, H, H with group, bounded855  apply criterion.backward856  witness G.one857  refine ⟨unitIn, ?_⟩858  symm859  exact fixed860861-- The number of conjugates of H is the index of its normalizer.862theorem conjugates.cardinality_eq_index (H : Set)863  requires bounded : H ⊆ G864  requires finite : Finite(G)865  shows cardinality(conjugates(G, H)) = index(G, normalizer(G, H))866proof867  have action := subsetConjugation.action with group868  have HIn := powerset.membership_iff.backward with bounded869  have same := orbit.cardinality_eq_index with action, HIn, finite870  rw [conjugates.eq_orbit, normalizer.eq_stabilizer]871  exact same872873end SubsetConjugation874