Skip to content

Commit 46d8280

Browse files
jamesmckinnajamesmckinna
committed
add: Centre of an algebra, following agda#2863 
1 parent 4b50bf3 commit 46d8280

5 files changed

Lines changed: 279 additions & 0 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,10 @@ Deprecated names
7979
New modules
8080
-----------
8181

82+
* `Algebra.Construct.Centre.X` for the definition of the centre of an algebra,
83+
where `X = {Semigroup|Monoid|Group}`, based on an underlying type defined in
84+
`Algebra.Construct.Centre`.
85+
8286
* `Algebra.Construct.Sub.Group` for the definition of subgroups.
8387

8488
* `Algebra.Module.Construct.Sub.Bimodule` for the definition of subbimodules.

‎src/Algebra/Construct/Centre/Center.agda‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definition of the centre as a subtype of (the carrier of) a raw magma
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Core using (Op₂)
10+
open import Relation.Binary.Core using (Rel)
11+
12+
module Algebra.Construct.Centre.Center
13+
{c ℓ} {Carrier : Set c} (_∼_ : Rel Carrier ℓ) (_∙_ : Op₂ Carrier)
14+
where
15+
16+
open import Algebra.Definitions _∼_ using (Central)
17+
open import Function.Base using (id; _on_)
18+
open import Level using (_⊔_)
19+
open import Relation.Binary.Morphism.Structures
20+
using (IsRelHomomorphism; IsRelMonomorphism)
21+
22+
23+
------------------------------------------------------------------------
24+
-- Definitions
25+
26+
record Center : Set (c ⊔ ℓ) where
27+
field
28+
ι : Carrier
29+
central : Central _∙_ ι
30+
31+
open Center public
32+
using (ι)
33+
34+
∙-comm : ∀ g h → (ι g ∙ ι h) ∼ (ι h ∙ ι g)
35+
∙-comm g h = Center.central g (ι h)
36+
37+
-- Center as subtype of Carrier
38+
39+
_≈_ : Rel Center _
40+
_≈_ = _∼_ on ι
41+
42+
isRelHomomorphism : IsRelHomomorphism _≈_ _∼_ ι
43+
isRelHomomorphism = record { cong = id }
44+
45+
isRelMonomorphism : IsRelMonomorphism _≈_ _∼_ ι
46+
isRelMonomorphism = record
47+
{ isHomomorphism = isRelHomomorphism
48+
; injective = id
49+
}

‎src/Algebra/Construct/Centre/Group.agda‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definition of the centre of an Algebra
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles
10+
using (Group; AbelianGroup; RawMonoid; RawGroup)
11+
12+
module Algebra.Construct.Centre.Group {c ℓ} (group : Group c ℓ) where
13+
14+
open import Algebra.Core using (Op₁)
15+
open import Algebra.Morphism.Structures
16+
open import Algebra.Morphism.GroupMonomorphism using (isGroup)
17+
open import Function.Base using (id; const; _$_)
18+
19+
20+
private
21+
module G = Group group
22+
23+
open import Relation.Binary.Reasoning.Setoid G.setoid as ≈-Reasoning
24+
open import Algebra.Properties.Group group using (∙-cancelʳ)
25+
26+
27+
------------------------------------------------------------------------
28+
-- Definition
29+
30+
-- Re-export the underlying sub-Monoid
31+
32+
open import Algebra.Construct.Centre.Monoid G.monoid as Z public
33+
using (Center; ι; ∙-comm)
34+
35+
-- Now, can define a commutative sub-Group
36+
37+
_⁻¹ : Op₁ Center
38+
g ⁻¹ = record
39+
{ ι = ι g G.⁻¹
40+
; central = λ k → ∙-cancelʳ (ι g) _ _ $ begin
41+
(ι g G.⁻¹ G.∙ k) G.∙ (ι g) ≈⟨ G.assoc _ _ _ ⟩
42+
ι g G.⁻¹ G.∙ (k G.∙ ι g) ≈⟨ G.∙-congˡ $ Center.central g k ⟨
43+
ι g G.⁻¹ G.∙ (ι g G.∙ k) ≈⟨ G.assoc _ _ _ ⟨
44+
(ι g G.⁻¹ G.∙ ι g) G.∙ k ≈⟨ G.∙-congʳ $ G.inverseˡ _ ⟩
45+
G.ε G.∙ k ≈⟨ Center.central Z.ε k ⟩
46+
k G.∙ G.ε ≈⟨ G.∙-congˡ $ G.inverseˡ _ ⟨
47+
k G.∙ (ι g G.⁻¹ G.∙ ι g) ≈⟨ G.assoc _ _ _ ⟨
48+
(k G.∙ ι g G.⁻¹) G.∙ (ι g) ∎
49+
} where open ≈-Reasoning
50+
51+
domain : RawGroup _ _
52+
domain = record { RawMonoid Z.domain; _⁻¹ = _⁻¹ }
53+
54+
isGroupHomomorphism : IsGroupHomomorphism domain G.rawGroup ι
55+
isGroupHomomorphism = record
56+
{ isMonoidHomomorphism = Z.isMonoidHomomorphism
57+
; ⁻¹-homo = λ _ → G.refl
58+
}
59+
60+
isGroupMonomorphism : IsGroupMonomorphism domain G.rawGroup ι
61+
isGroupMonomorphism = record
62+
{ isGroupHomomorphism = isGroupHomomorphism
63+
; injective = id
64+
}
65+
66+
abelianGroup : AbelianGroup _ _
67+
abelianGroup = record
68+
{ isAbelianGroup = record
69+
{ isGroup = isGroup isGroupMonomorphism G.isGroup
70+
; comm = ∙-comm
71+
}
72+
}
73+
74+
Z[_] = abelianGroup
75+
76+
{-
77+
normalSubgroup : NormalSubgroup _ _
78+
normalSubgroup = record
79+
{ subgroup = record { ι-isGroupMonomorphism = isGroupMonomorphism }
80+
; normal = record
81+
{ conjugate = const
82+
; normal = Center.central
83+
}
84+
}
85+
-}

‎src/Algebra/Construct/Centre/Monoid.agda‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definition of the centre of an Monoid
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles
10+
using (Monoid; CommutativeMonoid; RawMagma; RawMonoid)
11+
12+
module Algebra.Construct.Centre.Monoid
13+
{c ℓ} (monoid : Monoid c ℓ)
14+
where
15+
16+
open import Algebra.Consequences.Setoid using (identity⇒central)
17+
open import Algebra.Morphism.Structures
18+
open import Algebra.Morphism.MonoidMonomorphism using (isMonoid)
19+
open import Function.Base using (id)
20+
21+
private
22+
module G = Monoid monoid
23+
24+
25+
------------------------------------------------------------------------
26+
-- Definition
27+
28+
-- Re-export the underlying sub-Semigroup
29+
30+
open import Algebra.Construct.Centre.Semigroup G.semigroup as Z public
31+
using (Center; ι; ∙-comm)
32+
33+
-- Now, can define a sub-Monoid
34+
35+
ε : Center
36+
ε = record
37+
{ ι = G.ε
38+
; central = identity⇒central G.setoid {_∙_ = G._∙_} G.identity
39+
}
40+
41+
domain : RawMonoid _ _
42+
domain = record { RawMagma Z.domain; ε = ε }
43+
44+
isMonoidHomomorphism : IsMonoidHomomorphism domain G.rawMonoid ι
45+
isMonoidHomomorphism = record
46+
{ isMagmaHomomorphism = Z.isMagmaHomomorphism
47+
; ε-homo = G.refl
48+
}
49+
50+
isMonoidMonomorphism : IsMonoidMonomorphism domain G.rawMonoid ι
51+
isMonoidMonomorphism = record
52+
{ isMonoidHomomorphism = isMonoidHomomorphism
53+
; injective = id
54+
}
55+
56+
-- And hence a CommutativeMonoid
57+
58+
commutativeMonoid : CommutativeMonoid _ _
59+
commutativeMonoid = record
60+
{ isCommutativeMonoid = record
61+
{ isMonoid = isMonoid isMonoidMonomorphism G.isMonoid
62+
; comm = ∙-comm
63+
}
64+
}
65+
66+
Z[_] = commutativeMonoid

‎src/Algebra/Construct/Centre/Semigroup.agda‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definition of the centre of an Semigroup
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles
10+
using (Semigroup; CommutativeSemigroup; RawMagma)
11+
12+
module Algebra.Construct.Centre.Semigroup
13+
{c ℓ} (semigroup : Semigroup c ℓ)
14+
where
15+
16+
open import Algebra.Core using (Op₂)
17+
open import Algebra.Morphism.MagmaMonomorphism using (isSemigroup)
18+
open import Algebra.Morphism.Structures
19+
open import Function.Base using (id; _$_)
20+
21+
private
22+
module G = Semigroup semigroup
23+
24+
open import Relation.Binary.Reasoning.Setoid G.setoid as ≈-Reasoning
25+
26+
27+
------------------------------------------------------------------------
28+
-- Definition
29+
30+
-- Re-export the underlying subtype
31+
32+
open import Algebra.Construct.Centre.Center G._≈_ G._∙_ as Z public
33+
using (Center; ι; ∙-comm)
34+
35+
-- Now, by associativity, a sub-Magma is definable
36+
37+
_∙_ : Op₂ Center
38+
g ∙ h = record
39+
{ ι = ι g G.∙ ι h
40+
; central = λ k → begin
41+
(ι g G.∙ ι h) G.∙ k ≈⟨ G.assoc _ _ _ ⟩
42+
ι g G.∙ (ι h G.∙ k) ≈⟨ G.∙-congˡ $ Center.central h k ⟩
43+
ι g G.∙ (k G.∙ ι h) ≈⟨ G.assoc _ _ _ ⟨
44+
ι g G.∙ k G.∙ ι h ≈⟨ G.∙-congʳ $ Center.central g k ⟩
45+
k G.∙ ι g G.∙ ι h ≈⟨ G.assoc _ _ _ ⟩
46+
k G.∙ (ι g G.∙ ι h) ∎
47+
} where open ≈-Reasoning
48+
49+
domain : RawMagma _ _
50+
domain = record {_≈_ = Z._≈_; _∙_ = _∙_ }
51+
52+
isMagmaHomomorphism : IsMagmaHomomorphism domain G.rawMagma ι
53+
isMagmaHomomorphism = record
54+
{ isRelHomomorphism = Z.isRelHomomorphism
55+
; homo = λ _ _ → G.refl
56+
}
57+
58+
isMagmaMonomorphism : IsMagmaMonomorphism domain G.rawMagma ι
59+
isMagmaMonomorphism = record
60+
{ isMagmaHomomorphism = isMagmaHomomorphism
61+
; injective = id
62+
}
63+
64+
-- And hence a CommutativeSemigroup
65+
66+
commutativeSemigroup : CommutativeSemigroup _ _
67+
commutativeSemigroup = record
68+
{ isCommutativeSemigroup = record
69+
{ isSemigroup = isSemigroup isMagmaMonomorphism G.isSemigroup
70+
; comm = ∙-comm
71+
}
72+
}
73+
74+
Z[_] = commutativeSemigroup
75+

0 commit comments

Comments
 (0)