Skip to content

Commit 64e2ba0

Browse files
Tanebandreasabel
Taneb
authored and
andreasabel
committed
Parametrize module morphisms by raw bundles (#2265)
* Index module morphisms by raw bundles * Use synonyms for RawModule's RawBimodule etc * Update changelog * Update constructed morphisms * Fix Algebra.Module.Morphism.ModuleHomomorphism
1 parent 63b61c6 commit 64e2ba0

File tree

5 files changed

+153
-154
lines changed

5 files changed

+153
-154
lines changed

‎CHANGELOG.md

+8
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,14 @@ Bug-fixes
1616
Non-backwards compatible changes
1717
--------------------------------
1818

19+
* The modules and morphisms in `Algebra.Module.Morphism.Structures` are now
20+
parametrized by _raw_ bundles rather than lawful bundles, in line with other
21+
modules defining morphism structures.
22+
* The definitions in `Algebra.Module.Morphism.Construct.Composition` are now
23+
parametrized by _raw_ bundles, and as such take a proof of transitivity.
24+
* The definitions in `Algebra.Module.Morphism.Construct.Identity` are now
25+
parametrized by _raw_ bundles, and as such take a proof of reflexivity.
26+
1927
Other major improvements
2028
------------------------
2129

‎src/Algebra/Module/Morphism/Construct/Composition.agda

+69-61
Original file line numberDiff line numberDiff line change
@@ -8,24 +8,25 @@
88

99
module Algebra.Module.Morphism.Construct.Composition where
1010

11-
open import Algebra.Bundles
12-
open import Algebra.Module.Bundles
11+
open import Algebra.Module.Bundles.Raw
1312
open import Algebra.Module.Morphism.Structures
1413
open import Algebra.Morphism.Construct.Composition
1514
open import Function.Base using (_∘_)
1615
import Function.Construct.Composition as Func
1716
open import Level using (Level)
17+
open import Relation.Binary.Definitions using (Transitive)
1818

1919
private
2020
variable
21-
r ℓr s ℓs m₁ ℓm₁ m₂ ℓm₂ m₃ ℓm₃ : Level
21+
r s m₁ ℓm₁ m₂ ℓm₂ m₃ ℓm₃ : Level
2222

2323
module _
24-
{semiring : Semiring r ℓr}
25-
{M₁ : LeftSemimodule semiring m₁ ℓm₁}
26-
{M₂ : LeftSemimodule semiring m₂ ℓm₂}
27-
{M₃ : LeftSemimodule semiring m₃ ℓm₃}
28-
(open LeftSemimodule)
24+
{R : Set r}
25+
{M₁ : RawLeftSemimodule R m₁ ℓm₁}
26+
{M₂ : RawLeftSemimodule R m₂ ℓm₂}
27+
{M₃ : RawLeftSemimodule R m₃ ℓm₃}
28+
(open RawLeftSemimodule)
29+
(≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
2930
{f : Carrierᴹ M₁ → Carrierᴹ M₂}
3031
{g : Carrierᴹ M₂ → Carrierᴹ M₃}
3132
where
@@ -34,8 +35,8 @@ module _
3435
IsLeftSemimoduleHomomorphism M₂ M₃ g →
3536
IsLeftSemimoduleHomomorphism M₁ M₃ (g ∘ f)
3637
isLeftSemimoduleHomomorphism f-homo g-homo = record
37-
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
38-
; *ₗ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
38+
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
39+
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
3940
} where module F = IsLeftSemimoduleHomomorphism f-homo; module G = IsLeftSemimoduleHomomorphism g-homo
4041

4142
isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ f →
@@ -55,11 +56,12 @@ module _
5556
} where module F = IsLeftSemimoduleIsomorphism f-iso; module G = IsLeftSemimoduleIsomorphism g-iso
5657

5758
module _
58-
{ring : Ring r ℓr}
59-
{M₁ : LeftModule ring m₁ ℓm₁}
60-
{M₂ : LeftModule ring m₂ ℓm₂}
61-
{M₃ : LeftModule ring m₃ ℓm₃}
62-
(open LeftModule)
59+
{R : Set r}
60+
{M₁ : RawLeftModule R m₁ ℓm₁}
61+
{M₂ : RawLeftModule R m₂ ℓm₂}
62+
{M₃ : RawLeftModule R m₃ ℓm₃}
63+
(open RawLeftModule)
64+
(≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
6365
{f : Carrierᴹ M₁ → Carrierᴹ M₂}
6466
{g : Carrierᴹ M₂ → Carrierᴹ M₃}
6567
where
@@ -68,8 +70,8 @@ module _
6870
IsLeftModuleHomomorphism M₂ M₃ g →
6971
IsLeftModuleHomomorphism M₁ M₃ (g ∘ f)
7072
isLeftModuleHomomorphism f-homo g-homo = record
71-
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
72-
; *ₗ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
73+
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
74+
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
7375
} where module F = IsLeftModuleHomomorphism f-homo; module G = IsLeftModuleHomomorphism g-homo
7476

7577
isLeftModuleMonomorphism : IsLeftModuleMonomorphism M₁ M₂ f →
@@ -89,11 +91,12 @@ module _
8991
} where module F = IsLeftModuleIsomorphism f-iso; module G = IsLeftModuleIsomorphism g-iso
9092

9193
module _
92-
{semiring : Semiring r ℓr}
93-
{M₁ : RightSemimodule semiring m₁ ℓm₁}
94-
{M₂ : RightSemimodule semiring m₂ ℓm₂}
95-
{M₃ : RightSemimodule semiring m₃ ℓm₃}
96-
(open RightSemimodule)
94+
{R : Set r}
95+
{M₁ : RawRightSemimodule R m₁ ℓm₁}
96+
{M₂ : RawRightSemimodule R m₂ ℓm₂}
97+
{M₃ : RawRightSemimodule R m₃ ℓm₃}
98+
(open RawRightSemimodule)
99+
(≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
97100
{f : Carrierᴹ M₁ → Carrierᴹ M₂}
98101
{g : Carrierᴹ M₂ → Carrierᴹ M₃}
99102
where
@@ -102,8 +105,8 @@ module _
102105
IsRightSemimoduleHomomorphism M₂ M₃ g →
103106
IsRightSemimoduleHomomorphism M₁ M₃ (g ∘ f)
104107
isRightSemimoduleHomomorphism f-homo g-homo = record
105-
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
106-
; *ᵣ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
108+
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
109+
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
107110
} where module F = IsRightSemimoduleHomomorphism f-homo; module G = IsRightSemimoduleHomomorphism g-homo
108111

109112
isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M₁ M₂ f →
@@ -123,11 +126,12 @@ module _
123126
} where module F = IsRightSemimoduleIsomorphism f-iso; module G = IsRightSemimoduleIsomorphism g-iso
124127

125128
module _
126-
{ring : Ring r ℓr}
127-
{M₁ : RightModule ring m₁ ℓm₁}
128-
{M₂ : RightModule ring m₂ ℓm₂}
129-
{M₃ : RightModule ring m₃ ℓm₃}
130-
(open RightModule)
129+
{R : Set r}
130+
{M₁ : RawRightModule R m₁ ℓm₁}
131+
{M₂ : RawRightModule R m₂ ℓm₂}
132+
{M₃ : RawRightModule R m₃ ℓm₃}
133+
(open RawRightModule)
134+
(≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
131135
{f : Carrierᴹ M₁ → Carrierᴹ M₂}
132136
{g : Carrierᴹ M₂ → Carrierᴹ M₃}
133137
where
@@ -136,8 +140,8 @@ module _
136140
IsRightModuleHomomorphism M₂ M₃ g →
137141
IsRightModuleHomomorphism M₁ M₃ (g ∘ f)
138142
isRightModuleHomomorphism f-homo g-homo = record
139-
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
140-
; *ᵣ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
143+
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
144+
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
141145
} where module F = IsRightModuleHomomorphism f-homo; module G = IsRightModuleHomomorphism g-homo
142146

143147
isRightModuleMonomorphism : IsRightModuleMonomorphism M₁ M₂ f →
@@ -157,12 +161,13 @@ module _
157161
} where module F = IsRightModuleIsomorphism f-iso; module G = IsRightModuleIsomorphism g-iso
158162

159163
module _
160-
{R-semiring : Semiring r ℓr}
161-
{S-semiring : Semiring s ℓs}
162-
{M₁ : Bisemimodule R-semiring S-semiring m₁ ℓm₁}
163-
{M₂ : Bisemimodule R-semiring S-semiring m₂ ℓm₂}
164-
{M₃ : Bisemimodule R-semiring S-semiring m₃ ℓm₃}
165-
(open Bisemimodule)
164+
{R : Set r}
165+
{S : Set s}
166+
{M₁ : RawBisemimodule R S m₁ ℓm₁}
167+
{M₂ : RawBisemimodule R S m₂ ℓm₂}
168+
{M₃ : RawBisemimodule R S m₃ ℓm₃}
169+
(open RawBisemimodule)
170+
(≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
166171
{f : Carrierᴹ M₁ → Carrierᴹ M₂}
167172
{g : Carrierᴹ M₂ → Carrierᴹ M₃}
168173
where
@@ -171,9 +176,9 @@ module _
171176
IsBisemimoduleHomomorphism M₂ M₃ g →
172177
IsBisemimoduleHomomorphism M₁ M₃ (g ∘ f)
173178
isBisemimoduleHomomorphism f-homo g-homo = record
174-
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
175-
; *ₗ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
176-
; *ᵣ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
179+
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
180+
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
181+
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
177182
} where module F = IsBisemimoduleHomomorphism f-homo; module G = IsBisemimoduleHomomorphism g-homo
178183

179184
isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M₁ M₂ f →
@@ -193,12 +198,13 @@ module _
193198
} where module F = IsBisemimoduleIsomorphism f-iso; module G = IsBisemimoduleIsomorphism g-iso
194199

195200
module _
196-
{R-ring : Ring r ℓr}
197-
{S-ring : Ring s ℓs}
198-
{M₁ : Bimodule R-ring S-ring m₁ ℓm₁}
199-
{M₂ : Bimodule R-ring S-ring m₂ ℓm₂}
200-
{M₃ : Bimodule R-ring S-ring m₃ ℓm₃}
201-
(open Bimodule)
201+
{R : Set r}
202+
{S : Set s}
203+
{M₁ : RawBimodule R S m₁ ℓm₁}
204+
{M₂ : RawBimodule R S m₂ ℓm₂}
205+
{M₃ : RawBimodule R S m₃ ℓm₃}
206+
(open RawBimodule)
207+
(≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
202208
{f : Carrierᴹ M₁ → Carrierᴹ M₂}
203209
{g : Carrierᴹ M₂ → Carrierᴹ M₃}
204210
where
@@ -207,9 +213,9 @@ module _
207213
IsBimoduleHomomorphism M₂ M₃ g →
208214
IsBimoduleHomomorphism M₁ M₃ (g ∘ f)
209215
isBimoduleHomomorphism f-homo g-homo = record
210-
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism (≈ᴹ-trans M₃) F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
211-
; *ₗ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
212-
; *ᵣ-homo = λ r x → ≈ᴹ-trans M₃ (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
216+
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
217+
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
218+
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
213219
} where module F = IsBimoduleHomomorphism f-homo; module G = IsBimoduleHomomorphism g-homo
214220

215221
isBimoduleMonomorphism : IsBimoduleMonomorphism M₁ M₂ f →
@@ -229,11 +235,12 @@ module _
229235
} where module F = IsBimoduleIsomorphism f-iso; module G = IsBimoduleIsomorphism g-iso
230236

231237
module _
232-
{commutativeSemiring : CommutativeSemiring r ℓr}
233-
{M₁ : Semimodule commutativeSemiring m₁ ℓm₁}
234-
{M₂ : Semimodule commutativeSemiring m₂ ℓm₂}
235-
{M₃ : Semimodule commutativeSemiring m₃ ℓm₃}
236-
(open Semimodule)
238+
{R : Set r}
239+
{M₁ : RawSemimodule R m₁ ℓm₁}
240+
{M₂ : RawSemimodule R m₂ ℓm₂}
241+
{M₃ : RawSemimodule R m₃ ℓm₃}
242+
(open RawSemimodule)
243+
(≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
237244
{f : Carrierᴹ M₁ → Carrierᴹ M₂}
238245
{g : Carrierᴹ M₂ → Carrierᴹ M₃}
239246
where
@@ -242,7 +249,7 @@ module _
242249
IsSemimoduleHomomorphism M₂ M₃ g →
243250
IsSemimoduleHomomorphism M₁ M₃ (g ∘ f)
244251
isSemimoduleHomomorphism f-homo g-homo = record
245-
{ isBisemimoduleHomomorphism = isBisemimoduleHomomorphism F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism
252+
{ isBisemimoduleHomomorphism = isBisemimoduleHomomorphism ≈ᴹ₃-trans F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism
246253
} where module F = IsSemimoduleHomomorphism f-homo; module G = IsSemimoduleHomomorphism g-homo
247254

248255
isSemimoduleMonomorphism : IsSemimoduleMonomorphism M₁ M₂ f →
@@ -262,11 +269,12 @@ module _
262269
} where module F = IsSemimoduleIsomorphism f-iso; module G = IsSemimoduleIsomorphism g-iso
263270

264271
module _
265-
{commutativeRing : CommutativeRing r ℓr}
266-
{M₁ : Module commutativeRing m₁ ℓm₁}
267-
{M₂ : Module commutativeRing m₂ ℓm₂}
268-
{M₃ : Module commutativeRing m₃ ℓm₃}
269-
(open Module)
272+
{R : Set r}
273+
{M₁ : RawModule R m₁ ℓm₁}
274+
{M₂ : RawModule R m₂ ℓm₂}
275+
{M₃ : RawModule R m₃ ℓm₃}
276+
(open RawModule)
277+
(≈ᴹ₃-trans : Transitive (_≈ᴹ_ M₃))
270278
{f : Carrierᴹ M₁ → Carrierᴹ M₂}
271279
{g : Carrierᴹ M₂ → Carrierᴹ M₃}
272280
where
@@ -275,7 +283,7 @@ module _
275283
IsModuleHomomorphism M₂ M₃ g →
276284
IsModuleHomomorphism M₁ M₃ (g ∘ f)
277285
isModuleHomomorphism f-homo g-homo = record
278-
{ isBimoduleHomomorphism = isBimoduleHomomorphism F.isBimoduleHomomorphism G.isBimoduleHomomorphism
286+
{ isBimoduleHomomorphism = isBimoduleHomomorphism ≈ᴹ₃-trans F.isBimoduleHomomorphism G.isBimoduleHomomorphism
279287
} where module F = IsModuleHomomorphism f-homo; module G = IsModuleHomomorphism g-homo
280288

281289
isModuleMonomorphism : IsModuleMonomorphism M₁ M₂ f →

‎src/Algebra/Module/Morphism/Construct/Identity.agda

+13-21
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,7 @@
88

99
module Algebra.Module.Morphism.Construct.Identity where
1010

11-
open import Algebra.Bundles
12-
open import Algebra.Module.Bundles
11+
open import Algebra.Module.Bundles.Raw
1312
open import Algebra.Module.Morphism.Structures
1413
using ( module LeftSemimoduleMorphisms
1514
; module LeftModuleMorphisms
@@ -25,13 +24,13 @@ open import Data.Product.Base using (_,_)
2524
open import Function.Base using (id)
2625
import Function.Construct.Identity as Id
2726
open import Level using (Level)
27+
open import Relation.Binary.Definitions using (Reflexive)
2828

2929
private
3030
variable
31-
r ℓr s ℓs m ℓm : Level
31+
r s m ℓm : Level
3232

33-
module _ {semiring : Semiring r ℓr} (M : LeftSemimodule semiring m ℓm) where
34-
open LeftSemimodule M using (≈ᴹ-refl)
33+
module _ {R : Set r} (M : RawLeftSemimodule R m ℓm) (open RawLeftSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
3534
open LeftSemimoduleMorphisms M M
3635

3736
isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism id
@@ -52,8 +51,7 @@ module _ {semiring : Semiring r ℓr} (M : LeftSemimodule semiring m ℓm) where
5251
; surjective = Id.surjective _
5352
}
5453

55-
module _ {ring : Ring r ℓr} (M : LeftModule ring m ℓm) where
56-
open LeftModule M using (≈ᴹ-refl)
54+
module _ {R : Set r} (M : RawLeftModule R m ℓm) (open RawLeftModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
5755
open LeftModuleMorphisms M M
5856

5957
isLeftModuleHomomorphism : IsLeftModuleHomomorphism id
@@ -74,8 +72,7 @@ module _ {ring : Ring r ℓr} (M : LeftModule ring m ℓm) where
7472
; surjective = Id.surjective _
7573
}
7674

77-
module _ {semiring : Semiring r ℓr} (M : RightSemimodule semiring m ℓm) where
78-
open RightSemimodule M using (≈ᴹ-refl)
75+
module _ {R : Set r} (M : RawRightSemimodule R m ℓm) (open RawRightSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
7976
open RightSemimoduleMorphisms M M
8077

8178
isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism id
@@ -96,8 +93,7 @@ module _ {semiring : Semiring r ℓr} (M : RightSemimodule semiring m ℓm) wher
9693
; surjective = Id.surjective _
9794
}
9895

99-
module _ {ring : Ring r ℓr} (M : RightModule ring m ℓm) where
100-
open RightModule M using (≈ᴹ-refl)
96+
module _ {R : Set r} (M : RawRightModule R m ℓm) (open RawRightModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
10197
open RightModuleMorphisms M M
10298

10399
isRightModuleHomomorphism : IsRightModuleHomomorphism id
@@ -118,8 +114,7 @@ module _ {ring : Ring r ℓr} (M : RightModule ring m ℓm) where
118114
; surjective = Id.surjective _
119115
}
120116

121-
module _ {R-semiring : Semiring r ℓr} {S-semiring : Semiring s ℓs} (M : Bisemimodule R-semiring S-semiring m ℓm) where
122-
open Bisemimodule M using (≈ᴹ-refl)
117+
module _ {R : Set r} {S : Set s} (M : RawBisemimodule R S m ℓm) (open RawBisemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
123118
open BisemimoduleMorphisms M M
124119

125120
isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism id
@@ -141,8 +136,7 @@ module _ {R-semiring : Semiring r ℓr} {S-semiring : Semiring s ℓs} (M : Bise
141136
; surjective = Id.surjective _
142137
}
143138

144-
module _ {R-ring : Ring r ℓr} {S-ring : Ring r ℓr} (M : Bimodule R-ring S-ring m ℓm) where
145-
open Bimodule M using (≈ᴹ-refl)
139+
module _ {R : Set r} {S : Set s} (M : RawBimodule R S m ℓm) (open RawBimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
146140
open BimoduleMorphisms M M
147141

148142
isBimoduleHomomorphism : IsBimoduleHomomorphism id
@@ -164,13 +158,12 @@ module _ {R-ring : Ring r ℓr} {S-ring : Ring r ℓr} (M : Bimodule R-ring S-ri
164158
; surjective = Id.surjective _
165159
}
166160

167-
module _ {commutativeSemiring : CommutativeSemiring r ℓr} (M : Semimodule commutativeSemiring m ℓm) where
168-
open Semimodule M using (≈ᴹ-refl)
161+
module _ {R : Set r} (M : RawSemimodule R m ℓm) (open RawSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
169162
open SemimoduleMorphisms M M
170163

171164
isSemimoduleHomomorphism : IsSemimoduleHomomorphism id
172165
isSemimoduleHomomorphism = record
173-
{ isBisemimoduleHomomorphism = isBisemimoduleHomomorphism _
166+
{ isBisemimoduleHomomorphism = isBisemimoduleHomomorphism _ ≈ᴹ-refl
174167
}
175168

176169
isSemimoduleMonomorphism : IsSemimoduleMonomorphism id
@@ -185,13 +178,12 @@ module _ {commutativeSemiring : CommutativeSemiring r ℓr} (M : Semimodule comm
185178
; surjective = Id.surjective _
186179
}
187180

188-
module _ {commutativeRing : CommutativeRing r ℓr} (M : Module commutativeRing m ℓm) where
189-
open Module M using (≈ᴹ-refl)
181+
module _ {R : Set r} (M : RawModule R m ℓm) (open RawModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
190182
open ModuleMorphisms M M
191183

192184
isModuleHomomorphism : IsModuleHomomorphism id
193185
isModuleHomomorphism = record
194-
{ isBimoduleHomomorphism = isBimoduleHomomorphism _
186+
{ isBimoduleHomomorphism = isBimoduleHomomorphism _ ≈ᴹ-refl
195187
}
196188

197189
isModuleMonomorphism : IsModuleMonomorphism id

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

+3-3
Original file line numberDiff line numberDiff line change
@@ -17,10 +17,10 @@ module Algebra.Module.Morphism.ModuleHomomorphism
1717
{r ℓr m ℓm : Level}
1818
{ring : CommutativeRing r ℓr}
1919
(modA modB : Module ring m ℓm)
20-
(open Module modA using () renaming (Carrierᴹ to A))
21-
(open Module modB using () renaming (Carrierᴹ to B))
20+
(open Module modA using () renaming (Carrierᴹ to A; rawModule to rawModA))
21+
(open Module modB using () renaming (Carrierᴹ to B; rawModule to rawModB))
2222
{f : A → B}
23-
(open MorphismStructures.ModuleMorphisms modA modB)
23+
(open MorphismStructures.ModuleMorphisms rawModA rawModB)
2424
(isModuleHomomorphism : IsModuleHomomorphism f)
2525
where
2626

0 commit comments

Comments
 (0)