Mercurial > hg > Members > kono > Proof > galois

changeset 273:9bee24b4017f

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, 24 Jan 2023 23:38:32 +0900
parents ce372f6347d6
children 691b2ee844ef
files src/Fundamental.agda
diffstat 1 files changed, 13 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/Fundamental.agda	Tue Jan 24 19:15:38 2023 +0900
+++ b/src/Fundamental.agda	Tue Jan 24 23:38:32 2023 +0900
@@ -124,7 +124,9 @@
   open NormalSubGroup K
 
 φ : (G : Group c c)  (K : NormalSubGroup G) → Group.Carrier G → Group.Carrier (G / K )
-φ G K g = ?
+φ G K g x = record { a = x ; n = ε ; aN=x = ? } where
+  open Group G
+  open NormalSubGroup K
 
 φ-homo : (G : Group c c)  (K : NormalSubGroup G) → IsGroupHomomorphism (GR G) (GR (G / K)) (φ G K)
 φ-homo = ?
@@ -141,17 +143,18 @@
        φ-cong : {f g : Carrier } → f ≈ g  → {x : Carrier } →  ⟦ n (φ G K f x ) ⟧ ≈ ⟦ n (φ G K g x ) ⟧ 
        φ-cong = ?
 
+inv-φ : (G : Group c c)  (K : NormalSubGroup G) → Group.Carrier (G / K ) → Group.Carrier G
+inv-φ = ?
+
 φ-surjective : (G : Group c c)  (K : NormalSubGroup G) → Surjective (φe G K )
-φ-surjective G K = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse } where
+φ-surjective G K = record { from = record { _⟨$⟩_ = inv-φ G K ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse } where
        open Group G
        open aN
        open NormalSubGroup K
        open IsGroupHomomorphism normal 
-       inv-φ : Group.Carrier (G / K ) → Group.Carrier G
-       inv-φ = ?
-       cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g
+       cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ G K f ≈ inv-φ G K g
        cong-i = ?
-       is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ G K (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧
+       is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ G K (inv-φ G K f) y) ⟧ ≈ ⟦ n (f y) ⟧
        is-inverse = ?
  
 record FundamentalHomomorphism (G H : Group c c )
@@ -178,8 +181,7 @@
   } where
     open Group H
     h : Group.Carrier (G / K ) → Group.Carrier H
-    h r = ?
-    _o_ = Group._∙_ G
+    h r = f ( aN.n (r (Group.ε G )  ))
     h03 : (x y : Group.Carrier (G / K ) ) →  h ( qadd G K x y ) ≈ h x ∙ h y
     h03 x y = {!!}
     h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
@@ -192,7 +194,9 @@
        ; ⁻¹-homo = {!!} }
     is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ G K x )
     is-solution x = begin
-         f x ≈⟨ grefl H ⟩
+         f x ≈⟨ ? ⟩
+         ? ≈⟨ ? ⟩
+         f ( aN.n (( φ G K x ) (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 )