Skip to content

Commit e12f942

Browse files
jamesmckinnajamesmckinna
committed
refactor: corresponding changes for Modules, plus new modules to support them
1 parent d7e2b7a commit e12f942

File tree

5 files changed

+108
-12
lines changed

5 files changed

+108
-12
lines changed

‎CHANGELOG.md

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,18 @@ Deprecated names
5151
*ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
5252
```
5353

54+
* In `Algebra.Modules.Structures.IsLeftModule`:
55+
```agda
56+
uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ
57+
uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ
58+
```
59+
60+
* In `Algebra.Modules.Structures.IsRightModule`:
61+
```agda
62+
uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ
63+
uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ
64+
```
65+
5466
* In `Algebra.Properties.Magma.Divisibility`:
5567
```agda
5668
∣∣-sym ↦ ∥-sym
@@ -86,7 +98,7 @@ Deprecated names
8698
∣-trans ↦ ∣ʳ-trans
8799
```
88100

89-
* In `Algebra.Structures`:
101+
* In `Algebra.Structures.Group`:
90102
```agda
91103
uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique
92104
uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique
@@ -119,6 +131,8 @@ Deprecated names
119131
New modules
120132
-----------
121133

134+
* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`.
135+
122136
* `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
123137

124138
* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.

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

Lines changed: 21 additions & 0 deletions
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 (identityˡ-uniqueᴹ; identityʳ-uniqueᴹ)

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

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
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 (identityˡ-unique to identityˡ-uniqueᴹ
24+
; identityʳ-unique to identityʳ-uniqueᴹ)

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

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
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 (identityˡ-unique to identityˡ-uniqueᴹ
24+
; identityʳ-unique to identityʳ-uniqueᴹ)

‎src/Algebra/Module/Structures.agda

Lines changed: 24 additions & 11 deletions
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
@@ -20,10 +16,13 @@ import Algebra.Definitions as Defs
2016
open import Algebra.Module.Definitions
2117
using (module LeftDefs; module RightDefs; module BiDefs
2218
; module SimultaneousBiDefs)
23-
import Algebra.Properties.AbelianGroup as AbelianGroupProperties
2419
open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup)
2520
open import Data.Product.Base using (_,_; proj₁; proj₂)
2621
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+
2726

2827
private
2928
variable
@@ -214,10 +213,17 @@ module _ (ring : Ring r ℓr)
214213
( isGroup to +ᴹ-isGroup
215214
; inverseˡ to -ᴹ‿inverseˡ
216215
; inverseʳ to -ᴹ‿inverseʳ
216+
; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
217+
; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
217218
)
218-
219-
open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public
220-
using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ)
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+
#-}
221227

222228

223229
record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
@@ -244,10 +250,17 @@ module _ (ring : Ring r ℓr)
244250
( isGroup to +ᴹ-isGroup
245251
; inverseˡ to -ᴹ‿inverseˡ
246252
; inverseʳ to -ᴹ‿inverseʳ
253+
; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
254+
; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
247255
)
248-
249-
open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public
250-
using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ)
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+
#-}
251264

252265

253266
module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs)

0 commit comments

Comments
 (0)