Skip to content

Commit 5365791

Browse files
laMudrilaMudri
authored
Add some standard algebraic constructs (unit and pairing) (#1109)
1 parent 94b61c8 commit 5365791

File tree

5 files changed

+401
-0
lines changed

5 files changed

+401
-0
lines changed

‎CHANGELOG.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,13 @@ Deprecated names
108108
New modules
109109
-----------
110110

111+
* The direct products and zeros over algebraic structures and bundles:
112+
```
113+
Algebra.Construct.Zero
114+
Algebra.Construct.DirectProduct
115+
Algebra.Module.Construct.DirectProduct.agda
116+
```
117+
111118
* Substituting the notion of equality for various structures
112119
```
113120
Algebra.Construct.Subst.Equality

‎src/Algebra/Construct/DirectProduct.agda

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances of algebraic structures made by taking two other instances
5+
-- A and B, and having elements of the new instance be pairs |A| × |B|.
6+
-- In mathematics, this would usually be written A × B or A ⊕ B.
7+
--
8+
-- From semigroups up, these new instances are products of the relevant
9+
-- category. For structures with commutative addition (commutative
10+
-- monoids, Abelian groups, semirings, rings), the direct product is
11+
-- also the coproduct, making it a biproduct.
12+
------------------------------------------------------------------------
13+
14+
{-# OPTIONS --without-K --safe #-}
15+
16+
module Algebra.Construct.DirectProduct where
17+
18+
open import Algebra
19+
open import Data.Product
20+
open import Data.Product.Relation.Binary.Pointwise.NonDependent
21+
open import Level using (Level; _⊔_)
22+
23+
private
24+
variable
25+
a b ℓ₁ ℓ₂ : Level
26+
27+
------------------------------------------------------------------------
28+
-- Raw bundles
29+
30+
rawMagma : RawMagma a ℓ₁ → RawMagma b ℓ₂ → RawMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
31+
rawMagma M N = record
32+
{ Carrier = M.Carrier × N.Carrier
33+
; _≈_ = Pointwise M._≈_ N._≈_
34+
; _∙_ = zip M._∙_ N._∙_
35+
} where module M = RawMagma M; module N = RawMagma N
36+
37+
rawMonoid : RawMonoid a ℓ₁ → RawMonoid b ℓ₂ → RawMonoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
38+
rawMonoid M N = record
39+
{ Carrier = M.Carrier × N.Carrier
40+
; _≈_ = Pointwise M._≈_ N._≈_
41+
; _∙_ = zip M._∙_ N._∙_
42+
; ε = M.ε , N.ε
43+
} where module M = RawMonoid M; module N = RawMonoid N
44+
45+
rawGroup : RawGroup a ℓ₁ → RawGroup b ℓ₂ → RawGroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
46+
rawGroup G H = record
47+
{ Carrier = G.Carrier × H.Carrier
48+
; _≈_ = Pointwise G._≈_ H._≈_
49+
; _∙_ = zip G._∙_ H._∙_
50+
; ε = G.ε , H.ε
51+
; _⁻¹ = map G._⁻¹ H._⁻¹
52+
} where module G = RawGroup G; module H = RawGroup H
53+
54+
------------------------------------------------------------------------
55+
-- Bundles
56+
57+
magma : Magma a ℓ₁ → Magma b ℓ₂ → Magma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
58+
magma M N = record
59+
{ Carrier = M.Carrier × N.Carrier
60+
; _≈_ = Pointwise M._≈_ N._≈_
61+
; _∙_ = zip M._∙_ N._∙_
62+
; isMagma = record
63+
{ isEquivalence = ×-isEquivalence M.isEquivalence N.isEquivalence
64+
; ∙-cong = zip M.∙-cong N.∙-cong
65+
}
66+
} where module M = Magma M; module N = Magma N
67+
68+
semigroup : Semigroup a ℓ₁ → Semigroup b ℓ₂ → Semigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
69+
semigroup G H = record
70+
{ isSemigroup = record
71+
{ isMagma = Magma.isMagma (magma G.magma H.magma)
72+
; assoc = λ x y z → (G.assoc , H.assoc) <*> x <*> y <*> z
73+
}
74+
} where module G = Semigroup G; module H = Semigroup H
75+
76+
band : Band a ℓ₁ → Band b ℓ₂ → Band (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
77+
band B C = record
78+
{ isBand = record
79+
{ isSemigroup = Semigroup.isSemigroup (semigroup B.semigroup C.semigroup)
80+
; idem = λ x → (B.idem , C.idem) <*> x
81+
}
82+
} where module B = Band B; module C = Band C
83+
84+
commutativeSemigroup : CommutativeSemigroup a ℓ₁ → CommutativeSemigroup b ℓ₂ →
85+
CommutativeSemigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
86+
commutativeSemigroup G H = record
87+
{ isCommutativeSemigroup = record
88+
{ isSemigroup = Semigroup.isSemigroup (semigroup G.semigroup H.semigroup)
89+
; comm = λ x y → (G.comm , H.comm) <*> x <*> y
90+
}
91+
} where module G = CommutativeSemigroup G; module H = CommutativeSemigroup H
92+
93+
semilattice : Semilattice a ℓ₁ → Semilattice b ℓ₂ →
94+
Semilattice (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
95+
semilattice L M = record
96+
{ isSemilattice = record
97+
{ isBand = Band.isBand (band L.band M.band)
98+
; comm = λ x y → (L.comm , M.comm) <*> x <*> y
99+
}
100+
} where module L = Semilattice L; module M = Semilattice M
101+
102+
monoid : Monoid a ℓ₁ → Monoid b ℓ₂ → Monoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
103+
monoid M N = record
104+
{ ε = M.ε , N.ε
105+
; isMonoid = record
106+
{ isSemigroup = Semigroup.isSemigroup (semigroup M.semigroup N.semigroup)
107+
; identity = (M.identityˡ , N.identityˡ <*>_)
108+
, (M.identityʳ , N.identityʳ <*>_)
109+
}
110+
} where module M = Monoid M; module N = Monoid N
111+
112+
commutativeMonoid : CommutativeMonoid a ℓ₁ → CommutativeMonoid b ℓ₂ →
113+
CommutativeMonoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
114+
commutativeMonoid M N = record
115+
{ isCommutativeMonoid = record
116+
{ isMonoid = Monoid.isMonoid (monoid M.monoid N.monoid)
117+
; comm = λ x y → (M.comm , N.comm) <*> x <*> y
118+
}
119+
} where module M = CommutativeMonoid M; module N = CommutativeMonoid N
120+
121+
idempotentCommutativeMonoid :
122+
IdempotentCommutativeMonoid a ℓ₁ → IdempotentCommutativeMonoid b ℓ₂ →
123+
IdempotentCommutativeMonoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
124+
idempotentCommutativeMonoid M N = record
125+
{ isIdempotentCommutativeMonoid = record
126+
{ isCommutativeMonoid = CommutativeMonoid.isCommutativeMonoid
127+
(commutativeMonoid M.commutativeMonoid N.commutativeMonoid)
128+
; idem = λ x → (M.idem , N.idem) <*> x
129+
}
130+
}
131+
where
132+
module M = IdempotentCommutativeMonoid M
133+
module N = IdempotentCommutativeMonoid N
134+
135+
group : Group a ℓ₁ → Group b ℓ₂ → Group (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
136+
group G H = record
137+
{ _⁻¹ = map G._⁻¹ H._⁻¹
138+
; isGroup = record
139+
{ isMonoid = Monoid.isMonoid (monoid G.monoid H.monoid)
140+
; inverse = (λ x → (G.inverseˡ , H.inverseˡ) <*> x)
141+
, (λ x → (G.inverseʳ , H.inverseʳ) <*> x)
142+
; ⁻¹-cong = map G.⁻¹-cong H.⁻¹-cong
143+
}
144+
} where module G = Group G; module H = Group H
145+
146+
abelianGroup : AbelianGroup a ℓ₁ → AbelianGroup b ℓ₂ →
147+
AbelianGroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
148+
abelianGroup G H = record
149+
{ isAbelianGroup = record
150+
{ isGroup = Group.isGroup (group G.group H.group)
151+
; comm = λ x y → (G.comm , H.comm) <*> x <*> y
152+
}
153+
} where module G = AbelianGroup G; module H = AbelianGroup H

‎src/Algebra/Construct/Zero.agda

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Instances of algebraic structures where the carrier is ⊤.
5+
-- In mathematics, this is usually called 0.
6+
--
7+
-- From monoids up, these are are zero-objects – i.e, both the initial
8+
-- and the terminal object in the relevant category.
9+
-- For structures without an identity element, we can't necessarily
10+
-- produce a homomorphism out of 0, because there is an instance of such
11+
-- a structure with an empty Carrier.
12+
------------------------------------------------------------------------
13+
14+
{-# OPTIONS --without-K --safe #-}
15+
16+
module Algebra.Construct.Zero where
17+
18+
open import Algebra.Bundles
19+
open import Data.Unit
20+
open import Level using (Level; 0ℓ)
21+
22+
------------------------------------------------------------------------
23+
-- Raw bundles
24+
25+
rawMagma : RawMagma 0ℓ 0ℓ
26+
rawMagma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
27+
28+
rawMonoid : RawMonoid 0ℓ 0ℓ
29+
rawMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
30+
31+
rawGroup : RawGroup 0ℓ 0ℓ
32+
rawGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
33+
34+
------------------------------------------------------------------------
35+
-- Bundles
36+
37+
magma : Magma 0ℓ 0ℓ
38+
magma = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
39+
40+
semigroup : Semigroup 0ℓ 0ℓ
41+
semigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
42+
43+
band : Band 0ℓ 0ℓ
44+
band = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
45+
46+
commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
47+
commutativeSemigroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
48+
49+
semilattice : Semilattice 0ℓ 0ℓ
50+
semilattice = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
51+
52+
monoid : Monoid 0ℓ 0ℓ
53+
monoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
54+
55+
commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
56+
commutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
57+
58+
idempotentCommutativeMonoid : IdempotentCommutativeMonoid 0ℓ 0ℓ
59+
idempotentCommutativeMonoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
60+
61+
group : Group 0ℓ 0ℓ
62+
group = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
63+
64+
abelianGroup : AbelianGroup 0ℓ 0ℓ
65+
abelianGroup = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }

‎src/Algebra/Module/Construct/DirectProduct.agda

Lines changed: 159 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- This module constructs the biproduct of two R-modules, and similar
5+
-- for weaker module-like structures.
6+
-- The intended universal property is that the biproduct is both a
7+
-- product and a coproduct in the category of R-modules.
8+
------------------------------------------------------------------------
9+
10+
{-# OPTIONS --without-K --safe #-}
11+
12+
module Algebra.Module.Construct.DirectProduct where
13+
14+
open import Algebra.Bundles
15+
open import Algebra.Construct.DirectProduct
16+
open import Algebra.Module.Bundles
17+
open import Data.Product
18+
open import Data.Product.Relation.Binary.Pointwise.NonDependent
19+
open import Level
20+
21+
private
22+
variable
23+
r s ℓr ℓs m m′ ℓm ℓm′ : Level
24+
25+
------------------------------------------------------------------------
26+
-- Bundles
27+
28+
leftSemimodule : {R : Semiring r ℓr} →
29+
LeftSemimodule R m ℓm →
30+
LeftSemimodule R m′ ℓm′ →
31+
LeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
32+
leftSemimodule M N = record
33+
{ _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_)
34+
; isLeftSemimodule = record
35+
{ +ᴹ-isCommutativeMonoid = CommutativeMonoid.isCommutativeMonoid
36+
(commutativeMonoid M.+ᴹ-commutativeMonoid N.+ᴹ-commutativeMonoid)
37+
; isPreleftSemimodule = record
38+
{ *ₗ-cong = λ where rr (mm , nn) → M.*ₗ-cong rr mm , N.*ₗ-cong rr nn
39+
; *ₗ-zeroˡ = λ where (m , n) → M.*ₗ-zeroˡ m , N.*ₗ-zeroˡ n
40+
; *ₗ-distribʳ = λ where
41+
(m , n) x y → M.*ₗ-distribʳ m x y , N.*ₗ-distribʳ n x y
42+
; *ₗ-identityˡ = λ where (m , n) → M.*ₗ-identityˡ m , N.*ₗ-identityˡ n
43+
; *ₗ-assoc = λ where x y (m , n) → M.*ₗ-assoc x y m , N.*ₗ-assoc x y n
44+
; *ₗ-zeroʳ = λ x → M.*ₗ-zeroʳ x , N.*ₗ-zeroʳ x
45+
; *ₗ-distribˡ = λ where
46+
x (m , n) (m′ , n′) → M.*ₗ-distribˡ x m m′ , N.*ₗ-distribˡ x n n′
47+
}
48+
}
49+
} where module M = LeftSemimodule M; module N = LeftSemimodule N
50+
51+
rightSemimodule : {R : Semiring r ℓr} →
52+
RightSemimodule R m ℓm →
53+
RightSemimodule R m′ ℓm′ →
54+
RightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
55+
rightSemimodule M N = record
56+
{ _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn
57+
; isRightSemimodule = record
58+
{ +ᴹ-isCommutativeMonoid = CommutativeMonoid.isCommutativeMonoid
59+
(commutativeMonoid M.+ᴹ-commutativeMonoid N.+ᴹ-commutativeMonoid)
60+
; isPrerightSemimodule = record
61+
{ *ᵣ-cong = λ where (mm , nn) rr → M.*ᵣ-cong mm rr , N.*ᵣ-cong nn rr
62+
; *ᵣ-zeroʳ = λ where (m , n) → M.*ᵣ-zeroʳ m , N.*ᵣ-zeroʳ n
63+
; *ᵣ-distribˡ = λ where
64+
(m , n) x y → M.*ᵣ-distribˡ m x y , N.*ᵣ-distribˡ n x y
65+
; *ᵣ-identityʳ = λ where (m , n) → M.*ᵣ-identityʳ m , N.*ᵣ-identityʳ n
66+
; *ᵣ-assoc = λ where
67+
(m , n) x y → M.*ᵣ-assoc m x y , N.*ᵣ-assoc n x y
68+
; *ᵣ-zeroˡ = λ x → M.*ᵣ-zeroˡ x , N.*ᵣ-zeroˡ x
69+
; *ᵣ-distribʳ = λ where
70+
x (m , n) (m′ , n′) → M.*ᵣ-distribʳ x m m′ , N.*ᵣ-distribʳ x n n′
71+
}
72+
}
73+
} where module M = RightSemimodule M; module N = RightSemimodule N
74+
75+
bisemimodule : {R : Semiring r ℓr} {S : Semiring s ℓs} →
76+
Bisemimodule R S m ℓm →
77+
Bisemimodule R S m′ ℓm′ →
78+
Bisemimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′)
79+
bisemimodule M N = record
80+
{ isBisemimodule = record
81+
{ +ᴹ-isCommutativeMonoid = CommutativeMonoid.isCommutativeMonoid
82+
(commutativeMonoid M.+ᴹ-commutativeMonoid N.+ᴹ-commutativeMonoid)
83+
; isPreleftSemimodule = LeftSemimodule.isPreleftSemimodule
84+
(leftSemimodule M.leftSemimodule N.leftSemimodule)
85+
; isPrerightSemimodule = RightSemimodule.isPrerightSemimodule
86+
(rightSemimodule M.rightSemimodule N.rightSemimodule)
87+
; *ₗ-*ᵣ-assoc = λ where
88+
x (m , n) y → M.*ₗ-*ᵣ-assoc x m y , N.*ₗ-*ᵣ-assoc x n y
89+
}
90+
} where module M = Bisemimodule M; module N = Bisemimodule N
91+
92+
semimodule : {R : CommutativeSemiring r ℓr} →
93+
Semimodule R m ℓm →
94+
Semimodule R m′ ℓm′ →
95+
Semimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
96+
semimodule M N = record
97+
{ isSemimodule = record
98+
{ isBisemimodule = Bisemimodule.isBisemimodule
99+
(bisemimodule M.bisemimodule N.bisemimodule)
100+
}
101+
} where module M = Semimodule M; module N = Semimodule N
102+
103+
leftModule : {R : Ring r ℓr} →
104+
LeftModule R m ℓm →
105+
LeftModule R m′ ℓm′ →
106+
LeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
107+
leftModule M N = record
108+
{ -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
109+
; isLeftModule = record
110+
{ isLeftSemimodule = LeftSemimodule.isLeftSemimodule
111+
(leftSemimodule M.leftSemimodule N.leftSemimodule)
112+
; -ᴹ‿cong = λ where (mm , nn) → M.-ᴹ‿cong mm , N.-ᴹ‿cong nn
113+
; -ᴹ‿inverse = λ where
114+
.proj₁ (m , n) → M.-ᴹ‿inverseˡ m , N.-ᴹ‿inverseˡ n
115+
.proj₂ (m , n) → M.-ᴹ‿inverseʳ m , N.-ᴹ‿inverseʳ n
116+
}
117+
} where module M = LeftModule M; module N = LeftModule N
118+
119+
rightModule : {R : Ring r ℓr} →
120+
RightModule R m ℓm →
121+
RightModule R m′ ℓm′ →
122+
RightModule R (m ⊔ m′) (ℓm ⊔ ℓm′)
123+
rightModule M N = record
124+
{ -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
125+
; isRightModule = record
126+
{ isRightSemimodule = RightSemimodule.isRightSemimodule
127+
(rightSemimodule M.rightSemimodule N.rightSemimodule)
128+
; -ᴹ‿cong = λ where (mm , nn) → M.-ᴹ‿cong mm , N.-ᴹ‿cong nn
129+
; -ᴹ‿inverse = λ where
130+
.proj₁ (m , n) → M.-ᴹ‿inverseˡ m , N.-ᴹ‿inverseˡ n
131+
.proj₂ (m , n) → M.-ᴹ‿inverseʳ m , N.-ᴹ‿inverseʳ n
132+
}
133+
} where module M = RightModule M; module N = RightModule N
134+
135+
bimodule : {R : Ring r ℓr} {S : Ring s ℓs} →
136+
Bimodule R S m ℓm →
137+
Bimodule R S m′ ℓm′ →
138+
Bimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′)
139+
bimodule M N = record
140+
{ -ᴹ_ = map M.-ᴹ_ N.-ᴹ_
141+
; isBimodule = record
142+
{ isBisemimodule = Bisemimodule.isBisemimodule
143+
(bisemimodule M.bisemimodule N.bisemimodule)
144+
; -ᴹ‿cong = λ where (mm , nn) → M.-ᴹ‿cong mm , N.-ᴹ‿cong nn
145+
; -ᴹ‿inverse = λ where
146+
.proj₁ (m , n) → M.-ᴹ‿inverseˡ m , N.-ᴹ‿inverseˡ n
147+
.proj₂ (m , n) → M.-ᴹ‿inverseʳ m , N.-ᴹ‿inverseʳ n
148+
}
149+
} where module M = Bimodule M; module N = Bimodule N
150+
151+
⟨module⟩ : {R : CommutativeRing r ℓr} →
152+
Module R m ℓm →
153+
Module R m′ ℓm′ →
154+
Module R (m ⊔ m′) (ℓm ⊔ ℓm′)
155+
⟨module⟩ M N = record
156+
{ isModule = record
157+
{ isBimodule = Bimodule.isBimodule (bimodule M.bimodule N.bimodule)
158+
}
159+
} where module M = Module M; module N = Module N

0 commit comments

Comments
 (0)