Skip to content

Commit 3b9f62b

Browse files
jamesmckinnajamesmckinna
authored
[ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} with knock-ons for Algebra.Module.* (#2571)
* deprecate: `uniqueˡ-⁻¹` and `uniqueʳ-⁻¹` * refactor: simplify imports * refactor: simplify imports * refactor: export of uniqueness proofs * tweak: remove parentheses * tweak: `import` refinements * tweak: whitespace/alignment * fix: semicolon * refactor: corresponding changes for `Module`s, plus new `module`s to support them * refactor: fix re-exports from `Algebra.Module.Properties` * fix: `CHANGELOG` * fix: names of lemmas, and their types! * fix: whitespace! * fix: names, types, and exports
1 parent 4d6129a commit 3b9f62b

10 files changed

+132
-13
lines changed

‎CHANGELOG.md

+26
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,18 @@ Deprecated names
5757
*ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
5858
```
5959

60+
* In `Algebra.Modules.Structures.IsLeftModule`:
61+
```agda
62+
uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ
63+
uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ
64+
```
65+
66+
* In `Algebra.Modules.Structures.IsRightModule`:
67+
```agda
68+
uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ
69+
uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ
70+
```
71+
6072
* In `Algebra.Properties.Magma.Divisibility`:
6173
```agda
6274
∣∣-sym ↦ ∥-sym
@@ -92,6 +104,12 @@ Deprecated names
92104
∣-trans ↦ ∣ʳ-trans
93105
```
94106

107+
* In `Algebra.Structures.Group`:
108+
```agda
109+
uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique
110+
uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique
111+
```
112+
95113
* In `Data.List.Base`:
96114
```agda
97115
and ↦ Data.Bool.ListAction.and
@@ -119,6 +137,8 @@ Deprecated names
119137
New modules
120138
-----------
121139

140+
* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`.
141+
122142
* `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
123143

124144
* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
@@ -161,6 +181,12 @@ Additions to existing modules
161181
commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
162182
```
163183

184+
* In `Algebra.Modules.Properties`:
185+
```agda
186+
inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y
187+
inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x
188+
```
189+
164190
* In `Algebra.Properties.Magma.Divisibility`:
165191
```agda
166192
∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_

‎src/Algebra/Module/Bundles.agda

-1
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,6 @@ open import Algebra.Module.Definitions
3939
open import Function.Base using (flip)
4040
open import Level using (Level; _⊔_; suc)
4141
open import Relation.Binary.Core using (Rel)
42-
open import Relation.Nullary using (¬_)
4342
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
4443

4544
private

‎src/Algebra/Module/Properties.agda

+3-5
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra using (CommutativeRing; Involutive)
9+
open import Algebra.Bundles using (CommutativeRing)
1010
open import Algebra.Module.Bundles using (Module)
1111
open import Level using (Level)
1212

@@ -18,7 +18,5 @@ module Algebra.Module.Properties
1818

1919
open Module mod
2020
open import Algebra.Module.Properties.Semimodule semimodule public
21-
open import Algebra.Properties.Group using (⁻¹-involutive)
22-
23-
-ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_
24-
-ᴹ-involutive = ⁻¹-involutive +ᴹ-group
21+
open import Algebra.Module.Properties.Bimodule bimodule public
22+
using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ; -ᴹ-involutive)

‎src/Algebra/Module/Properties/Bimodule.agda

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of bimodules.
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Algebra.Bundles using (Ring)
10+
open import Algebra.Module.Bundles using (Bimodule)
11+
open import Level using (Level)
12+
13+
module Algebra.Module.Properties.Bimodule
14+
{r ℓr s ℓs m ℓm : Level}
15+
{ringR : Ring r ℓr} {ringS : Ring s ℓs}
16+
(mod : Bimodule ringR ringS m ℓm)
17+
where
18+
19+
open Bimodule mod
20+
open import Algebra.Module.Properties.LeftModule leftModule public
21+
using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ; -ᴹ-involutive)

‎src/Algebra/Module/Properties/LeftModule.agda

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of left modules.
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Algebra.Bundles using (Ring)
10+
open import Algebra.Module.Bundles using (LeftModule)
11+
open import Level using (Level)
12+
13+
module Algebra.Module.Properties.LeftModule
14+
{r ℓr m ℓm : Level}
15+
{ring : Ring r ℓr}
16+
(mod : LeftModule ring m ℓm)
17+
where
18+
19+
open Ring ring
20+
open LeftModule mod
21+
open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
22+
using ()
23+
renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
24+
; inverseʳ-unique to inverseʳ-uniqueᴹ
25+
; ⁻¹-involutive to -ᴹ-involutive)

‎src/Algebra/Module/Properties/RightModule.agda

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of right modules.
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Algebra.Bundles using (Ring)
10+
open import Algebra.Module.Bundles using (RightModule)
11+
open import Level using (Level)
12+
13+
module Algebra.Module.Properties.RightModule
14+
{r ℓr m ℓm : Level}
15+
{ring : Ring r ℓr}
16+
(mod : RightModule ring m ℓm)
17+
where
18+
19+
open Ring ring
20+
open RightModule mod
21+
open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
22+
using ()
23+
renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
24+
; inverseʳ-unique to inverseʳ-uniqueᴹ
25+
; ⁻¹-involutive to -ᴹ-involutive)

‎src/Algebra/Module/Properties/Semimodule.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra using (CommutativeSemiring)
9+
open import Algebra.Bundles using (CommutativeSemiring)
1010
open import Algebra.Module.Bundles using (Semimodule)
1111
open import Level using (Level)
1212

@@ -18,8 +18,8 @@ module Algebra.Module.Properties.Semimodule
1818

1919
open CommutativeSemiring semiring
2020
open Semimodule semimod
21-
open import Relation.Nullary.Negation using (contraposition)
2221
open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid
22+
open import Relation.Nullary.Negation using (contraposition)
2323

2424
x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ
2525
x≈0⇒x*y≈0 {x} {y} x≈0 = begin

‎src/Algebra/Module/Structures.agda

+22-4
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,6 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Relation.Binary.Core using (Rel)
10-
open import Relation.Binary.Bundles using (Setoid)
11-
open import Relation.Binary.Structures using (IsEquivalence)
12-
139
module Algebra.Module.Structures where
1410

1511
open import Algebra.Bundles
@@ -23,6 +19,10 @@ open import Algebra.Module.Definitions
2319
open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup)
2420
open import Data.Product.Base using (_,_; proj₁; proj₂)
2521
open import Level using (Level; _⊔_)
22+
open import Relation.Binary.Core using (Rel)
23+
open import Relation.Binary.Bundles using (Setoid)
24+
open import Relation.Binary.Structures using (IsEquivalence)
25+
2626

2727
private
2828
variable
@@ -216,6 +216,15 @@ module _ (ring : Ring r ℓr)
216216
; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
217217
; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
218218
)
219+
{-# WARNING_ON_USAGE uniqueˡ‿-ᴹ
220+
"Warning: uniqueˡ‿-ᴹ was deprecated in v2.3.
221+
Please use Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ instead."
222+
#-}
223+
{-# WARNING_ON_USAGE uniqueʳ‿-ᴹ
224+
"Warning: uniqueʳ‿-ᴹ was deprecated in v2.3.
225+
Please use Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ instead."
226+
#-}
227+
219228

220229
record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
221230
open Defs ≈ᴹ
@@ -244,6 +253,15 @@ module _ (ring : Ring r ℓr)
244253
; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
245254
; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
246255
)
256+
{-# WARNING_ON_USAGE uniqueˡ‿-ᴹ
257+
"Warning: uniqueˡ‿-ᴹ was deprecated in v2.3.
258+
Please use Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ instead."
259+
#-}
260+
{-# WARNING_ON_USAGE uniqueʳ‿-ᴹ
261+
"Warning: uniqueʳ‿-ᴹ was deprecated in v2.3.
262+
Please use Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ instead."
263+
#-}
264+
247265

248266
module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs)
249267
(≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)

‎src/Algebra/Morphism.agda

-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ module Algebra.Morphism where
1010

1111
import Algebra.Morphism.Definitions as MorphismDefinitions
1212
open import Algebra
13-
import Algebra.Properties.Group as GroupP
1413
open import Function.Base
1514
open import Level
1615
open import Relation.Binary.Core using (Rel; _Preserves_⟶_)

‎src/Algebra/Structures.agda

+8
Original file line numberDiff line numberDiff line change
@@ -323,10 +323,18 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w
323323
uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹)
324324
uniqueˡ-⁻¹ = Consequences.assoc∧id∧invʳ⇒invˡ-unique
325325
setoid ∙-cong assoc identity inverseʳ
326+
{-# WARNING_ON_USAGE uniqueˡ-⁻¹
327+
"Warning: uniqueˡ-⁻¹ was deprecated in v2.3.
328+
Please use Algebra.Properties.Group.inverseˡ-unique instead. "
329+
#-}
326330

327331
uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹)
328332
uniqueʳ-⁻¹ = Consequences.assoc∧id∧invˡ⇒invʳ-unique
329333
setoid ∙-cong assoc identity inverseˡ
334+
{-# WARNING_ON_USAGE uniqueʳ-⁻¹
335+
"Warning: uniqueʳ-⁻¹ was deprecated in v2.3.
336+
Please use Algebra.Properties.Group.inverseʳ-unique instead. "
337+
#-}
330338

331339
isInvertibleMagma : IsInvertibleMagma _∙_ ε _⁻¹
332340
isInvertibleMagma = record

0 commit comments

Comments
 (0)