Mercurial > hg > Members > kono > Proof > galois

changeset 264:c4458b479a0f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 31 May 2022 08:47:46 +0900
parents 93a2a2c2d7c0
children 1dbe1f357569
files src/Fundamental.agda src/FundamentalHomomorphism.agda src/Gutil0.agda
diffstat 3 files changed, 265 insertions(+), 192 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Fundamental.agda	Tue May 31 08:47:46 2022 +0900
@@ -0,0 +1,167 @@
+-- fundamental homomorphism theorem
+--
+
+open import Level hiding ( suc ; zero )
+module Fundamental (c l : Level) where
+
+open import Algebra
+open import Algebra.Structures
+open import Algebra.Definitions
+open import Data.Product
+open import Relation.Binary.PropositionalEquality 
+open import Algebra.Morphism.Structures 
+open GroupMorphisms
+open import Gutil0
+
+--
+-- Given two groups G and H and a group homomorphism f : G → H,
+-- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K
+-- (where G/K is the quotient group of G by K).
+-- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ.
+--     https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms
+--
+--       f
+--    G --→ H
+--    |   /
+--  φ |  / h
+--    ↓ /
+--    G/K
+--
+
+-- open import Relation.Binary.Structures
+-- open import Relation.Binary.Morphism.Structures
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+
+open HomoMorphism
+
+--
+--  Coset : N : NormalSubGroup →  { a ∙ n | G ∋ a , N ∋ n }
+--
+
+data Coset (G : Group c l)  (K : NormalSubGroup G) :  Group.Carrier G → Set ( c  Level.⊔  l ) where
+    coset  : (a b : Group.Carrier G ) → Coset G K ( Group._∙_ G a (NormalSubGroup.sub K b) )
+    cscong : {a b : Group.Carrier G } → Group._≈_ G a b  → Coset G K a → Coset G K b
+
+open NormalSubGroup  -- G has at least an element other than ε
+-- open import Relation.Binary.Structures
+
+φ :   {G : Group c l} →  {K : NormalSubGroup G} → (g x : Group.Carrier G ) → Coset G K x
+φ {G} {K} g x = cscong p01 ( coset (x ∙ (sub K g) ⁻¹ )  g)  where
+   open Group G
+   p01 : x ∙ sub K g ⁻¹ ∙ sub K g ≈ x
+   p01 = begin x ∙ sub K g ⁻¹ ∙ sub K g ≈⟨ assoc x _ _  ⟩
+         x ∙ (  sub K g ⁻¹ ∙ sub K g ) ≈⟨  ∙-cong (grefl G) (proj₁ inverse  _ ) ⟩
+         x ∙ ε ≈⟨ proj₂ identity  _  ⟩
+         x   ∎ where open EqReasoning (Algebra.Group.setoid G )
+
+base :  {G : Group c l}  {K : NormalSubGroup G} → ( (g : Group.Carrier G )→ Coset G K g)  → Group.Carrier G
+base {G} {K} x = base1 (x ε) where     -- with x ε won't work why?
+    open Group G
+    base1 : {x : Carrier} → Coset G K x → Carrier 
+    base1 (coset a b) = a ⁻¹ ∙ b 
+    base1 (cscong x y) = base1 y
+
+--  Na ∙ Nb = Nab
+mul : {G : Group c l}  {K : NormalSubGroup G} → (x y : (g : Group.Carrier G ) → Coset G K g ) → (g : Group.Carrier G ) → Coset G K g
+mul {G} {K} x y g = φ (base x ∙ base y) g where open Group G
+
+-- ceq : {G : Group c l } {K : NormalSubGroup G}  → {a b : Group.Carrier G } → (x : Coset G K a) (y : Coset G K b) → Set l
+-- ceq {G} {K} (coset a b) (coset a₁ b₁) = Group._≈_ G (sub K b ) (sub K b₁)
+-- ceq (coset a b) (cscong eq y) = ceq (coset a b) y
+-- ceq (cscong eq x) (coset a b) = ceq x (coset a b)
+-- ceq (cscong eqx x) (cscong eqy y) = ceq x y
+
+-- _==_ : {G : Group c l}  {K : NormalSubGroup G} → (x y : (g : Group.Carrier G ) → Coset G K g ) → Set l
+-- _==_ {G}  {K} x y = ceq (x ε) (y ε) where open Group G
+
+inv : {G : Group c l}  {K : NormalSubGroup G} → ( (g : Group.Carrier G )→ Coset G K g)  → ( (g : Group.Carrier G )→ Coset G K g)
+inv {G} {K} x g = inv1 (x g) where
+    open Group G
+    inv1 : {a : Carrier} → (x : Coset G K a) → Coset G K g
+    inv1 (coset a b) = φ  (a ⁻¹) g 
+    inv1 (cscong eq x) = inv1 x
+
+COSET : (G : Group c l)  (K : NormalSubGroup G) →  Set ( c  Level.⊔  l )
+COSET G K = (g : Group.Carrier G ) → Coset G K g
+
+-- import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+-- open HE
+
+-- G / K : Quotient
+_/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) ( c  Level.⊔  l )
+G / K = record {
+     Carrier        = (g : Group.Carrier G ) → Coset G K g
+     ; _≈_          = λ x y → x ≡ y
+     ; _∙_          = λ x y → mul x y
+     ; ε            = φ (Group.ε G )
+     ; _⁻¹          = λ x → inv x
+     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
+       isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 
+       ; ∙-cong = λ {x y u v} → cresp }
+       ; assoc = {!!} }
+       ; identity = {!!} }
+       ; inverse   = {!!}
+       ; ⁻¹-cong   = λ {x} {y} → {!!}
+      } 
+   } where 
+      open Group G hiding (refl ; sym ; trans )
+      open EqReasoning (Algebra.Group.setoid G)
+      open IsGroupHomomorphism (s-homo K )
+      cresp : {x y u v : COSET G K} → x ≡ y → u ≡ v → mul x u ≡ mul y v
+      cresp {x} {y} {u} {v} refl refl = refl
+      assoc1 : {x y z  : COSET G K} → mul x ( mul y z ) ≡ mul (mul x y ) z
+      assoc1 = {!!}
+        -- crefl1 (coset a b) = ⟦⟧-cong (grefl G) 
+
+-- K ⊂ ker(f)
+K⊆ker : (G H : Group c l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
+K⊆ker G H K f = (x : Group.Carrier G ) → f ( sub K x ) ≈ ε   where
+  open Group H
+
+record FundamentalHomomorphism (G H : Group c l)  
+    (f : Group.Carrier G → Group.Carrier H ) 
+    (homo : IsGroupHomomorphism (GR G) (GR H) f ) 
+    (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set ( c  Level.⊔  l ) where
+  open Group H
+  field
+    h : {!!} → Group.Carrier H
+    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) {!!} 
+    unique : (x : Group.Carrier G)  →  {!!} -- f x ≈ h ( φ x )
+
+FundamentalHomomorphismTheorm : (G H : Group c l)
+    (f : Group.Carrier G → Group.Carrier H )
+    (homo : IsGroupHomomorphism (GR G) (GR H) f )
+    (K : NormalSubGroup G ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f homo K kf
+FundamentalHomomorphismTheorm G H f homo K kf = record {
+     h = h
+   ; h-homo = h-homo
+   ; unique = unique
+  } where
+    open Group H
+    EqH =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
+             (IsGroup.isMonoid isGroup )))
+    EqG =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
+             (IsGroup.isMonoid (Group.isGroup G) )))
+    h1 : {x : Group.Carrier G } → Coset G K x → Carrier
+    h1 (coset a b) = f a 
+    h : {!!} -- CosetCarrier G K → Carrier   --  G / K → H
+    h r = {!!}
+    _o_ = Group._∙_ G
+    h03 : (x y : Group.Carrier (G / K ) ) → {!!}
+    h03 x y = {!!} 
+    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) {!!} 
+    h-homo = record {
+     isMonoidHomomorphism = record {
+          isMagmaHomomorphism = record {
+             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } 
+           ; homo = h03 }
+        ; ε-homo = {!!} }
+       ; ⁻¹-homo = {!!} }
+    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
+    unique x = begin
+         f x ≈⟨ {!!} ⟩
+         f ( x o (Group._⁻¹ G (sub K x)))   ∎ where open EqReasoning (Algebra.Group.setoid H )
+
+
+
+
--- a/src/FundamentalHomomorphism.agda	Mon May 30 11:36:57 2022 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
--- fundamental homomorphism theorem
---
-
-open import Level hiding ( suc ; zero )
-module FundamentalHomomorphism (c l : Level) where
-
-open import Algebra
-open import Algebra.Structures
-open import Algebra.Definitions
-open import Data.Product
-open import Relation.Binary.PropositionalEquality 
-open import Algebra.Morphism.Structures
-open GroupMorphisms
-
-Group→Raw : {c l : Level } → Group c l → RawGroup c l
-Group→Raw G = record {
-     Carrier        = Carrier G
-     ; _≈_          = _≈_ G
-     ; _∙_          = _∙_ G
-     ; ε            = ε G
-     ; _⁻¹          = _⁻¹ G
-  } where open Group
-
-record NormalSubGroup ( G : Group c l ) : Set ( c  Level.⊔  l ) where
-  open Group G
-  field
-     sub : Carrier → Carrier 
-     s-homo  : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub
-     commute : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
-
-open import Relation.Binary.Morphism.Structures
-
-import Relation.Binary.Reasoning.Setoid as EqReasoning
-
-record HomoMorphism (G : Group c l) (f :  Group.Carrier G → Group.Carrier G) : Set ( c  Level.⊔  l ) where
-  open Group G
-  field
-     f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y
-     f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y
-     f-ε : f ( ε ) ≈ ε
-     f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹
-
-HM : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
-  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → HomoMorphism G f
-HM G f homo = record {
-   f-cong = λ eq → IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism
-           ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq
- ; f-homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))
- ; f-ε  = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo)
- ; f-inv = IsGroupHomomorphism.⁻¹-homo homo
- }
-
-open HomoMorphism
-
-hm : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
-   → HomoMorphism G f
-   → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f
-hm G f hm = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record {
-             isRelHomomorphism = record { cong = λ {x} {y} eq → f-cong hm {x} {y} eq } 
-           ; homo =  f-homo hm } ; ε-homo =  f-ε hm } ; ⁻¹-homo = f-inv hm
- } 
-
---
---  Coset : N : NormalSubGroup →  { a ∙ n | G ∋ a , N ∋ n }
---
-
-data Coset (G : Group c l)  (K : NormalSubGroup G) :  Group.Carrier G → Set ( c  Level.⊔  l ) where
-    coset : (a b : Group.Carrier G ) → Coset G K ( Group._∙_ G a (NormalSubGroup.sub K b) )
-
-record CosetCarrier (G : Group c l)  (K : NormalSubGroup G) :  Set ( c  Level.⊔  l ) where  
-  field
-    r :  Group.Carrier G
-    isCoset : Coset G K r
-
-open CosetCarrier 
-open NormalSubGroup 
-open import Relation.Binary.Structures
-
-φ :   {G : Group c l} →  {K : NormalSubGroup G} → Group.Carrier G → CosetCarrier G K
-φ {G} {K} x = record { r = ((x ∙ (sub K x) ⁻¹) ∙ sub K x) ; isCoset = coset (x ∙ (sub K x) ⁻¹) x }  where
-   open Group G
-
--- G / K : Quotient
-_/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) l 
-G / K = record {
-     Carrier        = CosetCarrier G K
-     ; _≈_          = λ x y → sub K (r x) ≈ sub K (r y)
-     ; _∙_          = λ x y → φ ( r x ∙ r y )
-     ; ε            = φ ε
-     ; _⁻¹          = λ x → φ ( (r x) ⁻¹ )
-     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = ise
-       ; ∙-cong = λ {x y u v} → ∙-cong1 {x} {y} {u} {v} }
-       ; assoc = assoc1 }
-       ; identity = identity1 }
-       ; inverse   = {!!} 
-       ; ⁻¹-cong   = {!!}
-      } 
-   } where 
-      open Group G
-      open EqReasoning (Algebra.Group.setoid G)
-      open HomoMorphism (HM G (sub K) (s-homo K ))
-      Eq =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
-             (IsGroup.isMonoid isGroup )))
-      ise : Relation.Binary.Structures.IsEquivalence _
-      ise = record { refl = IsEquivalence.refl Eq ; sym = IsEquivalence.sym Eq ; trans =  IsEquivalence.trans Eq } where
-      postulate   -- cheat
-        ∙-cong1 : {x y u v : CosetCarrier G K  }
-         → sub K (r x) ≈ sub K (r y)
-         → sub K (r u) ≈ sub K (r v)
-         → sub K (r ( φ {G} {K} (r x ∙ r u ) ))  ≈ sub K (r ( φ {G} {K} (r y ∙ r v ) ))  
-      -- ∙-cong1 {x} {y} {u} {v} x=y y=z = begin
-      --   sub K ((r x ∙ r u) ∙ sub K (r x ∙ r u) ⁻¹ ∙ sub K (r x ∙ r u)) ≈⟨ {!!} ⟩
-      --   sub K ((r y ∙ r v) ∙ sub K (r y ∙ r v) ⁻¹ ∙ sub K (r y ∙ r v)) ≈⟨ {!!} ⟩
-      --   sub K (r ( φ {G} {K} (r y ∙ r v ) )) ∎
-        assoc1 : (x y z : CosetCarrier G K )
-         → sub K (r (φ  {G} {K} (r (φ  {G} {K} (r x ∙ r y)) ∙ r z))) ≈ sub K (r (φ  {G} {K} (r x ∙ r (φ  {G} {K} (r y ∙ r z)))))
-      -- assoc1 x y z = begin
-      --     sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z ∙
-      --          sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z) ⁻¹ ∙
-      --          sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z)) ≈⟨ {!!} ⟩
-      --     sub K (r x ∙ r y ∙  r z ∙ sub K (r x ∙ r y ∙ r z) ⁻¹ ∙ sub K (r x ∙ r y ∙ r z))  ≈⟨ {!!} ⟩
-      --     sub K (r x ∙ r y ∙  r z )  ≈⟨ {!!} ⟩
-      --     sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z)) ∙
-      --          sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z))) ⁻¹ ∙
-      --          sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z)))) ∎
-        identity1 : ( (x : CosetCarrier G K ) → sub K (r (φ  {G} {K} (r (φ  {G} {K} ε) ∙ r x))) ≈ sub K (r x) )
-          × ( ( x : CosetCarrier G K ) → sub K (r (φ  {G} {K} (r x ∙ r (φ  {G} {K} ε)))) ≈ sub K (r x) )
-        inverse1 : Inverse (λ x y → sub K (r x) ≈ sub K (r y)) (φ  {G} {K}ε) (λ x → φ  {G} {K}(r x ⁻¹)) (λ x y → φ  {G} {K}(r x ∙ r y))
-        ⁻¹-cong1 :  Congruent₁ (λ x y → sub K (r x) ≈ sub K (r y)) (λ x → φ  {G} {K}(r x ⁻¹))
-
--- K ⊂ ker(f)
-K⊆ker : (G H : Group c l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
-K⊆ker G H K f = (x : Group.Carrier G ) → f ( sub K x ) ≈ ε   where
-  open Group H
-
-record FundamentalHomomorphism (G H : Group c l)  
-    (f : Group.Carrier G → Group.Carrier H ) 
-    (homo : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f ) 
-    (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set ( c  Level.⊔  l ) where
-  open Group H
-  field
-    h : CosetCarrier G K → Group.Carrier H
-    h-homo :  IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) h 
-    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
-
-FundamentalHomomorphismTheorm : (G H : Group c l)
-    (f : Group.Carrier G → Group.Carrier H )
-    (homo : IsGroupHomomorphism (Group→Raw G) (Group→Raw H) f )
-    (K : NormalSubGroup G ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f homo K kf
-FundamentalHomomorphismTheorm G H f homo K kf = record {
-     h = h
-   ; h-homo = h-homo
-   ; unique = unique
-  } where
-    open Group H
-    EqH =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
-             (IsGroup.isMonoid isGroup )))
-    EqG =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
-             (IsGroup.isMonoid (Group.isGroup G) )))
-    h1 : {x : Group.Carrier G } → Coset G K x → Carrier
-    h1 (coset a b) = f a 
-    h : CosetCarrier G K → Carrier   --  G / K → H
-    h r = h1 (isCoset r) 
-    _o_ = Group._∙_ G
-    open EqReasoning (Algebra.Group.setoid H )
-    h03 : (x y : Group.Carrier (G / K ) ) → h ( Group._∙_ (G / K ) x  y ) ≈ h x ∙ h y
-    h03 x y = h13 (isCoset x) (isCoset y) where
-        h13 : {gx gy : Group.Carrier G } → ( x : Coset G K gx ) ( y : Coset G K gy )
-           → h (Group._∙_ (G / K) record { r = gx ; isCoset = x } record {r = gy ; isCoset = y } ) ≈ h1 x ∙ h1 y
-        h13  (coset a b) (coset c d) = begin
-          h (φ {G} {K} ((a o sub K b) o (c o sub K d) )) ≡⟨ _≡_.refl  ⟩
-          f ( ((a o sub K b) o (c o sub K d )) o Group._⁻¹ G ( sub K ( (a o sub K b) o (c o sub K d)))) ≈⟨ {!!} ⟩
-          f (a o c) ≈⟨ {!!} ⟩
-          f a ∙ f c ≡⟨ _≡_.refl ⟩
-          h1 (coset a b) ∙ h1 (coset c d)  ∎
-    h-homo :  IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) h 
-    h-homo = record {
-     isMonoidHomomorphism = record {
-          isMagmaHomomorphism = record {
-             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } 
-           ; homo = h03 }
-        ; ε-homo = {!!} }
-       ; ⁻¹-homo = {!!} }
-    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
-    unique x = begin
-         f x ≈⟨ {!!} ⟩
-         f ( x o (Group._⁻¹ G (sub K x)))   ∎
-
-
-
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Gutil0.agda	Tue May 31 08:47:46 2022 +0900
@@ -0,0 +1,98 @@
+open import Level hiding ( suc ; zero )
+module Gutil0  where
+
+open import Algebra
+open import Algebra.Structures
+open import Algebra.Definitions
+open import Data.Product
+open import Relation.Binary.PropositionalEquality 
+open import Algebra.Morphism.Structures
+open import Data.Empty
+open import Relation.Nullary
+
+open GroupMorphisms
+
+GR : {c l : Level } → Group c l → RawGroup c l
+GR G = record {
+     Carrier        = Carrier G
+     ; _≈_          = _≈_ G
+     ; _∙_          = _∙_ G
+     ; ε            = ε G
+     ; _⁻¹          = _⁻¹ G
+  } where open Group
+
+record GAxiom {c l : Level } (G : Group c l)  : Set ( c  Level.⊔  l ) where
+  open Group G
+  field
+     ∙-cong :  {x y u v : Carrier } → x ≈ y → u ≈ v →  x ∙ u ≈  y ∙ v 
+     assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈  x ∙ ( y ∙ z )
+     identity : ((y : Carrier) → ε ∙ y ≈ y ) ×  ((y : Carrier) → y ∙ ε ≈ y )
+     inverse   : ((y : Carrier) → y ⁻¹ ∙ y  ≈ ε ) ×  ((y : Carrier) → y ∙ y ⁻¹  ≈ ε )
+     ⁻¹-cong   : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹
+
+GA : {c l : Level } → (G : Group c l) → GAxiom G
+GA G = record {
+        ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)))
+     ;  assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))
+     ;  identity = IsMonoid.identity ( IsGroup.isMonoid isGroup)
+     ;  inverse   = IsGroup.inverse isGroup
+     ;  ⁻¹-cong   = IsGroup.⁻¹-cong isGroup
+   } where open Group G
+
+open import Relation.Binary.Structures
+
+Eq : {c l : Level } → (G : Group c l) → IsEquivalence _
+Eq G =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
+             (IsGroup.isMonoid (Group.isGroup G ))) )
+
+grefl : {c l : Level } → (G : Group c l ) → {x : Group.Carrier G} → Group._≈_ G x x
+grefl G = IsGroup.refl ( Group.isGroup G )
+
+gsym : {c l : Level } → (G : Group c l ) → {x y : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y x
+gsym G = IsGroup.sym ( Group.isGroup G )
+
+gtrans : {c l : Level } → (G : Group c l ) → {x y z : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y z → Group._≈_ G x z
+gtrans G = IsGroup.trans ( Group.isGroup G )
+
+record NormalSubGroup {c l : Level } ( G : Group c l ) : Set ( c  Level.⊔  l ) where
+  open Group G
+  field
+     sub : Carrier → Carrier 
+     s-homo  : IsGroupHomomorphism (GR G) (GR G) sub
+     commute : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
+     -- it has at least one element other than ε 
+     -- anElement : Carrier
+     -- notE : ¬ ( Group._≈_ G anElement (Group.ε G) )
+
+-- open import Relation.Binary.Morphism.Structures
+
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+
+record HomoMorphism {c l : Level } (G : Group c l) (f :  Group.Carrier G → Group.Carrier G) : Set ( c  Level.⊔  l ) where
+  open Group G
+  field
+     f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y
+     f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y
+     f-ε : f ( ε ) ≈ ε
+     f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹
+
+-- HM : {c l : Level } → (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+--   → IsGroupHomomorphism (GR G) (GR G) f → HomoMorphism G f
+-- HM G f homo = record {
+--    f-cong = λ eq → IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism
+--            ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq
+--  ; f-homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))
+--  ; f-ε  = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo)
+--  ; f-inv = IsGroupHomomorphism.⁻¹-homo homo
+--  }
+-- 
+-- open HomoMorphism
+-- 
+-- hm : {c l : Level } → (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+--    → HomoMorphism G f
+--    → IsGroupHomomorphism (GR G) (GR G) f
+-- hm G f hm = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record {
+--              isRelHomomorphism = record { cong = λ {x} {y} eq → f-cong hm {x} {y} eq } 
+--            ; homo =  f-homo hm } ; ε-homo =  f-ε hm } ; ⁻¹-homo = f-inv hm
+--  } 
+--