Grace/Cumulus/Algebra/Group/Basic.g17

Open in Workbench Download source

Imports

Core

Declarations

Source

1-- Bundled groups: a group as one structure of its carrier, operation, unit,2-- and inverse, the laws of a group under their standard names, and the3-- group rewrite set4-- 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.Basic10import Core1112-- A group is a structure of its carrier, its operation graph, its unit, and13-- its inverse graph, built by Group.mk(A, m, e, i) and read back by the14-- projections G.carrier, G.mul, G.one, and G.inv. The operation applies to15-- two arguments, G.mul(x, y), and the inverse as a function, G.inv(x).16-- Group(G) says that G is such a structure whose data satisfy the laws17-- below, under their standard names; Group.Data(G) is the shape alone, and18-- Group.intro builds a group from its four pieces and the laws.19structure Group20  | carrier : Set21  | mul : carrier × carrier → carrier22  | one : carrier23  | inv : carrier → carrier24  where25    mul_assoc : ∀ a b c ∈ carrier, mul(mul(a, b), c) = mul(a, mul(b, c))26    one_mul : ∀ a ∈ carrier, mul(one, a) = a27    mul_one : ∀ a ∈ carrier, mul(a, one) = a28    inv_mul : ∀ a ∈ carrier, mul(inv(a), a) = one29    mul_inv : ∀ a ∈ carrier, mul(a, inv(a)) = one3031-- The projection laws of a constructed group as one rewrite set.32tactic group_projections := simp [Group.mk.carrier, Group.mk.mul, Group.mk.one, Group.mk.inv]3334-- The monoid and the abelian group as properties of the same structure:35-- Monoid(G) is the unbundled monoid at the projections, and AbelianGroup(G)36-- is a group whose operation commutes. IsMonoid(A, m, e), IsGroup(A, m, e, i),37-- and IsAbelianGroup(A, m, e, i) remain the forms over separate pieces.38predicate Monoid (G : Set) := Group.Data(G) ∧ IsMonoid(G.carrier, G.mul, G.one)39predicate AbelianGroup (G : Set) := Group(G) ∧ Commutative(G.carrier, G.mul)4041-- The operation is written a * b and the inverse a⁻¹ wherever a hypothesis42-- in scope supplies the group; the operands' membership in G.carrier43-- selects the group when several are in scope. Under the same hypotheses a44-- binder (a : G) is a set variable with a ∈ G.carrier.45notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis Monoid(G) for G.carrier46notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis Group(G) for G.carrier47notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis AbelianGroup(G) for G.carrier48notation postfix 90 "⁻¹" => apply(G.inv, _) via hypothesis Group(G) for G.carrier49notation postfix 90 "⁻¹" => apply(G.inv, _) via hypothesis AbelianGroup(G) for G.carrier5051-- Bridges between the structure and the forms over separate pieces.52theorem Group.parts (G : Set)53  requires group : Group(G)54  shows IsGroup(G.carrier, G.mul, G.one, G.inv)55proof56  obtain ⟨shape, mulF, oneIn, invF, assoc, oneMul, mulOne, invMul, mulInv⟩ := group57  unfold IsGroup58  constructor59  . unfold IsMonoid60    constructor61    . unfold IsSemigroup62      constructor63      . exact mulF64      . unfold Associative65        exact assoc66    . unfold Identity67      refine ⟨oneIn, ?_⟩68      intros x xIn69      have left := oneMul with x, xIn70      have right := mulOne with x, xIn71      exact ⟨left, right⟩72  . unfold Inverse73    refine ⟨invF, ?_⟩74    intros x xIn75    have left := invMul with x, xIn76    have right := mulInv with x, xIn77    exact ⟨left, right⟩7879theorem Group.of_parts (A m e i : Set)80  requires group : IsGroup(A, m, e, i)81  shows Group(Group.mk(A, m, e, i))82proof83  have monoid := IsGroup.monoid with group84  have mulF := IsGroup.magma with group85  have assoc := IsMonoid.associative with monoid86  have oneIn := IsMonoid.unit_in_carrier with monoid87  obtain ⟨invF, inverses⟩ := IsGroup.inverse with group88  apply Group.intro89  . exact mulF90  . exact oneIn91  . exact invF92  . unfold Associative at assoc93    exact assoc94  . intros x xIn95    exact IsMonoid.left_identity with monoid, xIn96  . intros x xIn97    exact IsMonoid.right_identity with monoid, xIn98  . intros x xIn99    have both := inverses with x, xIn100    exact both.left101  . intros x xIn102    have both := inverses with x, xIn103    exact both.right104105theorem Monoid.parts (G : Set)106  requires monoid : Monoid(G)107  shows IsMonoid(G.carrier, G.mul, G.one)108proof109  obtain ⟨shape, laws⟩ := monoid110  exact laws111112theorem Monoid.of_parts (A m e i : Set)113  requires monoid : IsMonoid(A, m, e)114  shows Monoid(Group.mk(A, m, e, i))115proof116  have shape := Group.mk.data at A, m, e, i117  unfold Monoid118  group_projections119120theorem AbelianGroup.parts (G : Set)121  requires abelian : AbelianGroup(G)122  shows IsAbelianGroup(G.carrier, G.mul, G.one, G.inv)123proof124  obtain ⟨group, commutative⟩ := abelian125  have parts := Group.parts with group126  unfold IsAbelianGroup127  exact ⟨parts, commutative⟩128129theorem AbelianGroup.of_parts (A m e i : Set)130  requires abelian : IsAbelianGroup(A, m, e, i)131  shows AbelianGroup(Group.mk(A, m, e, i))132proof133  have group := Group.of_parts with (IsAbelianGroup.group with abelian)134  have commutative := IsAbelianGroup.commutative with abelian135  unfold AbelianGroup136  group_projections137138theorem Group.to_monoid (G : Set)139  requires group : Group(G)140  shows Monoid(G)141proof142  obtain ⟨shape, rest⟩ := group143  have parts := Group.parts with group144  unfold Monoid145  exact ⟨shape, IsGroup.monoid with parts⟩146147theorem AbelianGroup.to_group (G : Set)148  requires abelian : AbelianGroup(G)149  shows Group(G)150proof151  obtain ⟨group, commutative⟩ := abelian152  exact group153154-- A group is the constructor applied to its projections.155theorem Group.eta_of_group (G : Set)156  requires group : Group(G)157  shows G = Group.mk(G.carrier, G.mul, G.one, G.inv)158proof159  obtain ⟨shape, rest⟩ := group160  exact Group.eta with shape161162section GroupLaws163variable (G : Set)164hypothesis group : Group(G)165166-- Closure: the operation, unit, and inverse stay in the carrier. These are167-- instances, so the membership of a compound term is synthesized.168instance Group.mul_mem (a b : G)169  shows a * b ∈ G170proof171  have monoid := IsGroup.monoid with (Group.parts with group)172  exact IsMonoid.closed with monoid, *173174instance Group.one_mem175  shows G.one ∈ G176proof177  have monoid := IsGroup.monoid with (Group.parts with group)178  exact IsMonoid.unit_in_carrier with monoid179180instance Group.inv_mem (a : G)181  shows a⁻¹ ∈ G182proof183  have parts := Group.parts with group184  exact IsGroup.inverse_closed with parts, *185186theorem Group.operation_function187  shows G.mul : G.carrier × G.carrier → G.carrier188proof189  have monoid := IsGroup.monoid with (Group.parts with group)190  have semigroup := IsMonoid.semigroup with monoid191  exact IsSemigroup.magma with semigroup192193theorem Group.inverse_function194  shows G.inv : G.carrier → G.carrier195proof196  obtain ⟨function, laws⟩ := IsGroup.inverse with (Group.parts with group)197  exact function198199-- The laws, under their standard names: the familiar underscore names, and200-- the dotted Group.inv_mul, Group.mul_inv, and Group.inv_involutive.201theorem mul_assoc (a b c : G)202  shows a * b * c = a * (b * c)203proof204  have monoid := IsGroup.monoid with (Group.parts with group)205  have associative := IsMonoid.associative with monoid206  exact Associative.law with associative, *207208theorem one_mul (a : G)209  shows G.one * a = a210proof211  have monoid := IsGroup.monoid with (Group.parts with group)212  exact IsMonoid.left_identity with monoid, *213214theorem mul_one (a : G)215  shows a * G.one = a216proof217  have monoid := IsGroup.monoid with (Group.parts with group)218  exact IsMonoid.right_identity with monoid, *219220theorem Group.inv_mul (a : G)221  shows a⁻¹ * a = G.one222proof223  have parts := Group.parts with group224  exact IsGroup.inverse_left with parts, *225226theorem Group.mul_inv (a : G)227  shows a * a⁻¹ = G.one228proof229  have parts := Group.parts with group230  exact IsGroup.inverse_right with parts, *231232theorem inv_mul_cancel_left (a b : G)233  shows a⁻¹ * (a * b) = b234proof235  rw [← mul_assoc, Group.inv_mul, one_mul]236  rfl237238theorem mul_inv_cancel_left (a b : G)239  shows a * (a⁻¹ * b) = b240proof241  rw [← mul_assoc, Group.mul_inv, one_mul]242  rfl243244theorem mul_inv_cancel_right (a b : G)245  shows a * b * b⁻¹ = a246proof247  rw [mul_assoc, Group.mul_inv, mul_one]248  rfl249250theorem inv_mul_cancel_right (a b : G)251  shows a * b⁻¹ * b = a252proof253  rw [mul_assoc, Group.inv_mul, mul_one]254  rfl255256theorem mul_left_cancel (a b c : G)257  requires equal : a * b = a * c258  shows b = c259proof260  calc261    b = a⁻¹ * (a * b) := by rw inv_mul_cancel_left262    _ = a⁻¹ * (a * c) := by rw equal263    _ = c := by rw inv_mul_cancel_left264265theorem mul_right_cancel (a b c : G)266  requires equal : a * b = c * b267  shows a = c268proof269  calc270    a = a * b * b⁻¹ := by rw mul_inv_cancel_right271    _ = c * b * b⁻¹ := by rw equal272    _ = c := by rw mul_inv_cancel_right273274theorem mul_right_inj (a b c : G)275  shows a * b = a * c ↔ b = c276proof277  constructor278  . intro equal279    exact mul_left_cancel with *280  . intro equal281    rw equal282    rfl283284theorem mul_left_inj (a b c : G)285  shows a * b = c * b ↔ a = c286proof287  constructor288  . intro equal289    exact mul_right_cancel with *290  . intro equal291    rw equal292    rfl293294theorem inv_one295  shows G.one⁻¹ = G.one296proof297  have cancel : G.one⁻¹ * G.one = G.one := Group.inv_mul with *298  rwa mul_one at cancel299300theorem eq_inv_of_mul_eq_one_left (a b : G)301  requires equal : a * b = G.one302  shows a = b⁻¹303proof304  calc305    a = a * b * b⁻¹ := by rw mul_inv_cancel_right306    _ = b⁻¹ := by rw [equal, one_mul]307308theorem eq_inv_of_mul_eq_one_right (a b : G)309  requires equal : a * b = G.one310  shows b = a⁻¹311proof312  calc313    b = a⁻¹ * (a * b) := by rw inv_mul_cancel_left314    _ = a⁻¹ := by rw [equal, mul_one]315316theorem inv_eq_of_mul_eq_one_right (a b : G)317  requires equal : a * b = G.one318  shows a⁻¹ = b319proof320  symm321  exact eq_inv_of_mul_eq_one_right with *322323theorem inv_inv (a : G)324  shows (a⁻¹)⁻¹ = a325proof326  have cancel : a⁻¹ * a = G.one := Group.inv_mul with *327  exact inv_eq_of_mul_eq_one_right with *328329theorem Group.inv_involutive (a : G)330  shows (a⁻¹)⁻¹ = a331proof332  exact inv_inv with *333334theorem mul_inv_rev (a b : G)335  shows (a * b)⁻¹ = b⁻¹ * a⁻¹336proof337  have product : a * b * (b⁻¹ * a⁻¹) = G.one338    rw [mul_assoc, mul_inv_cancel_left, Group.mul_inv]339    rfl340  exact inv_eq_of_mul_eq_one_right with *341342theorem mul_eq_one_iff_eq_inv (a b : G)343  shows a * b = G.one ↔ a = b⁻¹344proof345  constructor346  . intro equal347    exact eq_inv_of_mul_eq_one_left with *348  . intro equal349    rw [equal, Group.inv_mul]350    rfl351352theorem mul_eq_one_iff_inv_eq (a b : G)353  shows a * b = G.one ↔ a⁻¹ = b354proof355  constructor356  . intro equal357    exact inv_eq_of_mul_eq_one_right with *358  . intro equal359    rw [← equal, Group.mul_inv]360    rfl361362theorem inv_mul_eq_one (a b : G)363  shows a⁻¹ * b = G.one ↔ a = b364proof365  have criterion : a⁻¹ * b = G.one ↔ (a⁻¹)⁻¹ = b := mul_eq_one_iff_inv_eq with *366  rwa inv_inv at criterion367368theorem mul_inv_eq_one (a b : G)369  shows a * b⁻¹ = G.one ↔ a = b370proof371  have criterion : a * b⁻¹ = G.one ↔ a = (b⁻¹)⁻¹ := mul_eq_one_iff_eq_inv with *372  rwa inv_inv at criterion373374theorem inv_inj (a b : G)375  shows a⁻¹ = b⁻¹ ↔ a = b376proof377  constructor378  . intro equal379    have twiceA : (a⁻¹)⁻¹ = a := inv_inv with *380    have twiceB : (b⁻¹)⁻¹ = b := inv_inv with *381    cc382  . intro equal383    rw equal384    rfl385386theorem inv_eq_one (a : G)387  shows a⁻¹ = G.one ↔ a = G.one388proof389  have criterion : a⁻¹ = G.one⁻¹ ↔ a = G.one := inv_inj with *390  rwa inv_one at criterion391392theorem mul_self_eq_self (a : G)393  shows a * a = a ↔ a = G.one394proof395  constructor396  . intro idempotent397    calc398      a = a⁻¹ * (a * a) := by rw inv_mul_cancel_left399      _ = G.one := by rw [idempotent, Group.inv_mul]400  . intro equal401    rw [equal, one_mul]402    rfl403404theorem mul_inv_eq_iff_eq_mul (a b c : G)405  shows a * b⁻¹ = c ↔ a = c * b406proof407  constructor408  . intro equal409    rw [← equal, inv_mul_cancel_right]410    rfl411  . intro equal412    rw [equal, mul_inv_cancel_right]413    rfl414415theorem eq_inv_mul_iff_mul_eq (a b c : G)416  shows a = b⁻¹ * c ↔ b * a = c417proof418  constructor419  . intro equal420    rw [equal, mul_inv_cancel_left]421    rfl422  . intro equal423    rw [← equal, inv_mul_cancel_left]424    rfl425426theorem inv_mul_eq_iff_eq_mul (a b c : G)427  shows a⁻¹ * b = c ↔ b = a * c428proof429  constructor430  . intro equal431    rw [← equal, mul_inv_cancel_left]432    rfl433  . intro equal434    rw [equal, inv_mul_cancel_left]435    rfl436437theorem eq_mul_inv_iff_mul_eq (a b c : G)438  shows a = b * c⁻¹ ↔ a * c = b439proof440  constructor441  . intro equal442    rw [equal, inv_mul_cancel_right]443    rfl444  . intro equal445    rw [← equal, mul_inv_cancel_right]446    rfl447448end GroupLaws449450-- The group rewrite set: associativity to the right, the unit and inverse451-- cancellations, each applied where its operands are in the carrier.452tactic group_simp := simp [mul_assoc, one_mul, mul_one, Group.inv_mul, Group.mul_inv, inv_inv, inv_one, mul_inv_rev, inv_mul_cancel_left, mul_inv_cancel_left, mul_inv_cancel_right, inv_mul_cancel_right]453454section AbelianLaws455variable (G : Set)456hypothesis abelian : AbelianGroup(G)457458theorem mul_comm (a b : G)459  shows a * b = b * a460proof461  have commutative := IsAbelianGroup.commutative with (AbelianGroup.parts with abelian)462  exact Commutative.law with commutative, *463464theorem mul_left_comm (a b c : G)465  shows a * (b * c) = b * (a * c)466proof467  have group := AbelianGroup.to_group with abelian468  have swap : a * b = b * a := mul_comm with *469  rw [← mul_assoc, swap, mul_assoc]470  rfl471472theorem mul_right_comm (a b c : G)473  shows a * b * c = a * c * b474proof475  have group := AbelianGroup.to_group with abelian476  have swap : b * c = c * b := mul_comm with *477  rw [mul_assoc, swap, ← mul_assoc]478  rfl479480theorem mul_mul_mul_comm (a b c d : G)481  shows a * b * (c * d) = a * c * (b * d)482proof483  have group := AbelianGroup.to_group with abelian484  have swap : b * (c * d) = c * (b * d) := mul_left_comm with *485  rw [mul_assoc, swap, ← mul_assoc]486  rfl487488theorem mul_inv (a b : G)489  shows (a * b)⁻¹ = a⁻¹ * b⁻¹490proof491  have group := AbelianGroup.to_group with abelian492  have swap : b⁻¹ * a⁻¹ = a⁻¹ * b⁻¹ := mul_comm with *493  rw [mul_inv_rev, swap]494  rfl495496end AbelianLaws497