Skip to content

Commit f702f82

Browse files
jamesmckinnajamesmckinna
committed
refactor: alternative to agda#2852 and agda#2854 
1 parent e2ff677 commit f702f82

File tree

5 files changed

+272
-0
lines changed

5 files changed

+272
-0
lines changed

‎src/Algebra/Construct/Quotient/AbelianGroup.agda‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Quotient Abelian groups
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles using (Group; AbelianGroup)
10+
import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup
11+
12+
module Algebra.Construct.Quotient.AbelianGroup
13+
{c ℓ} (G : AbelianGroup c ℓ)
14+
(open AbelianSubgroup G using (Subgroup; normalSubgroup))
15+
{c′ ℓ′} (N : Subgroup c′ ℓ′)
16+
where
17+
18+
private
19+
module G = AbelianGroup G
20+
21+
-- Re-export the quotient group
22+
23+
open import Algebra.Construct.Quotient.Group G.group (normalSubgroup N) public
24+
25+
-- With its additional bundle
26+
27+
quotientAbelianGroup : AbelianGroup c _
28+
quotientAbelianGroup = record
29+
{ isAbelianGroup = record
30+
{ isGroup = isGroup
31+
; comm = λ g h → ≈⇒≋ (G.comm g h)
32+
}
33+
} where open Group quotientGroup
34+
35+
-- Public re-exports, as needed?

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

Lines changed: 126 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,126 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Quotient groups
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles using (Group)
10+
open import Algebra.Construct.Sub.Group.Normal using (NormalSubgroup)
11+
12+
module Algebra.Construct.Quotient.Group
13+
{c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where
14+
15+
open import Algebra.Definitions using (Congruent₁; Congruent₂)
16+
open import Algebra.Morphism.Structures
17+
using (IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism)
18+
open import Data.Product.Base using (_,_)
19+
open import Function.Base using (_∘_)
20+
open import Function.Definitions using (Surjective)
21+
open import Level using (_⊔_)
22+
open import Relation.Binary.Core using (_⇒_)
23+
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
24+
25+
private
26+
open module G = Group G
27+
28+
open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
29+
open import Algebra.Properties.Monoid monoid
30+
open import Relation.Binary.Reasoning.Setoid setoid
31+
32+
private
33+
open module N = NormalSubgroup N
34+
using (ι; module ι; conjugate; normal)
35+
36+
infix 0 _by_
37+
38+
data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
39+
_by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y
40+
41+
≈⇒≋ : _≈_ ⇒ _≋_
42+
≈⇒≋ x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ _)
43+
44+
≋-refl : Reflexive _≋_
45+
≋-refl = ≈⇒≋ refl
46+
47+
≋-sym : Symmetric _≋_
48+
≋-sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin
49+
ι (g N.⁻¹) ∙ y ≈⟨ ∙-cong (ι.⁻¹-homo g) (sym ιg∙x≈y) ⟩
50+
ι g ⁻¹ ∙ (ι g ∙ x) ≈⟨ cancelˡ (inverseˡ (ι g)) x ⟩
51+
x ∎
52+
53+
≋-trans : Transitive _≋_
54+
≋-trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin
55+
ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩
56+
(ι h ∙ ι g) ∙ x ≈⟨ uv≈w⇒xu∙v≈xw ιg∙x≈y (ι h) ⟩
57+
ι h ∙ y ≈⟨ ιh∙y≈z ⟩
58+
z ∎
59+
60+
≋-∙-cong : Congruent₂ _≋_ _∙_
61+
≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin
62+
ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩
63+
(ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x) (ι g) u ⟩
64+
(ι g ∙ x) ∙ (ι h ∙ u) ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩
65+
y ∙ v ∎
66+
where h′ = conjugate h x
67+
68+
≋-⁻¹-cong : Congruent₁ _≋_ _⁻¹
69+
≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin
70+
ι h ∙ x ⁻¹ ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩
71+
x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩
72+
x ⁻¹ ∙ ι g ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨
73+
(ι g ∙ x) ⁻¹ ≈⟨ ⁻¹-cong ιg∙x≈y ⟩
74+
y ⁻¹ ∎
75+
where h = conjugate (g N.⁻¹) (x ⁻¹)
76+
77+
quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
78+
quotientGroup = record
79+
{ isGroup = record
80+
{ isMonoid = record
81+
{ isSemigroup = record
82+
{ isMagma = record
83+
{ isEquivalence = record
84+
{ refl = ≋-refl
85+
; sym = ≋-sym
86+
; trans = ≋-trans
87+
}
88+
; ∙-cong = ≋-∙-cong
89+
}
90+
; assoc = λ x y z → ≈⇒≋ (assoc x y z)
91+
}
92+
; identity = ≈⇒≋ ∘ identityˡ , ≈⇒≋ ∘ identityʳ
93+
}
94+
; inverse = ≈⇒≋ ∘ inverseˡ , ≈⇒≋ ∘ inverseʳ
95+
; ⁻¹-cong = ≋-⁻¹-cong
96+
}
97+
}
98+
99+
_/_ : Group c (c ⊔ ℓ ⊔ c′)
100+
_/_ = quotientGroup
101+
102+
π : Group.Carrier G → Group.Carrier quotientGroup
103+
π x = x -- because we do all the work in the relation
104+
105+
π-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) π
106+
π-isMagmaHomomorphism = record
107+
{ isRelHomomorphism = record
108+
{ cong = ≈⇒≋
109+
}
110+
; homo = λ _ _ → ≋-refl
111+
}
112+
113+
π-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) π
114+
π-isMonoidHomomorphism = record
115+
{ isMagmaHomomorphism = π-isMagmaHomomorphism
116+
; ε-homo = ≋-refl
117+
}
118+
119+
π-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π
120+
π-isGroupHomomorphism = record
121+
{ isMonoidHomomorphism = π-isMonoidHomomorphism
122+
; ⁻¹-homo = λ _ → ≋-refl
123+
}
124+
125+
π-surjective : Surjective _≈_ _≋_ π
126+
π-surjective g = g , ≈⇒≋

‎src/Algebra/Construct/Sub/AbelianGroup.agda‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Subgroups of Abelian groups: necessarily Normal
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles using (AbelianGroup)
10+
11+
module Algebra.Construct.Sub.AbelianGroup {c ℓ} (G : AbelianGroup c ℓ) where
12+
13+
open import Algebra.Morphism.GroupMonomorphism using (isAbelianGroup)
14+
15+
private
16+
module G = AbelianGroup G
17+
18+
open import Algebra.Construct.Sub.Group.Normal G.group
19+
using (IsNormal; NormalSubgroup)
20+
21+
-- Re-export the notion of subgroup of the underlying Group
22+
23+
open import Algebra.Construct.Sub.Group G.group public
24+
using (Subgroup)
25+
26+
-- Then, for any such Subgroup:
27+
-- * it defines an AbelianGroup
28+
-- * and is, in fact, Normal
29+
30+
module _ {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) where
31+
32+
open Subgroup subgroup public
33+
using (ι; ι-monomorphism)
34+
35+
abelianGroup : AbelianGroup c′ ℓ′
36+
abelianGroup = record
37+
{ isAbelianGroup = isAbelianGroup ι-monomorphism G.isAbelianGroup }
38+
39+
open AbelianGroup abelianGroup public
40+
41+
isNormal : IsNormal subgroup
42+
isNormal = record { normal = λ n → G.comm (ι n) }
43+
44+
normalSubgroup : NormalSubgroup c′ ℓ′
45+
normalSubgroup = record { isNormal = isNormal }
46+
47+
open NormalSubgroup normalSubgroup public
48+
using (conjugate; normal)

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

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definition of subgroup via Group monomorphism
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles using (Group; RawGroup)
10+
11+
module Algebra.Construct.Sub.Group {c ℓ} (G : Group c ℓ) where
12+
13+
open import Algebra.Morphism.Structures using (IsGroupMonomorphism)
14+
open import Algebra.Morphism.GroupMonomorphism using (isGroup)
15+
open import Level using (suc; _⊔_)
16+
17+
private
18+
module G = Group G
19+
20+
record Subgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
21+
field
22+
domain : RawGroup c′ ℓ′
23+
ι : _ → G.Carrier
24+
ι-monomorphism : IsGroupMonomorphism domain G.rawGroup ι
25+
26+
module ι = IsGroupMonomorphism ι-monomorphism
27+
28+
group : Group _ _
29+
group = record { isGroup = isGroup ι-monomorphism G.isGroup }
30+
31+
open Group group public

‎src/Algebra/Construct/Sub/Group/Normal.agda‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Definition of normal subgroups
5+
------------------------------------------------------------------------
6+
7+
{-# OPTIONS --safe --cubical-compatible #-}
8+
9+
open import Algebra.Bundles using (Group)
10+
11+
module Algebra.Construct.Sub.Group.Normal {c ℓ} (G : Group c ℓ) where
12+
13+
open import Algebra.Construct.Sub.Group G using (Subgroup)
14+
open import Level using (suc; _⊔_)
15+
16+
private
17+
module G = Group G
18+
19+
-- every element of the subgroup commutes in G
20+
record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where
21+
open Subgroup subgroup using (ι)
22+
field
23+
conjugate : ∀ n g → _
24+
normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n
25+
26+
record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
27+
field
28+
subgroup : Subgroup c′ ℓ′
29+
isNormal : IsNormal subgroup
30+
31+
open Subgroup subgroup public
32+
open IsNormal isNormal public

0 commit comments

Comments
 (0)