Mercurial > hg > Members > kono > Proof > galois

changeset 268:86408a621c6e

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 12:42:57 +0900
parents 864afb582fc7
children 0452e7021054
files src/Fundamental.agda
diffstat 1 files changed, 10 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/Fundamental.agda	Tue May 31 12:27:07 2022 +0900
+++ b/src/Fundamental.agda	Tue May 31 12:42:57 2022 +0900
@@ -125,7 +125,7 @@
           sub K (base y ∙ base v) ≈⟨ {!!} ⟩
           sub K (base (mul y v))  ∎ 
       assoc1 : (x y z  : COSET G K) → sub K (base (mul (mul x y ) z)) ≈ sub K (base (mul x ( mul y z ) ))
-      assoc1 x y z =  {!!} where
+      assoc1 x y z =  {!!} 
         -- crefl1 (coset a b) = ⟦⟧-cong (grefl G) 
 
 -- K ⊂ ker(f)
@@ -139,9 +139,9 @@
     (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 )
+    h : COSET G K → Group.Carrier H
+    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
+    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
 
 FundamentalHomomorphismTheorm : (G H : Group c l)
     (f : Group.Carrier G → Group.Carrier H )
@@ -159,10 +159,11 @@
              (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 (cscong a b) = h1 b
+    h : COSET G K → Carrier   --  G / K → H
+    h r = h1 {Group.ε G} (r (Group.ε G))
     _o_ = Group._∙_ G
-    h03 : (x y : Group.Carrier (G / K ) ) → {!!}
+    h03 : (x y : Group.Carrier (G / K ) ) →  h ( mul x y ) ≈ h x ∙ h y
     h03 x y = {!!} 
     h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) {!!} 
     h-homo = record {
@@ -175,7 +176,8 @@
     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 )
+         f ((G Group.∙ Group.ε G) ((G Group.⁻¹) (sub K x))) ≈⟨ grefl H  ⟩
+         h1 {Group.ε G} ((φ x) (Group.ε G))  ∎ where open EqReasoning (Algebra.Group.setoid H )