|
302
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 open import Level hiding ( suc ; zero )
|
|
|
3 module NormalSubgroup where
|
|
|
4
|
|
|
5 open import Algebra
|
|
|
6 open import Algebra.Structures
|
|
|
7 open import Algebra.Definitions
|
|
|
8 open import Data.Product
|
|
|
9 open import Relation.Binary.PropositionalEquality
|
|
|
10 open import Algebra.Morphism.Structures
|
|
|
11 open import Data.Empty
|
|
|
12 open import Relation.Nullary
|
|
|
13
|
|
|
14 open GroupMorphisms
|
|
|
15
|
|
|
16 GR : {c l : Level } → Group c l → RawGroup c l
|
|
|
17 GR G = record {
|
|
|
18 Carrier = Carrier G
|
|
|
19 ; _≈_ = _≈_ G
|
|
|
20 ; _∙_ = _∙_ G
|
|
|
21 ; ε = ε G
|
|
|
22 ; _⁻¹ = _⁻¹ G
|
|
|
23 } where open Group
|
|
|
24
|
|
|
25 record GAxiom {c l : Level } (G : Group c l) : Set ( c Level.⊔ l ) where
|
|
|
26 open Group G
|
|
|
27 field
|
|
|
28 ∙-cong : {x y u v : Carrier } → x ≈ y → u ≈ v → x ∙ u ≈ y ∙ v
|
|
|
29 assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈ x ∙ ( y ∙ z )
|
|
|
30 identity : ((y : Carrier) → ε ∙ y ≈ y ) × ((y : Carrier) → y ∙ ε ≈ y )
|
|
|
31 inverse : ((y : Carrier) → y ⁻¹ ∙ y ≈ ε ) × ((y : Carrier) → y ∙ y ⁻¹ ≈ ε )
|
|
|
32 ⁻¹-cong : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹
|
|
|
33
|
|
|
34 GA : {c l : Level } → (G : Group c l) → GAxiom G
|
|
|
35 GA G = record {
|
|
|
36 ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)))
|
|
|
37 ; assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))
|
|
|
38 ; identity = IsMonoid.identity ( IsGroup.isMonoid isGroup)
|
|
|
39 ; inverse = IsGroup.inverse isGroup
|
|
|
40 ; ⁻¹-cong = IsGroup.⁻¹-cong isGroup
|
|
|
41 } where open Group G
|
|
|
42
|
|
|
43 open import Relation.Binary.Structures
|
|
|
44
|
|
|
45 Eq : {c l : Level } → (G : Group c l) → IsEquivalence _
|
|
|
46 Eq G = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
|
|
|
47 (IsGroup.isMonoid (Group.isGroup G ))) )
|
|
|
48
|
|
|
49 _<_∙_> : {c d : Level} (m : Group c d ) → Group.Carrier m → Group.Carrier m → Group.Carrier m
|
|
|
50 m < x ∙ y > = Group._∙_ m x y
|
|
|
51
|
|
|
52 _<_≈_> : {c d : Level} (m : Group c d ) → (f g : Group.Carrier m ) → Set d
|
|
|
53 m < x ≈ y > = Group._≈_ m x y
|
|
|
54
|
|
|
55 infixr 9 _<_∙_>
|
|
|
56
|
|
307
|
57 record SubGroup {l c d : Level} (A : Group c d ) : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
|
|
302
|
58 open Group A
|
|
|
59 field
|
|
|
60 P : Carrier → Set l
|
|
|
61 Pε : P ε
|
|
|
62 P⁻¹ : (a : Carrier ) → P a → P (a ⁻¹)
|
|
|
63 P≈ : {a b : Carrier } → a ≈ b → P a → P b
|
|
|
64 P∙ : {a b : Carrier } → P a → P b → P ( a ∙ b )
|
|
307
|
65
|
|
|
66 -- assuming Homomorphism is too strong
|
|
|
67 --
|
|
|
68 record NormalSubGroup {l c d : Level} (A : Group c d ) : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
|
|
|
69 open Group A
|
|
|
70 field
|
|
|
71 Psub : SubGroup {l} A
|
|
302
|
72 -- gN ≈ Ng
|
|
307
|
73 Pcomm : {a b : Carrier } → SubGroup.P Psub a → SubGroup.P Psub ( b ∙ ( a ∙ b ⁻¹ ) )
|
|
|
74 P : Carrier → Set l
|
|
|
75 P = SubGroup.P Psub
|
|
|
76 Pε : P ε
|
|
|
77 Pε = SubGroup.Pε Psub
|
|
|
78 P⁻¹ : (a : Carrier ) → P a → P (a ⁻¹)
|
|
|
79 P⁻¹ = SubGroup.P⁻¹ Psub
|
|
|
80 P≈ : {a b : Carrier } → a ≈ b → P a → P b
|
|
|
81 P≈ = SubGroup.P≈ Psub
|
|
|
82 P∙ : {a b : Carrier } → P a → P b → P ( a ∙ b )
|
|
|
83 P∙ = SubGroup.P∙ Psub
|
|
302
|
84
|
|
|
85 import Relation.Binary.Reasoning.Setoid as EqReasoning
|
|
|
86
|
|
307
|
87 record Nelm {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) : Set (Level.suc e ⊔ (Level.suc c ⊔ d)) where
|
|
302
|
88 open Group A
|
|
307
|
89 open SubGroup n
|
|
302
|
90 field
|
|
|
91 elm : Carrier
|
|
|
92 Pelm : P elm
|
|
|
93
|
|
307
|
94 SGroup : {c d e : Level} (A : Group c d ) (n : SubGroup {e} A) → Group (Level.suc e ⊔ (Level.suc c ⊔ d)) d
|
|
|
95 SGroup {_} {_} {_} A n = record {
|
|
|
96 Carrier = Nelm A n
|
|
302
|
97 ; _≈_ = λ x y → elm x ≈ elm y
|
|
|
98 ; _∙_ = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) }
|
|
|
99 ; ε = record { elm = ε ; Pelm = Pε }
|
|
|
100 ; _⁻¹ = λ x → record { elm = (elm x) ⁻¹ ; Pelm = P⁻¹ (elm x) (Pelm x) }
|
|
|
101 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
|
|
|
102 isEquivalence = record { refl = IsEquivalence.refl (IsGroup.isEquivalence ga)
|
|
|
103 ; sym = IsEquivalence.sym (IsGroup.isEquivalence ga)
|
|
|
104 ; trans = IsEquivalence.trans (IsGroup.isEquivalence ga) }
|
|
|
105 ; ∙-cong = IsGroup.∙-cong ga }
|
|
|
106 ; assoc = λ a b c → IsGroup.assoc ga (elm a) (elm b) (elm c) }
|
|
|
107 ; identity = ( (λ q → proj₁ (IsGroup.identity ga) (elm q)) , (λ q → proj₂ (IsGroup.identity ga) (elm q)) ) }
|
|
|
108 ; inverse = ( (λ q → proj₁ (IsGroup.inverse ga) (elm q)) , (λ q → proj₂ (IsGroup.inverse ga) (elm q)) )
|
|
|
109 ; ⁻¹-cong = IsGroup.⁻¹-cong ga }
|
|
|
110 } where
|
|
|
111 open Group A
|
|
307
|
112 open SubGroup n
|
|
302
|
113 open Nelm
|
|
|
114 ga = Group.isGroup A
|
|
|
115
|
|
|
116
|
