From 3a60b0bafd8b058df32d67ed440eaade196abd4c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 3 Feb 2025 11:54:52 +0000 Subject: [PATCH 01/14] =?UTF-8?q?deprecate:=20`unique=CB=A1-=E2=81=BB?= =?UTF-8?q?=C2=B9`=20and=20`unique=CA=B3-=E2=81=BB=C2=B9`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 6 ++++++ src/Algebra/Structures.agda | 8 ++++++++ 2 files changed, 14 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index f16ed00b65..8727d4f68e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -51,6 +51,12 @@ Deprecated names ∣∣-trans ↦ ∥-trans ``` +* In `Algebra.Structures`: + ```agda + uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique + uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique + ``` + New modules ----------- diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 1aae80d1cc..b15bad236f 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -323,10 +323,18 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹) uniqueˡ-⁻¹ = Consequences.assoc∧id∧invʳ⇒invˡ-unique setoid ∙-cong assoc identity inverseʳ + {-# WARNING_ON_USAGE uniqueˡ-⁻¹ + "Warning: uniqueˡ-⁻¹ was deprecated in v2.3. + Please use Algebra.Properties.Group.inverseˡ-unique instead. " + #-} uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹) uniqueʳ-⁻¹ = Consequences.assoc∧id∧invˡ⇒invʳ-unique setoid ∙-cong assoc identity inverseˡ + {-# WARNING_ON_USAGE uniqueʳ-⁻¹ + "Warning: uniqueʳ-⁻¹ was deprecated in v2.3. + Please use Algebra.Properties.Group.inverseʳ-unique instead. " + #-} isInvertibleMagma : IsInvertibleMagma _∙_ ε _⁻¹ isInvertibleMagma = record From 29b97aff8d9dd111ce2d099efef7ee1d35b535a4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 3 Feb 2025 11:55:38 +0000 Subject: [PATCH 02/14] refactor: simplify imports --- src/Algebra/Module/Bundles.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index 5df96258d6..08bb03256d 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/src/Algebra/Module/Bundles.agda @@ -32,11 +32,9 @@ import Algebra.Module.Bundles.Raw as Raw open import Algebra.Module.Core open import Algebra.Module.Structures open import Algebra.Module.Definitions -open import Algebra.Properties.Group open import Function.Base open import Level open import Relation.Binary.Core using (Rel) -open import Relation.Nullary using (¬_) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning private From dfc0baa1b6663f4f1d38389e2fb663a7d0ad6506 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 3 Feb 2025 12:44:52 +0000 Subject: [PATCH 03/14] refactor: simplify imports --- src/Algebra/Morphism.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda index e3bcb53e9b..555398fdde 100644 --- a/src/Algebra/Morphism.agda +++ b/src/Algebra/Morphism.agda @@ -10,7 +10,6 @@ module Algebra.Morphism where import Algebra.Morphism.Definitions as MorphismDefinitions open import Algebra -import Algebra.Properties.Group as GroupP open import Function.Base open import Level open import Relation.Binary.Core using (Rel; _Preserves_⟶_) From bd2bd16f21425f16364d67b9be6dba5775b8496e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 3 Feb 2025 12:45:38 +0000 Subject: [PATCH 04/14] refactor: export of uniqueness proofs --- src/Algebra/Module/Structures.agda | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 64873252bd..87f5eecad0 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -17,6 +17,7 @@ open import Algebra.Core open import Algebra.Module.Core import Algebra.Definitions as Defs open import Algebra.Module.Definitions +import Algebra.Properties.AbelianGroup as AbelianGroupProperties open import Algebra.Structures open import Data.Product.Base using (_,_; proj₁; proj₂) open import Level using (Level; _⊔_) @@ -210,10 +211,12 @@ module _ (ring : Ring r ℓr) ( isGroup to +ᴹ-isGroup ; inverseˡ to -ᴹ‿inverseˡ ; inverseʳ to -ᴹ‿inverseʳ - ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ - ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ ) + open AbelianGroupProperties (record { isAbelianGroup = +ᴹ-isAbelianGroup }) public + using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ) + + record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where open Defs ≈ᴹ field @@ -238,10 +241,12 @@ module _ (ring : Ring r ℓr) ( isGroup to +ᴹ-isGroup ; inverseˡ to -ᴹ‿inverseˡ ; inverseʳ to -ᴹ‿inverseʳ - ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ - ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ ) + open AbelianGroupProperties (record { isAbelianGroup = +ᴹ-isAbelianGroup }) public + using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ) + + module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M) where From 1a71b8cbfd56653515fbeb216b3016406a3d8aa3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 4 Feb 2025 08:44:03 +0000 Subject: [PATCH 05/14] tweak: remove parentheses --- src/Algebra/Module/Structures.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 87f5eecad0..0373b32700 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -213,7 +213,7 @@ module _ (ring : Ring r ℓr) ; inverseʳ to -ᴹ‿inverseʳ ) - open AbelianGroupProperties (record { isAbelianGroup = +ᴹ-isAbelianGroup }) public + open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ) @@ -243,7 +243,7 @@ module _ (ring : Ring r ℓr) ; inverseʳ to -ᴹ‿inverseʳ ) - open AbelianGroupProperties (record { isAbelianGroup = +ᴹ-isAbelianGroup }) public + open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ) From 605a1ccabf001d6ee2501c3ba51e45474c77bbcd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 25 Mar 2025 08:04:22 +0000 Subject: [PATCH 06/14] tweak: `import` refinements --- src/Algebra/Module/Properties.agda | 9 +++++---- src/Algebra/Module/Properties/Semimodule.agda | 4 ++-- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda index 28f61b50bc..bc0ea3b3ac 100644 --- a/src/Algebra/Module/Properties.agda +++ b/src/Algebra/Module/Properties.agda @@ -6,19 +6,20 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra using (CommutativeRing; Involutive) +open import Algebra.Bundles using (CommutativeRing) open import Algebra.Module.Bundles using (Module) open import Level using (Level) module Algebra.Module.Properties {r ℓr m ℓm : Level} - {ring : CommutativeRing r ℓr} - (mod : Module ring m ℓm) + {ring : CommutativeRing r ℓr} + (mod : Module ring m ℓm) where open Module mod +open import Algebra.Definitions _≈ᴹ_ using (Involutive) open import Algebra.Module.Properties.Semimodule semimodule public open import Algebra.Properties.Group using (⁻¹-involutive) --ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_ +-ᴹ-involutive : Involutive -ᴹ_ -ᴹ-involutive = ⁻¹-involutive +ᴹ-group diff --git a/src/Algebra/Module/Properties/Semimodule.agda b/src/Algebra/Module/Properties/Semimodule.agda index f6db3680b4..d7686b25ef 100644 --- a/src/Algebra/Module/Properties/Semimodule.agda +++ b/src/Algebra/Module/Properties/Semimodule.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Algebra using (CommutativeSemiring) +open import Algebra.Bundles using (CommutativeSemiring) open import Algebra.Module.Bundles using (Semimodule) open import Level using (Level) @@ -18,8 +18,8 @@ module Algebra.Module.Properties.Semimodule open CommutativeSemiring semiring open Semimodule semimod -open import Relation.Nullary.Negation using (contraposition) open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid +open import Relation.Nullary.Negation using (contraposition) x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ x≈0⇒x*y≈0 {x} {y} x≈0 = begin From 796f1561a5c1f2b1745afa33b3107c505b9d11e2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 25 Mar 2025 17:56:52 +0000 Subject: [PATCH 07/14] tweak: whitespace/alignment --- src/Algebra/Module/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 59e71e01fc..e6995b4a40 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -19,7 +19,7 @@ open import Algebra.Module.Core using (Opₗ; Opᵣ) import Algebra.Definitions as Defs open import Algebra.Module.Definitions using (module LeftDefs; module RightDefs; module BiDefs; - module SimultaneousBiDefs) + ; module SimultaneousBiDefs) import Algebra.Properties.AbelianGroup as AbelianGroupProperties open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup) open import Data.Product.Base using (_,_; proj₁; proj₂) From d7e2b7a017f224c527caba2e87920cd1f7680d8c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 25 Mar 2025 18:03:43 +0000 Subject: [PATCH 08/14] fix: semicolon --- src/Algebra/Module/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index e6995b4a40..073400b1aa 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -18,7 +18,7 @@ open import Algebra.Core using (Op₁; Op₂) open import Algebra.Module.Core using (Opₗ; Opᵣ) import Algebra.Definitions as Defs open import Algebra.Module.Definitions - using (module LeftDefs; module RightDefs; module BiDefs; + using (module LeftDefs; module RightDefs; module BiDefs ; module SimultaneousBiDefs) import Algebra.Properties.AbelianGroup as AbelianGroupProperties open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup) From e12f94278055356a1aa747176410a4b1cf4bc54b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 26 Mar 2025 12:07:26 +0000 Subject: [PATCH 09/14] refactor: corresponding changes for `Module`s, plus new `module`s to support them --- CHANGELOG.md | 16 ++++++++- src/Algebra/Module/Properties/Bimodule.agda | 21 +++++++++++ src/Algebra/Module/Properties/LeftModule.agda | 24 +++++++++++++ .../Module/Properties/RightModule.agda | 24 +++++++++++++ src/Algebra/Module/Structures.agda | 35 +++++++++++++------ 5 files changed, 108 insertions(+), 12 deletions(-) create mode 100644 src/Algebra/Module/Properties/Bimodule.agda create mode 100644 src/Algebra/Module/Properties/LeftModule.agda create mode 100644 src/Algebra/Module/Properties/RightModule.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index a50d7bd272..1f983225f5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -51,6 +51,18 @@ Deprecated names *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc ``` +* In `Algebra.Modules.Structures.IsLeftModule`: + ```agda + uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ + uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ + ``` + +* In `Algebra.Modules.Structures.IsRightModule`: + ```agda + uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ + uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ + ``` + * In `Algebra.Properties.Magma.Divisibility`: ```agda ∣∣-sym ↦ ∥-sym @@ -86,7 +98,7 @@ Deprecated names ∣-trans ↦ ∣ʳ-trans ``` -* In `Algebra.Structures`: +* In `Algebra.Structures.Group`: ```agda uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique @@ -119,6 +131,8 @@ Deprecated names New modules ----------- +* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`. + * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. diff --git a/src/Algebra/Module/Properties/Bimodule.agda b/src/Algebra/Module/Properties/Bimodule.agda new file mode 100644 index 0000000000..18ca0209c6 --- /dev/null +++ b/src/Algebra/Module/Properties/Bimodule.agda @@ -0,0 +1,21 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of bimodules. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Ring) +open import Algebra.Module.Bundles using (Bimodule) +open import Level using (Level) + +module Algebra.Module.Properties.Bimodule + {r ℓr s ℓs m ℓm : Level} + {ringR : Ring r ℓr} {ringS : Ring s ℓs} + (mod : Bimodule ringR ringS m ℓm) + where + +open Bimodule mod +open import Algebra.Module.Properties.LeftModule leftModule public + using (identityˡ-uniqueᴹ; identityʳ-uniqueᴹ) diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda new file mode 100644 index 0000000000..4ab5deed04 --- /dev/null +++ b/src/Algebra/Module/Properties/LeftModule.agda @@ -0,0 +1,24 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of left modules. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Ring) +open import Algebra.Module.Bundles using (LeftModule) +open import Level using (Level) + +module Algebra.Module.Properties.LeftModule + {r ℓr m ℓm : Level} + {ring : Ring r ℓr} + (mod : LeftModule ring m ℓm) + where + +open Ring ring +open LeftModule mod +open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public + using () + renaming (identityˡ-unique to identityˡ-uniqueᴹ + ; identityʳ-unique to identityʳ-uniqueᴹ) diff --git a/src/Algebra/Module/Properties/RightModule.agda b/src/Algebra/Module/Properties/RightModule.agda new file mode 100644 index 0000000000..20252df80c --- /dev/null +++ b/src/Algebra/Module/Properties/RightModule.agda @@ -0,0 +1,24 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of right modules. +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles using (Ring) +open import Algebra.Module.Bundles using (RightModule) +open import Level using (Level) + +module Algebra.Module.Properties.RightModule + {r ℓr m ℓm : Level} + {ring : Ring r ℓr} + (mod : RightModule ring m ℓm) + where + +open Ring ring +open RightModule mod +open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public + using () + renaming (identityˡ-unique to identityˡ-uniqueᴹ + ; identityʳ-unique to identityʳ-uniqueᴹ) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 073400b1aa..0084b33d90 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -6,10 +6,6 @@ {-# OPTIONS --cubical-compatible --safe #-} -open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.Structures using (IsEquivalence) - module Algebra.Module.Structures where open import Algebra.Bundles @@ -20,10 +16,13 @@ import Algebra.Definitions as Defs open import Algebra.Module.Definitions using (module LeftDefs; module RightDefs; module BiDefs ; module SimultaneousBiDefs) -import Algebra.Properties.AbelianGroup as AbelianGroupProperties open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Level using (Level; _⊔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.Structures using (IsEquivalence) + private variable @@ -214,10 +213,17 @@ module _ (ring : Ring r ℓr) ( isGroup to +ᴹ-isGroup ; inverseˡ to -ᴹ‿inverseˡ ; inverseʳ to -ᴹ‿inverseʳ + ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ + ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ ) - - open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public - using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ) + {-# WARNING_ON_USAGE uniqueˡ‿-ᴹ + "Warning: uniqueˡ‿-ᴹ was deprecated in v2.3. + Please use Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ instead." + #-} + {-# WARNING_ON_USAGE uniqueʳ‿-ᴹ + "Warning: uniqueʳ‿-ᴹ was deprecated in v2.3. + Please use Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ instead." + #-} record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where @@ -244,10 +250,17 @@ module _ (ring : Ring r ℓr) ( isGroup to +ᴹ-isGroup ; inverseˡ to -ᴹ‿inverseˡ ; inverseʳ to -ᴹ‿inverseʳ + ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ + ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ ) - - open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public - using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ) + {-# WARNING_ON_USAGE uniqueˡ‿-ᴹ + "Warning: uniqueˡ‿-ᴹ was deprecated in v2.3. + Please use Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ instead." + #-} + {-# WARNING_ON_USAGE uniqueʳ‿-ᴹ + "Warning: uniqueʳ‿-ᴹ was deprecated in v2.3. + Please use Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ instead." + #-} module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) From 8e6c8e57a592784563c729dfb77579de6ff0de51 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 26 Mar 2025 13:11:49 +0000 Subject: [PATCH 10/14] refactor: fix re-exports from `Algebra.Module.Properties` --- src/Algebra/Module/Properties.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda index bc0ea3b3ac..c0e1c17ae4 100644 --- a/src/Algebra/Module/Properties.agda +++ b/src/Algebra/Module/Properties.agda @@ -12,14 +12,14 @@ open import Level using (Level) module Algebra.Module.Properties {r ℓr m ℓm : Level} - {ring : CommutativeRing r ℓr} - (mod : Module ring m ℓm) + {ring : CommutativeRing r ℓr} + (mod : Module ring m ℓm) where open Module mod -open import Algebra.Definitions _≈ᴹ_ using (Involutive) open import Algebra.Module.Properties.Semimodule semimodule public -open import Algebra.Properties.Group using (⁻¹-involutive) - --ᴹ-involutive : Involutive -ᴹ_ --ᴹ-involutive = ⁻¹-involutive +ᴹ-group +open import Algebra.Module.Properties.LeftModule leftModule public + using (identityˡ-uniqueᴹ; identityʳ-uniqueᴹ) +open import Algebra.Properties.Group +ᴹ-group public + using () + renaming (⁻¹-involutive to -ᴹ-involutive) From e67d1e9a5c3b13e7a2465b7bc1c8c8d2de3045d5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 27 Mar 2025 07:56:26 +0000 Subject: [PATCH 11/14] fix: `CHANGELOG` --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1f983225f5..8cec683c61 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -175,6 +175,12 @@ Additions to existing modules commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) ``` +* In `Algebra.Modules.Properties`: + ```agda + inverseˡ-uniqueᴹ : x +ᴹ y ≈ y → x ≈ 0ᴹ + inverseʳ-uniqueᴹ : x +ᴹ y ≈ x → y ≈ 0ᴹ + ``` + * In `Algebra.Properties.Magma.Divisibility`: ```agda ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ From f1bb2f1d16cb82e34ba4c8ef06f79c54d507b4d2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 27 Mar 2025 11:12:36 +0000 Subject: [PATCH 12/14] fix: names of lemmas, and their types! --- CHANGELOG.md | 4 ++-- src/Algebra/Module/Properties.agda | 2 +- src/Algebra/Module/Properties/LeftModule.agda | 4 ++-- src/Algebra/Module/Properties/RightModule.agda | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8cec683c61..fce644e3fd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -177,8 +177,8 @@ Additions to existing modules * In `Algebra.Modules.Properties`: ```agda - inverseˡ-uniqueᴹ : x +ᴹ y ≈ y → x ≈ 0ᴹ - inverseʳ-uniqueᴹ : x +ᴹ y ≈ x → y ≈ 0ᴹ + inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y + inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x ``` * In `Algebra.Properties.Magma.Divisibility`: diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda index c0e1c17ae4..beb1de7b83 100644 --- a/src/Algebra/Module/Properties.agda +++ b/src/Algebra/Module/Properties.agda @@ -19,7 +19,7 @@ module Algebra.Module.Properties open Module mod open import Algebra.Module.Properties.Semimodule semimodule public open import Algebra.Module.Properties.LeftModule leftModule public - using (identityˡ-uniqueᴹ; identityʳ-uniqueᴹ) + using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ) open import Algebra.Properties.Group +ᴹ-group public using () renaming (⁻¹-involutive to -ᴹ-involutive) diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda index 4ab5deed04..3e94658ea2 100644 --- a/src/Algebra/Module/Properties/LeftModule.agda +++ b/src/Algebra/Module/Properties/LeftModule.agda @@ -20,5 +20,5 @@ open Ring ring open LeftModule mod open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public using () - renaming (identityˡ-unique to identityˡ-uniqueᴹ - ; identityʳ-unique to identityʳ-uniqueᴹ) + renaming (inverseˡ-unique to inverseˡ-uniqueᴹ + ; inverseʳ-unique to inverseʳ-uniqueᴹ) diff --git a/src/Algebra/Module/Properties/RightModule.agda b/src/Algebra/Module/Properties/RightModule.agda index 20252df80c..4784c84d9a 100644 --- a/src/Algebra/Module/Properties/RightModule.agda +++ b/src/Algebra/Module/Properties/RightModule.agda @@ -20,5 +20,5 @@ open Ring ring open RightModule mod open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public using () - renaming (identityˡ-unique to identityˡ-uniqueᴹ - ; identityʳ-unique to identityʳ-uniqueᴹ) + renaming (inverseˡ-unique to inverseˡ-uniqueᴹ + ; inverseʳ-unique to inverseʳ-uniqueᴹ) From 116aea4d87548bbce1c8757729d0fd86ab729366 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 27 Mar 2025 11:17:49 +0000 Subject: [PATCH 13/14] fix: whitespace! --- src/Algebra/Module/Properties/Bimodule.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Properties/Bimodule.agda b/src/Algebra/Module/Properties/Bimodule.agda index 18ca0209c6..8330bb3d0e 100644 --- a/src/Algebra/Module/Properties/Bimodule.agda +++ b/src/Algebra/Module/Properties/Bimodule.agda @@ -12,7 +12,7 @@ open import Level using (Level) module Algebra.Module.Properties.Bimodule {r ℓr s ℓs m ℓm : Level} - {ringR : Ring r ℓr} {ringS : Ring s ℓs} + {ringR : Ring r ℓr} {ringS : Ring s ℓs} (mod : Bimodule ringR ringS m ℓm) where From b5a3fc87f6122f7794ad481315632efec9a23213 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 27 Mar 2025 11:25:35 +0000 Subject: [PATCH 14/14] fix: names, types, and exports --- src/Algebra/Module/Properties.agda | 7 ++----- src/Algebra/Module/Properties/Bimodule.agda | 2 +- src/Algebra/Module/Properties/LeftModule.agda | 3 ++- src/Algebra/Module/Properties/RightModule.agda | 3 ++- 4 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda index beb1de7b83..b9b529681f 100644 --- a/src/Algebra/Module/Properties.agda +++ b/src/Algebra/Module/Properties.agda @@ -18,8 +18,5 @@ module Algebra.Module.Properties open Module mod open import Algebra.Module.Properties.Semimodule semimodule public -open import Algebra.Module.Properties.LeftModule leftModule public - using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ) -open import Algebra.Properties.Group +ᴹ-group public - using () - renaming (⁻¹-involutive to -ᴹ-involutive) +open import Algebra.Module.Properties.Bimodule bimodule public + using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ; -ᴹ-involutive) diff --git a/src/Algebra/Module/Properties/Bimodule.agda b/src/Algebra/Module/Properties/Bimodule.agda index 8330bb3d0e..539759c1b6 100644 --- a/src/Algebra/Module/Properties/Bimodule.agda +++ b/src/Algebra/Module/Properties/Bimodule.agda @@ -18,4 +18,4 @@ module Algebra.Module.Properties.Bimodule open Bimodule mod open import Algebra.Module.Properties.LeftModule leftModule public - using (identityˡ-uniqueᴹ; identityʳ-uniqueᴹ) + using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ; -ᴹ-involutive) diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda index 3e94658ea2..ad6d33cc67 100644 --- a/src/Algebra/Module/Properties/LeftModule.agda +++ b/src/Algebra/Module/Properties/LeftModule.agda @@ -21,4 +21,5 @@ open LeftModule mod open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public using () renaming (inverseˡ-unique to inverseˡ-uniqueᴹ - ; inverseʳ-unique to inverseʳ-uniqueᴹ) + ; inverseʳ-unique to inverseʳ-uniqueᴹ + ; ⁻¹-involutive to -ᴹ-involutive) diff --git a/src/Algebra/Module/Properties/RightModule.agda b/src/Algebra/Module/Properties/RightModule.agda index 4784c84d9a..ef6b7c9f90 100644 --- a/src/Algebra/Module/Properties/RightModule.agda +++ b/src/Algebra/Module/Properties/RightModule.agda @@ -21,4 +21,5 @@ open RightModule mod open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public using () renaming (inverseˡ-unique to inverseˡ-uniqueᴹ - ; inverseʳ-unique to inverseʳ-uniqueᴹ) + ; inverseʳ-unique to inverseʳ-uniqueᴹ + ; ⁻¹-involutive to -ᴹ-involutive)