|
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
|
|
|
57 -- assuming Homomorphism is too strong
|
|
|
58 --
|
|
|
59 record NormalSubGroup {l c d : Level} (A : Group c d ) : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
|
|
|
60 open Group A
|
|
|
61 field
|
|
|
62 P : Carrier → Set l
|
|
|
63 Pε : P ε
|
|
|
64 P⁻¹ : (a : Carrier ) → P a → P (a ⁻¹)
|
|
|
65 P≈ : {a b : Carrier } → a ≈ b → P a → P b
|
|
|
66 P∙ : {a b : Carrier } → P a → P b → P ( a ∙ b )
|
|
|
67 -- gN ≈ Ng
|
|
|
68 Pcomm : {a b : Carrier } → P a → P ( b ∙ ( a ∙ b ⁻¹ ) )
|
|
|
69
|
|
|
70 import Relation.Binary.Reasoning.Setoid as EqReasoning
|
|
|
71
|
|
|
72 record Nelm {c d : Level} {A : Group c d } (n : NormalSubGroup {d} A) : Set (Level.suc c ⊔ d) where
|
|
|
73 open Group A
|
|
|
74 open NormalSubGroup n
|
|
|
75 field
|
|
|
76 elm : Carrier
|
|
|
77 Pelm : P elm
|
|
|
78
|
|
|
79 NGroup : {c d : Level} {A : Group c d } (n : NormalSubGroup A) → Group (Level.suc c ⊔ d) d
|
|
|
80 NGroup {_} {_} {A} n = record {
|
|
|
81 Carrier = Nelm n
|
|
|
82 ; _≈_ = λ x y → elm x ≈ elm y
|
|
|
83 ; _∙_ = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) }
|
|
|
84 ; ε = record { elm = ε ; Pelm = Pε }
|
|
|
85 ; _⁻¹ = λ x → record { elm = (elm x) ⁻¹ ; Pelm = P⁻¹ (elm x) (Pelm x) }
|
|
|
86 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
|
|
|
87 isEquivalence = record { refl = IsEquivalence.refl (IsGroup.isEquivalence ga)
|
|
|
88 ; sym = IsEquivalence.sym (IsGroup.isEquivalence ga)
|
|
|
89 ; trans = IsEquivalence.trans (IsGroup.isEquivalence ga) }
|
|
|
90 ; ∙-cong = IsGroup.∙-cong ga }
|
|
|
91 ; assoc = λ a b c → IsGroup.assoc ga (elm a) (elm b) (elm c) }
|
|
|
92 ; identity = ( (λ q → proj₁ (IsGroup.identity ga) (elm q)) , (λ q → proj₂ (IsGroup.identity ga) (elm q)) ) }
|
|
|
93 ; inverse = ( (λ q → proj₁ (IsGroup.inverse ga) (elm q)) , (λ q → proj₂ (IsGroup.inverse ga) (elm q)) )
|
|
|
94 ; ⁻¹-cong = IsGroup.⁻¹-cong ga }
|
|
|
95 } where
|
|
|
96 open Group A
|
|
|
97 open NormalSubGroup n
|
|
|
98 open Nelm
|
|
|
99 ga = Group.isGroup A
|
|
|
100
|
|
|
101
|
