Skip to content

Commit a18e51b

Browse files
Tanebgallais
Taneb
and
gallais
authored
Consequences of module monomorphisms (#2276)
* First shot at left semimodule monomorphism consequences * Weaken arguments of properties * Remember I made a variable declaration for this * Left module monomorphisms * Attempt using qualified names rather than renaming * Mark modules as private * Typo * These modules should be private * Monomorphisms over right semimodules * Monomorphisms over right modules * Add properties of bisemimodule monomorphisms * Make these modules private * Properties of bimodule monomorphisms * Properties of semimodule monomorphisms * Move modules to the right location * Add missing options * Properties of module monomorphisms * Fix somewhitespace * Use IsMagma rather than IsMonoid in several places * Spell re-exports consistently * Use modules to make type signatures of structures clearer * [ changelog ] listing the new modules --------- Co-authored-by: Guillaume Allais <[email protected]>
1 parent 8e2754f commit a18e51b

9 files changed

+780
-0
lines changed

‎CHANGELOG.md

+12
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,18 @@ New modules
9191
Algebra.Properties.IdempotentCommutativeMonoid
9292
```
9393

94+
* Consequences of module monomorphisms
95+
```agda
96+
Algebra.Module.Morphism.BimoduleMonomorphism
97+
Algebra.Module.Morphism.BisemimoduleMonomorphism
98+
Algebra.Module.Morphism.LeftModuleMonomorphism
99+
Algebra.Module.Morphism.LeftSemimoduleMonomorphism
100+
Algebra.Module.Morphism.ModuleMonomorphism
101+
Algebra.Module.Morphism.RightModuleMonomorphism
102+
Algebra.Module.Morphism.RightSemimoduleMonomorphism
103+
Algebra.Module.Morphism.SemimoduleMonomorphism
104+
```
105+
94106
* Refactoring of the `Algebra.Solver.*Monoid` implementations, via
95107
a single `Solver` module API based on the existing `Expr`, and
96108
a common `Normal`-form API:

‎src/Algebra/Module/Morphism/BimoduleMonomorphism.agda

+73
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of a monomorphism between bimodules
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Module.Bundles.Raw
10+
open import Algebra.Module.Morphism.Structures
11+
12+
module Algebra.Module.Morphism.BimoduleMonomorphism
13+
{r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBimodule R S a ℓ₁} {N : RawBimodule R S b ℓ₂} {⟦_⟧}
14+
(isBimoduleMonomorphism : IsBimoduleMonomorphism M N ⟦_⟧)
15+
where
16+
17+
open IsBimoduleMonomorphism isBimoduleMonomorphism
18+
private
19+
module M = RawBimodule M
20+
module N = RawBimodule N
21+
22+
open import Algebra.Bundles
23+
open import Algebra.Core
24+
open import Algebra.Module.Structures
25+
open import Algebra.Structures
26+
open import Relation.Binary.Core
27+
28+
------------------------------------------------------------------------
29+
-- Re-exports
30+
31+
open import Algebra.Morphism.GroupMonomorphism +ᴹ-isGroupMonomorphism public
32+
using () renaming
33+
( inverseˡ to -ᴹ‿inverseˡ
34+
; inverseʳ to -ᴹ‿inverseʳ
35+
; inverse to -ᴹ‿inverse
36+
; ⁻¹-cong to -ᴹ‿cong
37+
; ⁻¹-distrib-∙ to -ᴹ‿distrib-+ᴹ
38+
; isGroup to +ᴹ-isGroup
39+
; isAbelianGroup to +ᴹ-isAbelianGroup
40+
)
41+
open import Algebra.Module.Morphism.BisemimoduleMonomorphism isBisemimoduleMonomorphism public
42+
43+
------------------------------------------------------------------------
44+
-- Structures
45+
46+
module _
47+
{ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ -r_ 0r 1r}
48+
{ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ -s_ 0s 1s}
49+
(R-isRing : IsRing _≈r_ _+r_ _*r_ -r_ 0r 1r)
50+
(S-isRing : IsRing _≈s_ _+s_ _*s_ -s_ 0s 1s)
51+
where
52+
53+
private
54+
R-ring : Ring _ _
55+
R-ring = record { isRing = R-isRing }
56+
57+
S-ring : Ring _ _
58+
S-ring = record { isRing = S-isRing }
59+
60+
module R = IsRing R-isRing
61+
module S = IsRing S-isRing
62+
63+
isBimodule
64+
: IsBimodule R-ring S-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_ N._*ᵣ_
65+
→ IsBimodule R-ring S-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_ M._*ᵣ_
66+
isBimodule isBimodule = record
67+
{ isBisemimodule = isBisemimodule R.isSemiring S.isSemiring NN.isBisemimodule
68+
; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong
69+
; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse
70+
}
71+
where
72+
module NN = IsBimodule isBimodule
73+

‎src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda

+149
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Consequences of a monomorphism between bisemimodules
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Module.Bundles.Raw
10+
open import Algebra.Module.Morphism.Structures
11+
12+
module Algebra.Module.Morphism.BisemimoduleMonomorphism
13+
{r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBisemimodule R S a ℓ₁} {N : RawBisemimodule R S b ℓ₂} {⟦_⟧}
14+
(isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M N ⟦_⟧)
15+
where
16+
17+
open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism
18+
private
19+
module M = RawBisemimodule M
20+
module N = RawBisemimodule N
21+
22+
open import Algebra.Bundles
23+
open import Algebra.Core
24+
import Algebra.Module.Definitions.Bi as BiDefs
25+
import Algebra.Module.Definitions.Left as LeftDefs
26+
import Algebra.Module.Definitions.Right as RightDefs
27+
open import Algebra.Module.Structures
28+
open import Algebra.Structures
29+
open import Function.Base
30+
open import Relation.Binary.Core
31+
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
32+
33+
------------------------------------------------------------------------
34+
-- Re-exports
35+
36+
open import Algebra.Morphism.MonoidMonomorphism
37+
+ᴹ-isMonoidMonomorphism public
38+
using ()
39+
renaming
40+
( cong to +ᴹ-cong
41+
; assoc to +ᴹ-assoc
42+
; comm to +ᴹ-comm
43+
; identityˡ to +ᴹ-identityˡ
44+
; identityʳ to +ᴹ-identityʳ
45+
; identity to +ᴹ-identity
46+
; isMagma to +ᴹ-isMagma
47+
; isSemigroup to +ᴹ-isSemigroup
48+
; isMonoid to +ᴹ-isMonoid
49+
; isCommutativeMonoid to +ᴹ-isCommutativeMonoid
50+
)
51+
52+
open import Algebra.Module.Morphism.LeftSemimoduleMonomorphism
53+
isLeftSemimoduleMonomorphism public
54+
using
55+
( *ₗ-cong
56+
; *ₗ-zeroˡ
57+
; *ₗ-distribʳ
58+
; *ₗ-identityˡ
59+
; *ₗ-assoc
60+
; *ₗ-zeroʳ
61+
; *ₗ-distribˡ
62+
; isLeftSemimodule
63+
)
64+
65+
open import Algebra.Module.Morphism.RightSemimoduleMonomorphism
66+
isRightSemimoduleMonomorphism public
67+
using
68+
( *ᵣ-cong
69+
; *ᵣ-zeroʳ
70+
; *ᵣ-distribˡ
71+
; *ᵣ-identityʳ
72+
; *ᵣ-assoc
73+
; *ᵣ-zeroˡ
74+
; *ᵣ-distribʳ
75+
; isRightSemimodule
76+
)
77+
78+
------------------------------------------------------------------------
79+
-- Properties
80+
81+
module _ (+ᴹ-isMagma : IsMagma N._≈ᴹ_ N._+ᴹ_) where
82+
83+
open IsMagma +ᴹ-isMagma
84+
using (setoid)
85+
renaming (∙-cong to +ᴹ-cong)
86+
open SetoidReasoning setoid
87+
88+
private
89+
module MDefs = BiDefs R S M._≈ᴹ_
90+
module NDefs = BiDefs R S N._≈ᴹ_
91+
module LDefs = LeftDefs R N._≈ᴹ_
92+
module RDefs = RightDefs S N._≈ᴹ_
93+
94+
*ₗ-*ᵣ-assoc
95+
: LDefs.LeftCongruent N._*ₗ_ → RDefs.RightCongruent N._*ᵣ_
96+
→ NDefs.Associative N._*ₗ_ N._*ᵣ_
97+
→ MDefs.Associative M._*ₗ_ M._*ᵣ_
98+
*ₗ-*ᵣ-assoc *ₗ-congˡ *ᵣ-congʳ *ₗ-*ᵣ-assoc x m y = injective $ begin
99+
⟦ (x M.*ₗ m) M.*ᵣ y ⟧ ≈⟨ *ᵣ-homo y (x M.*ₗ m) ⟩
100+
⟦ x M.*ₗ m ⟧ N.*ᵣ y ≈⟨ *ᵣ-congʳ (*ₗ-homo x m) ⟩
101+
(x N.*ₗ ⟦ m ⟧) N.*ᵣ y ≈⟨ *ₗ-*ᵣ-assoc x ⟦ m ⟧ y ⟩
102+
x N.*ₗ (⟦ m ⟧ N.*ᵣ y) ≈˘⟨ *ₗ-congˡ (*ᵣ-homo y m) ⟩
103+
x N.*ₗ ⟦ m M.*ᵣ y ⟧ ≈˘⟨ *ₗ-homo x (m M.*ᵣ y) ⟩
104+
⟦ x M.*ₗ (m M.*ᵣ y) ⟧ ∎
105+
106+
------------------------------------------------------------------------
107+
-- Structures
108+
109+
module _
110+
{ℓr} {_≈r_ : Rel R ℓr} {_+r_ _*r_ 0r 1r}
111+
{ℓs} {_≈s_ : Rel S ℓs} {_+s_ _*s_ 0s 1s}
112+
(R-isSemiring : IsSemiring _≈r_ _+r_ _*r_ 0r 1r)
113+
(S-isSemiring : IsSemiring _≈s_ _+s_ _*s_ 0s 1s)
114+
where
115+
116+
private
117+
R-semiring : Semiring _ _
118+
R-semiring = record { isSemiring = R-isSemiring }
119+
120+
S-semiring : Semiring _ _
121+
S-semiring = record { isSemiring = S-isSemiring }
122+
123+
isBisemimodule
124+
: IsBisemimodule R-semiring S-semiring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N._*ₗ_ N._*ᵣ_
125+
→ IsBisemimodule R-semiring S-semiring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M._*ₗ_ M._*ᵣ_
126+
isBisemimodule isBisemimodule = record
127+
{ +ᴹ-isCommutativeMonoid = +ᴹ-isCommutativeMonoid NN.+ᴹ-isCommutativeMonoid
128+
; isPreleftSemimodule = record
129+
{ *ₗ-cong = *ₗ-cong NN.+ᴹ-isMagma NN.*ₗ-cong
130+
; *ₗ-zeroˡ = *ₗ-zeroˡ NN.+ᴹ-isMagma NN.*ₗ-zeroˡ
131+
; *ₗ-distribʳ = *ₗ-distribʳ NN.+ᴹ-isMagma NN.*ₗ-distribʳ
132+
; *ₗ-identityˡ = *ₗ-identityˡ NN.+ᴹ-isMagma NN.*ₗ-identityˡ
133+
; *ₗ-assoc = *ₗ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-assoc
134+
; *ₗ-zeroʳ = *ₗ-zeroʳ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-zeroʳ
135+
; *ₗ-distribˡ = *ₗ-distribˡ NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ₗ-distribˡ
136+
}
137+
; isPrerightSemimodule = record
138+
{ *ᵣ-cong = *ᵣ-cong NN.+ᴹ-isMagma NN.*ᵣ-cong
139+
; *ᵣ-zeroʳ = *ᵣ-zeroʳ NN.+ᴹ-isMagma NN.*ᵣ-zeroʳ
140+
; *ᵣ-distribˡ = *ᵣ-distribˡ NN.+ᴹ-isMagma NN.*ᵣ-distribˡ
141+
; *ᵣ-identityʳ = *ᵣ-identityʳ NN.+ᴹ-isMagma NN.*ᵣ-identityʳ
142+
; *ᵣ-assoc = *ᵣ-assoc NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-assoc
143+
; *ᵣ-zeroˡ = *ᵣ-zeroˡ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-zeroˡ
144+
; *ᵣ-distribʳ = *ᵣ-distribʳ NN.+ᴹ-isMagma NN.*ᵣ-congʳ NN.*ᵣ-distribʳ
145+
}
146+
; *ₗ-*ᵣ-assoc = *ₗ-*ᵣ-assoc NN.+ᴹ-isMagma NN.*ₗ-congˡ NN.*ᵣ-congʳ NN.*ₗ-*ᵣ-assoc
147+
}
148+
where
149+
module NN = IsBisemimodule isBisemimodule

‎src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda

+62
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Consequences of a monomorphism between left modules
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Algebra.Module.Bundles.Raw
10+
open import Algebra.Module.Morphism.Structures
11+
12+
module Algebra.Module.Morphism.LeftModuleMonomorphism
13+
{r a b ℓ₁ ℓ₂} {R : Set r} {M : RawLeftModule R a ℓ₁} {N : RawLeftModule R b ℓ₂} {⟦_⟧}
14+
(isLeftModuleMonomorphism : IsLeftModuleMonomorphism M N ⟦_⟧)
15+
where
16+
17+
open IsLeftModuleMonomorphism isLeftModuleMonomorphism
18+
private
19+
module M = RawLeftModule M
20+
module N = RawLeftModule N
21+
22+
open import Algebra.Bundles
23+
open import Algebra.Core
24+
open import Algebra.Module.Structures
25+
open import Algebra.Structures
26+
open import Relation.Binary.Core
27+
28+
------------------------------------------------------------------------
29+
-- Re-exports
30+
31+
open import Algebra.Morphism.GroupMonomorphism +ᴹ-isGroupMonomorphism public
32+
using () renaming
33+
( inverseˡ to -ᴹ‿inverseˡ
34+
; inverseʳ to -ᴹ‿inverseʳ
35+
; inverse to -ᴹ‿inverse
36+
; ⁻¹-cong to -ᴹ‿cong
37+
; ⁻¹-distrib-∙ to -ᴹ‿distrib-+ᴹ
38+
; isGroup to +ᴹ-isGroup
39+
; isAbelianGroup to +ᴹ-isAbelianGroup
40+
)
41+
open import Algebra.Module.Morphism.LeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism public
42+
43+
------------------------------------------------------------------------
44+
-- Structures
45+
46+
module _ {ℓr} {_≈_ : Rel R ℓr} {_+_ _*_ -_ 0# 1#} (R-isRing : IsRing _≈_ _+_ _*_ -_ 0# 1#) where
47+
48+
private
49+
R-ring : Ring _ _
50+
R-ring = record { isRing = R-isRing }
51+
open IsRing R-isRing
52+
53+
isLeftModule
54+
: IsLeftModule R-ring N._≈ᴹ_ N._+ᴹ_ N.0ᴹ N.-ᴹ_ N._*ₗ_
55+
→ IsLeftModule R-ring M._≈ᴹ_ M._+ᴹ_ M.0ᴹ M.-ᴹ_ M._*ₗ_
56+
isLeftModule isLeftModule = record
57+
{ isLeftSemimodule = isLeftSemimodule isSemiring NN.isLeftSemimodule
58+
; -ᴹ‿cong = -ᴹ‿cong NN.+ᴹ-isMagma NN.-ᴹ‿cong
59+
; -ᴹ‿inverse = -ᴹ‿inverse NN.+ᴹ-isMagma NN.-ᴹ‿inverse
60+
}
61+
where
62+
module NN = IsLeftModule isLeftModule

0 commit comments

Comments
 (0)