Grace/Cumulus/Algebra/Group/Center.g17

Open in Workbench Download source

Imports

Generated

Declarations

Source

1-- The center of a group and centralizers of subsets: both are subgroups,2-- the center is a normal abelian subgroup, and it is the whole group3-- exactly when the group is abelian4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Group.Center10import Generated1112-- The elements commuting with everything in S, and with everything.13def centralizer (G S : Set) : Set := { z ∈ G.carrier | ∀ x ∈ S, G.mul(z, x) = G.mul(x, z) }14def center (G : Set) : Set := centralizer(G, G.carrier)1516theorem center.membership (G z : Set)17  shows z ∈ center(G) ↔ z ∈ G.carrier ∧ (∀ x ∈ G.carrier, G.mul(z, x) = G.mul(x, z))18proof19  simp [center, centralizer]2021theorem centralizer.subset (G S : Set)22  shows centralizer(G, S) ⊆ G.carrier23proof24  intros z hz25  have parts := centralizer.membership.forward with hz26  exact parts.left2728theorem center.subset (G : Set)29  shows center(G) ⊆ G.carrier30proof31  intros z hz32  have parts := center.membership.forward with hz33  exact parts.left3435theorem center.eq_centralizer (G : Set)36  shows center(G) = centralizer(G, G.carrier)37proof38  simp [center]3940theorem centralizer.antitone (G S T : Set)41  requires included : S ⊆ T42  shows centralizer(G, T) ⊆ centralizer(G, S)43proof44  intros z hz45  have parts := centralizer.membership.forward with hz46  apply centralizer.membership.backward47  refine ⟨parts.left, ?_⟩48  intros x hx49  have xT := included with x, hx50  exact parts.right with x, xT5152theorem center.subset_centralizer (G S : Set)53  requires bounded : S ⊆ G.carrier54  shows center(G) ⊆ centralizer(G, S)55proof56  rw center.eq_centralizer57  exact centralizer.antitone at G, S, G.carrier with bounded5859theorem centralizer.empty (G : Set)60  shows centralizer(G, ∅) = G.carrier61proof62  apply Subset.antisymmetric with (centralizer.subset at G, ∅)63  intros z hz64  apply centralizer.membership.backward65  refine ⟨hz, ?_⟩66  intros x hx67  exfalso68  exact set.empty with hx6970theorem centralizer.singleton_mem (G x : Set)71  requires hx : x ∈ G.carrier72  shows x ∈ centralizer(G, {x})73proof74  apply centralizer.membership.backward75  refine ⟨hx, ?_⟩76  intros y hy77  have equal := singleton.membership.forward with hy78  rw equal79  rfl8081section CenterLaws82variable (G : Set)83hypothesis group : Group(G)8485theorem centralizer.commute (S z : Set) (x : G)86  requires hz : z ∈ centralizer(G, S)87  requires hx : x ∈ S88  shows z * x = x * z89proof90  have parts := centralizer.membership.forward with hz91  exact parts.right with x, hx9293theorem center.commute (z : Set) (x : G)94  requires hz : z ∈ center(G)95  shows z * x = x * z96proof97  have parts := center.membership.forward with hz98  have xIn : x ∈ G by assumption99  exact parts.right with x, xIn100101theorem centralizer.one_mem (S : Set)102  requires bounded : S ⊆ G103  shows G.one ∈ centralizer(G, S)104proof105  apply centralizer.membership.backward106  refine ⟨(Group.one_mem with group), ?_⟩107  intros x hx108  have xIn := bounded with x, hx109  rw [one_mul, mul_one]110  rfl111112theorem centralizer.subgroup (S : Set)113  requires bounded : S ⊆ G114  shows Subgroup(centralizer(G, S), G)115proof116  have unitIn := centralizer.one_mem with group, bounded117  apply Subgroup.mk with group, (centralizer.subset at G, S), unitIn118  . intros z hz w hw119    have pz := centralizer.membership.forward with hz120    have pw := centralizer.membership.forward with hw121    have zIn := pz.left122    have wIn := pw.left123    apply centralizer.membership.backward124    refine ⟨(Group.mul_mem with *), ?_⟩125    intros x hx126    have xIn := bounded with x, hx127    have commuteZ := pz.right with x, hx128    have commuteW := pw.right with x, hx129    rw [mul_assoc, commuteW, ← mul_assoc, commuteZ, mul_assoc]130    rfl131  . intros z hz132    have pz := centralizer.membership.forward with hz133    have zIn := pz.left134    apply centralizer.membership.backward135    refine ⟨(Group.inv_mem with *), ?_⟩136    intros x hx137    have xIn := bounded with x, hx138    have commute := pz.right with x, hx139    have criterion : z⁻¹ * x = x * z⁻¹ ↔ x = z * (x * z⁻¹) := inv_mul_eq_iff_eq_mul with *140    apply criterion.backward141    rw [← mul_assoc, commute, mul_inv_cancel_right]142    rfl143144theorem center.subgroup145  shows Subgroup(center(G), G)146proof147  rw center.eq_centralizer148  exact centralizer.subgroup with group, (Subset.reflexive at G.carrier)149150theorem center.normal151  shows NormalSubgroup(center(G), G)152proof153  have subgroup := center.subgroup with group154  apply NormalSubgroup.mk with subgroup155  intros g hg z hz156  have zIn : z ∈ G := Subgroup.mem_carrier with *157  have commute : z * g = g * z := center.commute with *158  have swapped : g * z = z * g by cc159  have fixed : conjugate(G, g, z) = z := conjugate.of_commute with *160  rwa fixed161162theorem center.commutative163  shows Commutative(center(G), G.mul)164proof165  intros z hz w hw166  have wIn := center.subset at G with w, hw167  exact center.commute with *168169theorem center.eq_carrier_iff170  shows center(G) = G.carrier ↔ Commutative(G.carrier, G.mul)171proof172  constructor173  . intros equal x hx y hy174    have xCenter : x ∈ center(G) by rwa equal175    exact center.commute with *176  . intro commutative177    apply Subset.antisymmetric with (center.subset at G)178    intros x hx179    apply center.membership.backward180    refine ⟨hx, ?_⟩181    intros y hy182    exact commutative with x, hx, y, hy183184theorem centralizer.self_mem_iff (S : Set)185  requires bounded : S ⊆ G186  shows S ⊆ centralizer(G, S) ↔ Commutative(S, G.mul)187proof188  constructor189  . intros included x hx y hy190    have xCentral := included with x, hx191    have yIn := bounded with y, hy192    exact centralizer.commute with *193  . intros commutative x hx194    have xIn := bounded with x, hx195    apply centralizer.membership.backward196    refine ⟨xIn, ?_⟩197    intros y hy198    exact commutative with x, hx, y, hy199200theorem centralizer.pow_mem (x : G) (n : Nat)201  shows x ^ n ∈ centralizer(G, {x})202proof203  have bounded : {x} ⊆ G204    intros y hy205    have equal := singleton.membership.forward with hy206    rwa equal207  have subgroup := centralizer.subgroup at G, {x} with group, bounded208  have member : x ∈ centralizer(G, {x}) := centralizer.singleton_mem with *209  exact Subgroup.pow_mem with *210211theorem centralizer.generated_subset (S : Set)212  requires bounded : S ⊆ G213  shows generatedSubgroup(G, S) ⊆ centralizer(G, centralizer(G, S))214proof215  have subgroup := centralizer.subgroup at G, centralizer(G, S) with group, (centralizer.subset at G, S)216  have included : S ⊆ centralizer(G, centralizer(G, S))217    intros x hx218    have xIn := bounded with x, hx219    apply centralizer.membership.backward220    refine ⟨xIn, ?_⟩221    intros z hz222    have commute : z * x = x * z := centralizer.commute with *223    symm224    exact commute225  exact generatedSubgroup.least with subgroup, included226227instance center.inv_mem (z : Set)228  requires hz : z ∈ center(G)229  shows z⁻¹ ∈ center(G)230proof231  have subgroup := center.subgroup with group232  exact Subgroup.inv_mem with *233234instance center.mul_mem (z w : Set)235  requires hz : z ∈ center(G)236  requires hw : w ∈ center(G)237  shows z * w ∈ center(G)238proof239  have subgroup := center.subgroup with group240  exact Subgroup.mul_mem with *241242theorem center.conjugate_fixed (g : G) (z : Set)243  requires hz : z ∈ center(G)244  shows conjugate(G, g, z) = z245proof246  have zIn := center.subset at G with z, hz247  have commute : z * g = g * z := center.commute with *248  have swapped : g * z = z * g by cc249  exact conjugate.of_commute with *250251end CenterLaws252253theorem center.of_abelian (G : Set)254  requires abelian : AbelianGroup(G)255  shows center(G) = G.carrier256proof257  have group := AbelianGroup.to_group with abelian258  have commutative := IsAbelianGroup.commutative with (AbelianGroup.parts with abelian)259  have criterion := center.eq_carrier_iff with group260  exact criterion.backward with commutative261262theorem center.image_subset (f G H : Set)263  requires hom : f : G →* H264  requires surjective : SurjectiveBetween(f, G.carrier, H.carrier)265  shows functionImage(f, center(G), H.carrier) ⊆ center(H)266proof267  have group := GroupHom.source with hom268  have target := GroupHom.target with hom269  have function := GroupHom.function with hom270  intros y hy271  obtain ⟨yIn, z, hz, yEq⟩ := functionImage.membership.forward with hy272  have zIn := center.subset at G with z, hz273  apply center.membership.backward274  refine ⟨yIn, ?_⟩275  intros w hw276  obtain ⟨x, hx, edge⟩ := surjective.right with w, hw277  have wEq := FunctionBetween.apply_value with function, hx, edge278  have commute : z * x = x * z := center.commute with *279  have first : f(z * x) = f(z) * f(x) := GroupHom.map_mul with *280  have second : f(x * z) = f(x) * f(z) := GroupHom.map_mul with *281  cc282