Mercurial > hg > Members > kono > Proof > galois

changeset 260:26c0d50e455f

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 20:23:40 +0900
parents b53eedf6dfb1
children ea6c61079789
files src/FundamentalHomomorphism.agda
diffstat 1 files changed, 32 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/src/FundamentalHomomorphism.agda	Sun May 29 17:46:47 2022 +0900
+++ b/src/FundamentalHomomorphism.agda	Sun May 29 20:23:40 2022 +0900
@@ -8,10 +8,6 @@
 open import Algebra.Structures
 open import Algebra.Definitions
 open import Data.Product
--- open import Function hiding (id ; flip)
--- open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
--- open import Function.LeftInverse  using ( _LeftInverseOf_ )
--- open import Function.Equality using (Π)
 open import Relation.Binary.PropositionalEquality 
 open import Algebra.Morphism.Structures
 open GroupMorphisms
@@ -140,35 +136,51 @@
 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 ) :  Set ( c  Level.⊔  l ) where
+    (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set ( c  Level.⊔  l ) where
   open Group H
   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)
-    unique : (kf : K⊆ker G H K f ) → (x : Group.Carrier G)  →  f x ≈ h kf ( φ x )
+    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 ) → FundamentalHomomorphism G H f homo K
-FundamentalHomomorphismTheorm G H f homo K = record {
+    (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
-    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 {
+    h1 : {x : Group.Carrier G } → Coset G K x → Carrier
+    h1 (coset a b) = f b
+    h1 (cscong eq t) = h1 t 
+    h : CosetCarrier G K → Carrier   --  G / K → H
+    h r = h1 (isCoset r) 
+    _o_ = Group._∙_ G
+    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
+          h1 (coset (a o c) (b o d) ) ≈⟨ {!!} ⟩
+          f (b o d)  ≈⟨ {!!} ⟩
+          f b  ∙ f d  ≈⟨ {!!} ⟩
+          h1 (coset a b) ∙ h1 (coset c d) ∎  where open EqReasoning (Algebra.Group.setoid H )
+        h13  (coset a b) (cscong x y) = {!!}
+        h13  (cscong x x₁) (coset a b) = {!!}
+        h13  (cscong x x₁) (cscong x₂ y) = {!!}
+    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 = ? }
-        ; ε-homo = ? }
-       ; ⁻¹-homo = ? }
-    unique : (kf : K⊆ker G H K f ) → (x : Group.Carrier G)  →  f x ≈ h kf ( φ x )
-    unique kf x = {!!}
+             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } 
+           ; homo = h03 }
+        ; ε-homo = {!!} }
+       ; ⁻¹-homo = {!!} }
+    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
+    unique x = Algebra.Group.refl H