Mercurial > hg > Members > kono > Proof > galois

changeset 259:b53eedf6dfb1

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 Sun, 29 May 2022 17:46:47 +0900
parents ea5087692f7e
children 26c0d50e455f
files src/FundamentalHomomorphism.agda
diffstat 1 files changed, 96 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/FundamentalHomomorphism.agda	Sun May 29 12:36:07 2022 +0900
+++ b/src/FundamentalHomomorphism.agda	Sun May 29 17:46:47 2022 +0900
@@ -30,30 +30,83 @@
   field
      sub : Carrier → Carrier 
      subgroup  : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub
-     normal : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
+     commute : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
+
+open import Relation.Binary.Morphism.Structures
+
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+
+
+f-cong : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f →  {x y : Group.Carrier G } → (Group._≈_ G) x y → (Group._≈_ G) (f x) (f y)
+f-cong G f homo eq = IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism
+           ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq
+
+f-homo : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → (x y : Group.Carrier G )
+  → Group._≈_ G (f ( Group._∙_ G x  y ))  ( Group._∙_ G (f x)  (f y))
+f-homo G f homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))
+
+f-ε : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → Group._≈_  G (f ( Group.ε G )) (Group.ε G)
+f-ε G f homo = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo)
+
+f-inv : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → (x : Group.Carrier G) → Group._≈_  G (f ( Group._⁻¹ G x )) (Group._⁻¹ G (f x ))
+f-inv G f homo = IsGroupHomomorphism.⁻¹-homo homo
+
+p01 : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+   → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f
+   → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f
+p01 G f homo = record {
+     isMonoidHomomorphism = record {
+          isMagmaHomomorphism = record {
+             isRelHomomorphism = record { cong = λ {x} {y} eq → p02 x y eq } 
+           ; homo = p03 
+          }
+        ; ε-homo = p04
+       }
+   ; ⁻¹-homo = p05
+ } where
+    open Group G
+    p02 : (x y : Carrier ) → x ≈ y → f x ≈ f y
+    p02 x y =  f-cong G f homo 
+    p03 : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y
+    p03 =  f-homo G f homo 
+    p04 : f ( ε ) ≈ ε
+    p04 =  f-ε G f homo 
+    p05 : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹
+    p05 = f-inv G f homo
+
 
 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
+    cscong : {a b : Group.Carrier G } → Group._≈_ G (NormalSubGroup.sub K a) (NormalSubGroup.sub K b) → Coset G K a → Coset G 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 
+
 φ :   {G : Group c l} →  {K : NormalSubGroup G} → Group.Carrier G → CosetCarrier G K
-φ {G} {K} x = record { r = NormalSubGroup.sub K x ; isCoset = p1 } where
-   p1 :  Coset G K (NormalSubGroup.sub K x)
-   p1 = cscong (proj₁ (Group.identity G) (NormalSubGroup.sub K x ) ) (coset (Group.ε G) x )
+φ {G} {K} x = record { r = sub K x ; isCoset = p1 } where
+   open Group G
+   p1 :  Coset G K (sub K x)
+   p1 = cscong 
+     (f-cong G (sub K) (subgroup K) (proj₁ (Group.identity G) (NormalSubGroup.sub K x ) ) )
+     (coset (Group.ε G) x )
 
 -- G / K : Quotient
 _/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) l
 G / K = record {
      Carrier        = CosetCarrier G K
-     ; _≈_          = λ x y → r x ≈ r y
-     ; _∙_          = λ x y → record { r =  r x ∙ r y ; isCoset = ? }
-     ; ε            = record { r =  ε ; isCoset = {!!} }
-     ; _⁻¹          = λ x → record { r = (r x) ⁻¹  ; isCoset = {!!} }
+     ; _≈_          = λ x y → sub K (r x) ≈ sub K (r y)
+     ; _∙_          = λ x y → record { r =  r x ∙ r y ; isCoset = q01 x y }
+     ; ε            = record { r =  ε ; isCoset = cscong {!!} (coset ε  ε) }
+     ; _⁻¹          = λ x → record { r = (r x) ⁻¹  ; isCoset = cscong {!!} ( coset ε ((r x) ⁻¹ )) }
      ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
        isEquivalence = {!!}
        ; ∙-cong = {!!} }
@@ -64,7 +117,20 @@
       } 
    } where 
       open Group G
-      open CosetCarrier 
+      open EqReasoning (Algebra.Group.setoid G)
+      q01 : (x y : CosetCarrier G K ) → Coset G K (r x ∙ r y)
+      q01 x y with isCoset x | isCoset y
+      ... | coset a b | coset c d = cscong q02 ( coset (a ∙ c) (b ∙ d) ) where
+          q02 : sub K (a ∙ c ∙ sub K (b ∙ d)) ≈ sub K (a ∙ sub K b ∙ (c ∙ sub K d))
+          q02 = f-cong G (sub K) (subgroup K) ( begin
+             a ∙ c ∙ sub K (b ∙ d)  ≈⟨ {!!} ⟩
+             a ∙ c ∙ (sub K b ∙ sub K d)  ≈⟨ {!!} ⟩
+             a ∙ (c ∙ sub K b ) ∙ sub K d  ≈⟨ {!!} ⟩
+             a ∙ (sub K b ∙ c ) ∙ sub K d  ≈⟨ {!!} ⟩
+             a ∙ sub K b ∙ (c ∙ sub K d)  ∎  )
+      ... | coset a b | cscong eq x = {!!}
+      ... | cscong eq x | coset a b = {!!}
+      ... | cscong eqx x | cscong eqy y = {!!}
 
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
@@ -79,13 +145,31 @@
   field
     h : K⊆ker G H K f → CosetCarrier G K → Group.Carrier H
     h-homo : (kf : K⊆ker G H K f ) → IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) (h kf)
-    uniqune : (kf : K⊆ker G H K f ) → (x : Group.Carrier G)  →  f x ≈ h kf ( φ x )
+    unique : (kf : K⊆ker G H K f ) → (x : Group.Carrier G)  →  f x ≈ h kf ( φ 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 ) → FundamentalHomomorphism G H f homo K
-FundamentalHomomorphismTheorm G H f homo K = {!!}
+FundamentalHomomorphismTheorm G H f homo K = record {
+     h = h
+   ; h-homo = h-homo
+   ; unique = unique
+  } where
+    open Group H
+    h : K⊆ker G H K f → CosetCarrier G K → Group.Carrier H
+    h kf r = {!!}
+    h-homo : (kf : K⊆ker G H K f ) → IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) (h kf)
+    h-homo kf = record {
+     isMonoidHomomorphism = record {
+          isMagmaHomomorphism = record {
+             isRelHomomorphism = record { cong = λ {x} {y} eq → ? } 
+           ; homo = ? }
+        ; ε-homo = ? }
+       ; ⁻¹-homo = ? }
+    unique : (kf : K⊆ker G H K f ) → (x : Group.Carrier G)  →  f x ≈ h kf ( φ x )
+    unique kf x = {!!}
 
 
 
+