Grace/Cumulus/Algebra/Group/Normal.g17

Open in Workbench Download source

Imports

Kernel · Coset

Declarations

Source

1-- Conjugation and normal subgroups: conjugation by a fixed element is an2-- automorphism, kernels are normal, every subgroup of an abelian group is3-- normal, and a subgroup is normal exactly when its left and right cosets4-- agree5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Group.Normal11import Kernel12import Coset1314-- The conjugate g * x * g⁻¹ of x by g.15def conjugate (G g x : Set) : Set := G.mul(G.mul(g, x), G.inv(g))1617theorem conjugate.value (G g x : Set)18  shows conjugate(G, g, x) = G.mul(G.mul(g, x), G.inv(g))19proof20  simp [conjugate]2122section Conjugation23variable (G : Set)24hypothesis group : Group(G)2526instance conjugate.mem (g x : G)27  shows conjugate(G, g, x) ∈ G28proof29  rw conjugate.value30  typecheck3132theorem conjugate.one (g : G)33  shows conjugate(G, g, G.one) = G.one34proof35  simp [conjugate.value, mul_one, Group.mul_inv]3637theorem conjugate.by_one (x : G)38  shows conjugate(G, G.one, x) = x39proof40  simp [conjugate.value, one_mul, inv_one, mul_one]4142theorem conjugate.mul (g x y : G)43  shows conjugate(G, g, x * y) = conjugate(G, g, x) * conjugate(G, g, y)44proof45  rw [conjugate.value, conjugate.value, conjugate.value]46  group_simp4748theorem conjugate.inv (g x : G)49  shows conjugate(G, g, x⁻¹) = conjugate(G, g, x)⁻¹50proof51  simp [conjugate.value, mul_inv_rev, inv_inv, mul_assoc]5253theorem conjugate.conjugate (g h x : G)54  shows conjugate(G, g, conjugate(G, h, x)) = conjugate(G, g * h, x)55proof56  simp [conjugate.value, mul_inv_rev, mul_assoc]5758theorem conjugate.cancel (g x : G)59  shows conjugate(G, g⁻¹, conjugate(G, g, x)) = x60proof61  rw [conjugate.value, conjugate.value]62  group_simp6364theorem conjugate.injective (g x y : G)65  requires equal : conjugate(G, g, x) = conjugate(G, g, y)66  shows x = y67proof68  have cancelX : conjugate(G, g⁻¹, conjugate(G, g, x)) = x := conjugate.cancel with *69  have cancelY : conjugate(G, g⁻¹, conjugate(G, g, y)) = y := conjugate.cancel with *70  cc7172theorem conjugate.of_commute (g x : G)73  requires commute : g * x = x * g74  shows conjugate(G, g, x) = x75proof76  rw [conjugate.value, commute, mul_inv_cancel_right]77  rfl7879theorem conjugate.commute_of_fixed (g x : G)80  requires fixed : conjugate(G, g, x) = x81  shows g * x = x * g82proof83  rw conjugate.value at fixed84  have criterion : g * x * g⁻¹ = x ↔ g * x = x * g := mul_inv_eq_iff_eq_mul with *85  exact criterion.forward with fixed8687end Conjugation8889-- Conjugation by g as a function on the carrier.90defgraph conjugation (G g : Set) (x ∈ G.carrier) : G.carrier := conjugate(G, g, x)91requires group : Group(G)92requires hg : g ∈ G.carrier93proof94  exact conjugate.mem with group, hg, member9596section ConjugationMap97variable (G : Set)98hypothesis group : Group(G)99100theorem conjugation.hom (g : G)101  shows conjugation(G, g) : G →* G102proof103  have function := conjugation.function at G, g with *104  apply GroupHom.mk with group, group, function105  intros x hx y hy106  have closed : x * y ∈ G by typecheck107  have vx := conjugation.value at G, g, x with *108  have vy := conjugation.value at G, g, y with *109  have output := conjugation.value at G, g, x * y with *110  have merged : conjugate(G, g, x * y) = conjugate(G, g, x) * conjugate(G, g, y) := conjugate.mul with *111  cc112113theorem conjugation.injective (g : G)114  shows InjectiveBetween(conjugation(G, g), G.carrier, G.carrier)115proof116  have function := conjugation.function at G, g with *117  constructor118  . exact function119  . intros x hx y hy z hz hxz hyz120    have vx := FunctionBetween.apply_value with function, hx, hxz121    have vy := FunctionBetween.apply_value with function, hy, hyz122    have cx := conjugation.value at G, g, x with *123    have cy := conjugation.value at G, g, y with *124    have equal : conjugate(G, g, x) = conjugate(G, g, y) by cc125    exact conjugate.injective with *126127theorem conjugation.surjective (g : G)128  shows SurjectiveBetween(conjugation(G, g), G.carrier, G.carrier)129proof130  have function := conjugation.function at G, g with *131  constructor132  . exact function133  . intros y hy134    have preimage : conjugate(G, g⁻¹, y) ∈ G by typecheck135    have cancel : conjugate(G, (g⁻¹)⁻¹, conjugate(G, g⁻¹, y)) = y := conjugate.cancel with *136    rw inv_inv at cancel137    have value := conjugation.value at G, g, conjugate(G, g⁻¹, y) with *138    have edge := FunctionBetween.relates_apply with function, preimage139    refine ⟨conjugate(G, g⁻¹, y), preimage, ?_⟩140    rw [value, cancel] at edge141    exact edge142143theorem conjugation.bijective (g : G)144  shows BijectiveBetween(conjugation(G, g), G.carrier, G.carrier)145proof146  constructor147  . exact conjugation.injective with *148  . exact conjugation.surjective with *149150end ConjugationMap151152-- NormalSubgroup(N, G): a subgroup closed under conjugation by every153-- element of G.154predicate NormalSubgroup (N G : Set) :=155  Subgroup(N, G) ∧ (∀ g ∈ G.carrier, ∀ n ∈ N, conjugate(G, g, n) ∈ N)156157notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis NormalSubgroup(N, G) for N158notation postfix 90 "⁻¹" => apply(G.inv, _) via hypothesis NormalSubgroup(N, G) for N159notation infixr 80 "^" => groupPow(G, _, _) via hypothesis NormalSubgroup(N, G) for N160161theorem NormalSubgroup.subgroup (N G : Set)162  requires normal : NormalSubgroup(N, G)163  shows Subgroup(N, G)164proof165  exact normal.left166167theorem NormalSubgroup.conjugate_mem (N G g n : Set)168  requires normal : NormalSubgroup(N, G)169  requires hg : g ∈ G.carrier170  requires hn : n ∈ N171  shows conjugate(G, g, n) ∈ N172proof173  exact normal.right with g, hg, n, hn174175theorem NormalSubgroup.mk (N G : Set)176  requires subgroup : Subgroup(N, G)177  requires closed : ∀ g ∈ G.carrier, ∀ n ∈ N, conjugate(G, g, n) ∈ N178  shows NormalSubgroup(N, G)179proof180  unfold NormalSubgroup181  exact ⟨subgroup, closed⟩182183section NormalLaws184variable (G N : Set)185hypothesis group : Group(G)186hypothesis normal : NormalSubgroup(N, G)187188theorem NormalSubgroup.mul_mem (g : G) (n : N)189  shows g * n * g⁻¹ ∈ N190proof191  have member : conjugate(G, g, n) ∈ N := NormalSubgroup.conjugate_mem with *192  rwa conjugate.value at member193194theorem NormalSubgroup.inv_mul_mem (g : G) (n : N)195  shows g⁻¹ * n * g ∈ N196proof197  have member : conjugate(G, g⁻¹, n) ∈ N := NormalSubgroup.conjugate_mem with *198  rw [conjugate.value, inv_inv] at member199  exact member200201-- Normality through cosets: left and right cosets coincide.202theorem NormalSubgroup.left_eq_right (g : G)203  shows leftCoset(G, g, N) = rightCoset(G, g, N)204proof205  have subgroup := NormalSubgroup.subgroup with normal206  ext y207  constructor208  . intro hy209    obtain ⟨yIn, n, hn, yEq⟩ := leftCoset.membership.forward with hy210    have conj : g * n * g⁻¹ ∈ N := NormalSubgroup.mul_mem with *211    apply rightCoset.membership.backward212    refine ⟨yIn, g * n * g⁻¹, conj, ?_⟩213    rw [yEq, inv_mul_cancel_right]214    rfl215  . intro hy216    obtain ⟨yIn, n, hn, yEq⟩ := rightCoset.membership.forward with hy217    have conj : g⁻¹ * n * g ∈ N := NormalSubgroup.inv_mul_mem with *218    apply leftCoset.membership.backward219    refine ⟨yIn, g⁻¹ * n * g, conj, ?_⟩220    rw [yEq, ← mul_assoc, mul_inv_cancel_left]221    rfl222223-- In a normal subgroup the order of a product does not matter for224-- membership.225theorem NormalSubgroup.mul_mem_comm (x y : G)226  requires member : x * y ∈ N227  shows y * x ∈ N228proof229  have conj : y * (x * y) * y⁻¹ ∈ N := NormalSubgroup.mul_mem with *230  rw [← mul_assoc, mul_inv_cancel_right] at conj231  exact conj232233end NormalLaws234235section NormalConstructions236variable (G : Set)237hypothesis group : Group(G)238239theorem NormalSubgroup.whole240  shows NormalSubgroup(G.carrier, G)241proof242  have subgroup := Subgroup.whole with group243  apply NormalSubgroup.mk with subgroup244  intros g hg n hn245  typecheck246247theorem NormalSubgroup.trivial248  shows NormalSubgroup({G.one}, G)249proof250  have subgroup := Subgroup.trivial with group251  apply NormalSubgroup.mk with subgroup252  intros g hg n hn253  have equal := singleton.membership.forward with hn254  have fixed : conjugate(G, g, G.one) = G.one := conjugate.one with *255  rw [equal, fixed]256  exact singleton.self257258theorem NormalSubgroup.intersection (N M : Set)259  requires normalN : NormalSubgroup(N, G)260  requires normalM : NormalSubgroup(M, G)261  shows NormalSubgroup(N ∩ M, G)262proof263  have subgroup := Subgroup.intersection with group, (NormalSubgroup.subgroup with normalN), (NormalSubgroup.subgroup with normalM)264  apply NormalSubgroup.mk with subgroup265  intros g hg n hn266  obtain ⟨nN, nM⟩ := intersection.membership.forward with hn267  have inN : conjugate(G, g, n) ∈ N := NormalSubgroup.conjugate_mem with *268  have inM : conjugate(G, g, n) ∈ M := NormalSubgroup.conjugate_mem with *269  exact intersection.membership.backward with ⟨inN, inM⟩270271theorem NormalSubgroup.of_left_eq_right (N : Set)272  requires subgroup : Subgroup(N, G)273  requires cosets : ∀ g ∈ G, leftCoset(G, g, N) = rightCoset(G, g, N)274  shows NormalSubgroup(N, G)275proof276  apply NormalSubgroup.mk with subgroup277  intros g hg n hn278  have gn : g * n ∈ leftCoset(G, g, N) := leftCoset.mul_mem with *279  have equal := cosets with g, hg280  rw equal at gn281  obtain ⟨gnIn, m, hm, gnEq⟩ := rightCoset.membership.forward with gn282  rw [conjugate.value, gnEq, mul_inv_cancel_right]283  exact hm284285theorem NormalSubgroup.iff_left_eq_right (N : Set)286  requires subgroup : Subgroup(N, G)287  shows NormalSubgroup(N, G) ↔ ∀ g ∈ G, leftCoset(G, g, N) = rightCoset(G, g, N)288proof289  constructor290  . intros normal g hg291    exact NormalSubgroup.left_eq_right with *292  . intro cosets293    exact NormalSubgroup.of_left_eq_right with *294295end NormalConstructions296297theorem NormalSubgroup.of_abelian (G N : Set)298  requires abelian : AbelianGroup(G)299  requires subgroup : Subgroup(N, G)300  shows NormalSubgroup(N, G)301proof302  have group := AbelianGroup.to_group with abelian303  apply NormalSubgroup.mk with subgroup304  intros g hg n hn305  have nIn : n ∈ G.carrier := Subgroup.mem_carrier with *306  have commute : g * n = n * g := mul_comm with *307  have fixed : conjugate(G, g, n) = n := conjugate.of_commute with *308  rwa fixed309310section NormalHoms311variable (f G H : Set)312hypothesis hom : f : G →* H313314theorem GroupHom.kernel_normal315  shows NormalSubgroup(ker(f), G)316proof317  have group := GroupHom.source with hom318  have target := GroupHom.target with hom319  have subgroup := GroupHom.kernel_subgroup with hom320  apply NormalSubgroup.mk with subgroup321  intros g hg n hn322  obtain ⟨nIn, vn⟩ := kernel.membership.forward with hn323  have vanishes : f(conjugate(G, g, n)) = H.one324    rw [conjugate.value, GroupHom.map_mul, GroupHom.map_mul, GroupHom.map_inv, vn, mul_one, Group.mul_inv]325    rfl326  exact kernel.of_value with (conjugate.mem with *), vanishes327328theorem NormalSubgroup.preimage (K : Set)329  requires normal : NormalSubgroup(K, H)330  shows NormalSubgroup(functionPreimage(f, G.carrier, K), G)331proof332  have group := GroupHom.source with hom333  have target := GroupHom.target with hom334  have subgroup := GroupHom.preimage_subgroup with hom, (NormalSubgroup.subgroup with normal)335  apply NormalSubgroup.mk with subgroup336  intros g hg n hn337  have parts := functionPreimage.membership.forward with hn338  have nIn := parts.left339  have conj : conjugate(H, f(g), f(n)) ∈ K := NormalSubgroup.conjugate_mem with normal, (GroupHom.map_mem with *), parts.right340  have value : f(conjugate(G, g, n)) ∈ K341    rw [conjugate.value, GroupHom.map_mul, GroupHom.map_mul, GroupHom.map_inv]342    rwa conjugate.value at conj343  exact functionPreimage.of_apply with (conjugate.mem with *), value344345theorem NormalSubgroup.image_of_surjective (N : Set)346  requires surjective : SurjectiveBetween(f, G.carrier, H.carrier)347  requires normal : NormalSubgroup(N, G)348  shows NormalSubgroup(functionImage(f, N, H.carrier), H)349proof350  have group := GroupHom.source with hom351  have target := GroupHom.target with hom352  have function := GroupHom.function with hom353  have subgroupN := NormalSubgroup.subgroup with normal354  have subgroup := GroupHom.image_subgroup with hom, subgroupN355  apply NormalSubgroup.mk with subgroup356  intros h hh y hy357  obtain ⟨yIn, n, hn, yEq⟩ := functionImage.membership.forward with hy358  obtain ⟨g, hg, edge⟩ := surjective.right with h, hh359  have hEq := FunctionBetween.apply_value with function, hg, edge360  have nIn : n ∈ G := Subgroup.mem_carrier with *361  have conj : conjugate(G, g, n) ∈ N := NormalSubgroup.conjugate_mem with *362  have closed : conjugate(H, h, y) ∈ H by typecheck363  apply functionImage.membership.backward364  refine ⟨closed, conjugate(G, g, n), conj, ?_⟩365  rw [conjugate.value, conjugate.value, GroupHom.map_mul, GroupHom.map_mul, GroupHom.map_inv, hEq, yEq]366  rfl367368end NormalHoms369