Grace/Cumulus/Algebra/Group/Core.g17

Open in Workbench Download source

Imports

Defs · Set.Function

Declarations

Source

1-- Core group theory2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Group.Core8import Defs9import Set.Function1011theorem IsMagma.closed (A op x y : Set)12  requires magma : IsMagma(A, op)13  requires xInA : x ∈ A14  requires yInA : y ∈ A15  shows op(x, y) ∈ A16proof17  unfold IsMagma at magma18  unfold call219  apply FunctionBetween.apply_closed with magma20  exact product.pair with xInA, yInA2122theorem IsSemigroup.magma (A op : Set)23  requires h : IsSemigroup(A, op)24  shows IsMagma(A, op)25proof26  simp [IsSemigroup]2728theorem IsSemigroup.associative (A op : Set)29  requires h : IsSemigroup(A, op)30  shows Associative(A, op)31proof32  simp [IsSemigroup]3334theorem IsSemigroup.closed (A op x y : Set)35  requires semigroup : IsSemigroup(A, op)36  requires xInA : x ∈ A37  requires yInA : y ∈ A38  shows op(x, y) ∈ A39proof40  have magma := IsSemigroup.magma with semigroup41  exact IsMagma.closed with magma, xInA, yInA4243theorem Associative.law (A op x y z : Set)44  requires associative : Associative(A, op)45  requires xInA : x ∈ A46  requires yInA : y ∈ A47  requires zInA : z ∈ A48  shows op(op(x, y), z) =49    op(x, op(y, z))50proof51  exact associative with x, xInA, y, yInA, z, zInA5253theorem Commutative.law (A op x y : Set)54  requires commutative : Commutative(A, op)55  requires xInA : x ∈ A56  requires yInA : y ∈ A57  shows op(x, y) = op(y, x)58proof59  exact commutative with x, xInA, y, yInA6061theorem IsMonoid.identity (A op unit : Set)62  requires h : IsMonoid(A, op, unit)63  shows Identity(A, op, unit)64proof65  simp [IsMonoid]6667theorem IsMonoid.closed (A op unit x y : Set)68  requires monoid : IsMonoid(A, op, unit)69  requires xInA : x ∈ A70  requires yInA : y ∈ A71  shows op(x, y) ∈ A72proof73  have semigroup := IsMonoid.semigroup with monoid74  exact IsSemigroup.closed with semigroup, xInA, yInA7576theorem IsMonoid.associative (A op unit : Set)77  requires monoid : IsMonoid(A, op, unit)78  shows Associative(A, op)79proof80  have semigroup := IsMonoid.semigroup with monoid81  exact IsSemigroup.associative with semigroup8283theorem IsMonoid.unit_in_carrier (A op unit : Set)84  requires monoid : IsMonoid(A, op, unit)85  shows unit ∈ A86proof87  obtain ⟨unitInA, laws⟩ := IsMonoid.identity with monoid88  exact unitInA8990theorem IsMonoid.left_identity (A op unit x : Set)91  requires monoid : IsMonoid(A, op, unit)92  requires xInA : x ∈ A93  shows op(unit, x) = x94proof95  obtain ⟨unitInA, laws⟩ := IsMonoid.identity with monoid96  obtain ⟨left, right⟩ := laws with x, xInA97  exact left9899theorem IsMonoid.right_identity (A op unit x : Set)100  requires monoid : IsMonoid(A, op, unit)101  requires xInA : x ∈ A102  shows op(x, unit) = x103proof104  obtain ⟨unitInA, laws⟩ := IsMonoid.identity with monoid105  obtain ⟨left, right⟩ := laws with x, xInA106  exact right107108theorem IsCommMonoid.monoid (A op unit : Set)109  requires h : IsCommMonoid(A, op, unit)110  shows IsMonoid(A, op, unit)111proof112  simp [IsCommMonoid]113114theorem IsCommMonoid.commutative (A op unit : Set)115  requires h : IsCommMonoid(A, op, unit)116  shows Commutative(A, op)117proof118  simp [IsCommMonoid]119120theorem IsGroup.magma (A op unit inv : Set)121  requires group : IsGroup(A, op, unit, inv)122  shows IsMagma(A, op)123proof124  have monoid := IsGroup.monoid with group125  have semigroup := IsMonoid.semigroup with monoid126  exact IsSemigroup.magma with semigroup127128theorem IsGroup.inverse (A op unit inv : Set)129  requires h : IsGroup(A, op, unit, inv)130  shows Inverse(A, op, unit, inv)131proof132  simp [IsGroup]133134theorem IsGroup.inverse_closed (A op unit inv x : Set)135  requires group : IsGroup(A, op, unit, inv)136  requires xInA : x ∈ A137  shows inv(x) ∈ A138proof139  obtain ⟨function, laws⟩ := IsGroup.inverse with group140  exact FunctionBetween.apply_closed with function, xInA141142theorem IsGroup.inverse_left (A op unit inv x : Set)143  requires group : IsGroup(A, op, unit, inv)144  requires xInA : x ∈ A145  shows op(inv(x), x) = unit146proof147  obtain ⟨function, laws⟩ := IsGroup.inverse with group148  obtain ⟨left, right⟩ := laws with x, xInA149  exact left150151theorem IsGroup.inverse_right (A op unit inv x : Set)152  requires group : IsGroup(A, op, unit, inv)153  requires xInA : x ∈ A154  shows op(x, inv(x)) = unit155proof156  obtain ⟨function, laws⟩ := IsGroup.inverse with group157  obtain ⟨left, right⟩ := laws with x, xInA158  exact right159160theorem IsAbelianGroup.group (A op unit inv : Set)161  requires h : IsAbelianGroup(A, op, unit, inv)162  shows IsGroup(A, op, unit, inv)163proof164  simp [IsAbelianGroup]165166theorem IsAbelianGroup.commutative (A op unit inv : Set)167  requires h : IsAbelianGroup(A, op, unit, inv)168  shows Commutative(A, op)169proof170  simp [IsAbelianGroup]171172theorem Identity.in_carrier (A op unit : Set)173  requires h : Identity(A, op, unit)174  shows unit ∈ A175proof176  simp [Identity]177178theorem Identity.unique (A op e f : Set)179  requires he : Identity(A, op, e)180  requires hf : Identity(A, op, f)181  shows e = f182proof183  rcases he with ⟨heA, heLaws⟩184  rcases hf with ⟨hfA, hfLaws⟩185  specialize heLaws with f, hfA186  rcases heLaws with ⟨hef, hfe⟩187  specialize hfLaws with e, heA188  rcases hfLaws with ⟨hfe2, hef2⟩189  rwa ← hef2190191theorem IsInverse.unique (A op unit a b c : Set)192  requires monoid : IsMonoid(A, op, unit)193  requires hb : IsInverse(A, op, unit, a, b)194  requires hc : IsInverse(A, op, unit, a, c)195  shows b = c196proof197  have monoidStructure := monoid198  rcases monoid with ⟨semigroup, identity⟩199  rcases semigroup with ⟨magma, associative⟩200  rcases identity with ⟨unitA, identityLaws⟩201  rcases hb with ⟨aA, bA, hba, hab⟩202  rcases hc with ⟨aA2, cA, hca, hac⟩203  specialize identityLaws with b, bA204  rcases identityLaws with ⟨unitB, bUnit⟩205  obtain ⟨unitA2, identityLawsC⟩ := IsMonoid.identity with monoidStructure206  specialize identityLawsC with c, cA207  rcases identityLawsC with ⟨unitC, cUnit⟩208  specialize associative with b, bA, a, aA, c, cA209  rewrite ← bUnit210  rewrite ← hac211  rewrite ← associative212  rwa hba213214theorem IsGroup.inverse_unit (A op unit inv : Set)215  requires group : IsGroup(A, op, unit, inv)216  shows inv(unit) = unit217proof218  have monoid := IsGroup.monoid with group219  have unitInA := IsMonoid.unit_in_carrier with monoid220  have inverseUnitInA := IsGroup.inverse_closed with group, unitInA221  have inverseEquation := IsGroup.inverse_left with group, unitInA222  have unitEquation := IsMonoid.right_identity with monoid, inverseUnitInA223  rwa unitEquation at inverseEquation224225theorem IsGroup.inverse_involutive (A op unit inv x : Set)226  requires group : IsGroup(A, op, unit, inv)227  requires xInA : x ∈ A228  shows inv(inv(x)) = x229proof230  have monoid := IsGroup.monoid with group231  have inverseXInA := IsGroup.inverse_closed with group, xInA232  have inverseInverseXInA := IsGroup.inverse_closed with group, inverseXInA233  have inverseLeft := IsGroup.inverse_left with group, xInA234  have inverseRight := IsGroup.inverse_right with group, xInA235  have twiceLeft := IsGroup.inverse_left with group, inverseXInA236  have twiceRight := IsGroup.inverse_right with group, inverseXInA237  have first : IsInverse(A, op, unit, inv(x), x)238    unfold IsInverse239    refine ⟨inverseXInA, xInA, inverseRight, inverseLeft⟩240  have second : IsInverse(A, op, unit,241      inv(x), inv(inv(x)))242    unfold IsInverse243    refine ⟨inverseXInA, inverseInverseXInA, twiceLeft, twiceRight⟩244  have unique := IsInverse.unique with monoid, first, second245  cc246247theorem IsAbelianGroup.four_shuffle (A op unit inv a b c d : Set)248  requires group : IsAbelianGroup(A, op, unit, inv)249  requires aInA : a ∈ A250  requires bInA : b ∈ A251  requires cInA : c ∈ A252  requires dInA : d ∈ A253  shows op(op(a, b), op(c, d)) =254    op(op(a, c), op(b, d))255proof256  have ordinary := IsAbelianGroup.group with group257  have monoid := IsGroup.monoid with ordinary258  have associative := IsMonoid.associative with monoid259  have commutative := IsAbelianGroup.commutative with group260  have cdInA := IsMonoid.closed with monoid, cInA, dInA261  have bdInA := IsMonoid.closed with monoid, bInA, dInA262  have outerLeft := Associative.law with associative, aInA, bInA, cdInA263  have middleLeft := Associative.law with associative, bInA, cInA, dInA264  have swap := commutative with b, bInA, c, cInA265  have middleRight := Associative.law with associative, cInA, bInA, dInA266  have outerRight := Associative.law with associative, aInA, cInA, bdInA267  cc268269theorem IsAbelianGroup.inverse_op (A op unit inv x y : Set)270  requires group : IsAbelianGroup(A, op, unit, inv)271  requires xInA : x ∈ A272  requires yInA : y ∈ A273  shows inv(op(x, y)) =274    op(inv(x), inv(y))275proof276  have ordinary := IsAbelianGroup.group with group277  have monoid := IsGroup.monoid with ordinary278  have inverseXInA := IsGroup.inverse_closed with ordinary, xInA279  have inverseYInA := IsGroup.inverse_closed with ordinary, yInA280  have xyInA := IsMonoid.closed with monoid, xInA, yInA281  have inverseXYInA := IsGroup.inverse_closed with ordinary, xyInA282  have candidateInA := IsMonoid.closed with monoid, inverseXInA, inverseYInA283  have shuffle := IsAbelianGroup.four_shuffle with group, inverseXInA, inverseYInA, xInA, yInA284  have inverseX := IsGroup.inverse_left with ordinary, xInA285  have inverseY := IsGroup.inverse_left with ordinary, yInA286  have unitInA := IsMonoid.unit_in_carrier with monoid287  have unitUnit := IsMonoid.left_identity with monoid, unitInA288  have candidateLeft : call2(op,289      op(inv(x), inv(y)), op(x, y)) = unit290    rwa [shuffle, inverseX, inverseY]291  have commutative := IsAbelianGroup.commutative with group292  have candidateSwap := commutative with293    op(inv(x), inv(y)), candidateInA,294    op(x, y), xyInA295  have candidateRight : call2(op, call2(op, x, y),296      op(inv(x), inv(y))) = unit297    rwa ← candidateSwap298  have canonical : IsInverse(A, op, unit,299      op(x, y), inv(op(x, y)))300    unfold IsInverse301    refine ⟨xyInA, inverseXYInA, _, _⟩302    . exact IsGroup.inverse_left at303        A, op, unit, inv, op(x, y) with ordinary, xyInA304    . exact IsGroup.inverse_right at305        A, op, unit, inv, op(x, y) with ordinary, xyInA306  have candidate : IsInverse(A, op, unit,307      op(x, y), op(inv(x), inv(y)))308    unfold IsInverse309    refine ⟨xyInA, candidateInA, candidateLeft, candidateRight⟩310  exact IsInverse.unique with monoid, canonical, candidate311312-- The inverse of a product reverses the factors.313theorem IsGroup.inverse_op (A op unit inv a b : Set)314  requires group : IsGroup(A, op, unit, inv)315  requires ha : a ∈ A316  requires hb : b ∈ A317  shows inv(op(a, b)) = op(inv(b), inv(a))318proof319  have monoid := group.left320  have associative := IsMonoid.associative with monoid321  have product := IsMonoid.closed with monoid, ha, hb322  have invA := IsGroup.inverse_closed with group, ha323  have invB := IsGroup.inverse_closed with group, hb324  have invProduct := IsGroup.inverse_closed with group, product325  have candidate := IsMonoid.closed with monoid, invB, invA326  have leftInverse := IsGroup.inverse_left with group, product327  have rearranged : op(op(inv(b), inv(a)), op(a, b)) = unit328    have step1 := Associative.law with associative, candidate, ha, hb329    have step2 := Associative.law with associative, invB, invA, ha330    have cancelA := IsGroup.inverse_left with group, ha331    have unitRight := IsMonoid.right_identity with monoid, invB332    have cancelB := IsGroup.inverse_left with group, hb333    rwa [← step1, step2, cancelA, unitRight]334  have equalProducts : op(inv(op(a, b)), op(a, b)) = op(op(inv(b), inv(a)), op(a, b))335    rw [leftInverse, rearranged]336    rfl337  have rightCancel : ∀ x ∈ A, ∀ y ∈ A, op(x, op(a, b)) = op(y, op(a, b)) → x = y338    intros x hx y hy equal339    have invProductIn := IsGroup.inverse_closed with group, product340    have cancelX : op(op(x, op(a, b)), inv(op(a, b))) = x341      have assoc := Associative.law with associative, hx, product, invProductIn342      have right := IsGroup.inverse_right with group, product343      have identity := IsMonoid.right_identity with monoid, hx344      rwa [assoc, right]345    have cancelY : op(op(y, op(a, b)), inv(op(a, b))) = y346      have assoc := Associative.law with associative, hy, product, invProductIn347      have right := IsGroup.inverse_right with group, product348      have identity := IsMonoid.right_identity with monoid, hy349      rwa [assoc, right]350    rw [equal, cancelY] at cancelX351    symm at cancelX352    exact cancelX353  have forX := rightCancel with invProduct354  have forXY := forX with candidate355  exact forXY with equalProducts356