Mercurial > hg > Members > kono > Proof > galois

changeset 262:f36d2ed8ed9e

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 Mon, 30 May 2022 11:28:38 +0900
parents ea6c61079789
children 93a2a2c2d7c0
files src/FundamentalHomomorphism.agda
diffstat 1 files changed, 8 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/FundamentalHomomorphism.agda	Mon May 30 10:57:30 2022 +0900
+++ b/src/FundamentalHomomorphism.agda	Mon May 30 11:28:38 2022 +0900
@@ -131,7 +131,7 @@
 
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
-K⊆ker G H K f = (k : CosetCarrier G K ) → f (CosetCarrier.r k ) ≈ ε   where
+K⊆ker G H K f = (x : Group.Carrier G ) → f ( sub K x ) ≈ ε   where
   open Group H
 
 record FundamentalHomomorphism (G H : Group c l)  
@@ -159,7 +159,7 @@
     EqG =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
              (IsGroup.isMonoid (Group.isGroup G) )))
     h1 : {x : Group.Carrier G } → Coset G K x → Carrier
-    h1 (coset a b) = f (sub K b)
+    h1 (coset a b) = f a ∙ f (sub K b)
     h : CosetCarrier G K → Carrier   --  G / K → H
     h r = h1 (isCoset r) 
     _o_ = Group._∙_ G
@@ -169,9 +169,11 @@
         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
-          h (φ {G} {K} ((a o sub K b) o (c o sub K d) )) ≈⟨ IsEquivalence.refl EqH ⟩
-          f (sub K (( a o sub K b ) o (c o sub K d )))  ≈⟨ {!!} ⟩
-          f (sub K b) ∙ f (sub K d) ≈⟨ IsEquivalence.refl EqH ⟩
+          h (φ {G} {K} ((a o sub K b) o (c o sub K d) )) ≡⟨  _≡_.refl  ⟩
+          f ( ((a o sub K b) o (c o sub K d)) o ( Group._⁻¹ G (sub K ((a o sub K b) o (c o sub K d))) )) ∙
+             f (sub K ((a o sub K b ) o (c o sub K d))) ≈⟨ {!!} ⟩
+          f ((a o sub K b ) o (c o sub K d)) ≈⟨ {!!} ⟩
+          f a ∙ f (sub K b) ∙ (f c ∙ f (sub K d)) ≡⟨ _≡_.refl ⟩
           h1 (coset a b) ∙ h1 (coset c d)  ∎
     h-homo :  IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) h 
     h-homo = record {
@@ -184,7 +186,7 @@
     unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
     unique x = begin
          f x ≈⟨ {!!} ⟩
-         f (sub K x ) ∎
+         f ( x o (Group._⁻¹ G (sub K x))) ∙ f (sub K x)  ∎