Mercurial > hg > Members > kono > Proof > galois

changeset 283:b89af4300407

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 Jan 2023 11:28:56 +0900
parents b70cc2534d2f
children 69645d667f45
files src/Fundamental.agda
diffstat 1 files changed, 38 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/src/Fundamental.agda	Sun Jan 29 10:47:09 2023 +0900
+++ b/src/Fundamental.agda	Sun Jan 29 11:28:56 2023 +0900
@@ -132,7 +132,7 @@
 open import Function.Surjection
 open import Function.Equality
 
-module _ (G : Group c c) (K : NormalSubGroup G) where
+module GK (G : Group c c) (K : NormalSubGroup G) where
     open Group G
     open aN
     open an
@@ -179,17 +179,33 @@
     φ-surjective : Surjective φe
     φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse }
 
+    gk00 : {x : Carrier } → ⟦ factor ε x ⟧ ⁻¹ ≈ x
+    gk00 {x} = begin
+        ⟦ factor ε x ⟧ ⁻¹ ≈⟨ ? ⟩ 
+        ( x ⁻¹ ∙ ( x ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ? ⟩ 
+        ( x ⁻¹ ∙ ( x ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ⁻¹-cong (∙-cong grefl (is-factor ε x))  ⟩ 
+        ( x ⁻¹ ∙ ε ) ⁻¹ ≈⟨ ? ⟩ 
+        ( x ⁻¹  ) ⁻¹ ≈⟨ ? ⟩ 
+        x ∎
+
+    gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x >
+    gk01 x = begin
+        ⟦ factor ε ( inv-φ x) ⟧  ≈⟨ ? ⟩ 
+        ⟦ n x ⟧ ∎
+
+
 record FundamentalHomomorphism (G H : Group c c )
     (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 where
   open Group H
+  open GK G K
   field
     h : Group.Carrier (G / K ) → Group.Carrier H
     h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
-    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ G K x )
-    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  →
-       ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
+    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
+    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
+       → ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
 
 FundamentalHomomorphismTheorm : (G H : Group c c)
     (f : Group.Carrier G → Group.Carrier H )
@@ -201,9 +217,14 @@
    ; is-solution = is-solution
    ; unique = unique
   } where
+    open GK G K
     open Group H
+    open Gutil H
+    open NormalSubGroup K
+    open IsGroupHomomorphism homo
+    open aN
     h : Group.Carrier (G / K ) → Group.Carrier H
-    h r = f ( aN.n ? )
+    h r = f ( inv-φ r )
     h03 : (x y : Group.Carrier (G / K ) ) →  h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
     h03 x y = {!!}
     h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
@@ -214,15 +235,19 @@
            ; homo = h03 }
         ; ε-homo = {!!} }
        ; ⁻¹-homo = {!!} }
-    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ G K x )
+    open EqReasoning (Algebra.Group.setoid H)
+    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
     is-solution x = begin
-         f x ≈⟨ ? ⟩
-         ? ≈⟨ ? ⟩
-         f ( aN.n (( φ G K  ) (Group.ε G )  )) ≈⟨ ?  ⟩
-         h ( φ G K x ) ∎ where open EqReasoning (Algebra.Group.setoid H )
-    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  →
-       ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
-    unique = ?
+         f x ≈⟨ gsym ( ⟦⟧-cong (gk00 ))  ⟩
+         f ( Group._⁻¹ G  ⟦ factor (Group.ε G) x  ⟧   ) ≈⟨ grefl  ⟩
+         h ( φ x ) ∎ 
+    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
+       → ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
+    unique h1 h1-homo h1-is-solution x = begin
+         h x ≈⟨ grefl ⟩
+         f ( inv-φ x ) ≈⟨ h1-is-solution _ ⟩
+         h1 ( φ ( inv-φ x ) ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (gk01 x)  ⟩
+         h1 x ∎