Mercurial > hg > Members > kono > Proof > galois

changeset 261:ea6c61079789

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 10:57:30 +0900
parents 26c0d50e455f
children f36d2ed8ed9e
files src/FundamentalHomomorphism.agda
diffstat 1 files changed, 79 insertions(+), 75 deletions(-) [+]
line wrap: on
line diff
--- a/src/FundamentalHomomorphism.agda	Sun May 29 20:23:40 2022 +0900
+++ b/src/FundamentalHomomorphism.agda	Mon May 30 10:57:30 2022 +0900
@@ -25,59 +25,47 @@
   open Group G
   field
      sub : Carrier → Carrier 
-     subgroup  : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub
+     s-homo  : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub
      commute : ( g n : Carrier  ) → g ∙  sub n  ≈ sub n ∙ g
 
 open import Relation.Binary.Morphism.Structures
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
-
-f-cong : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
-  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f →  {x y : Group.Carrier G } → (Group._≈_ G) x y → (Group._≈_ G) (f x) (f y)
-f-cong G f homo eq = IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism
-           ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq
+record HomoMorphism (G : Group c l) (f :  Group.Carrier G → Group.Carrier G) : Set ( c  Level.⊔  l ) where
+  open Group G
+  field
+     f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y
+     f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y
+     f-ε : f ( ε ) ≈ ε
+     f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹
 
-f-homo : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
-  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → (x y : Group.Carrier G )
-  → Group._≈_ G (f ( Group._∙_ G x  y ))  ( Group._∙_ G (f x)  (f y))
-f-homo G f homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))
+HM : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → HomoMorphism G f
+HM G f homo = record {
+   f-cong = λ eq → IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism
+           ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq
+ ; f-homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))
+ ; f-ε  = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo)
+ ; f-inv = IsGroupHomomorphism.⁻¹-homo homo
+ }
 
-f-ε : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
-  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → Group._≈_  G (f ( Group.ε G )) (Group.ε G)
-f-ε G f homo = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo)
+open HomoMorphism
 
-f-inv : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
-  → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → (x : Group.Carrier G) → Group._≈_  G (f ( Group._⁻¹ G x )) (Group._⁻¹ G (f x ))
-f-inv G f homo = IsGroupHomomorphism.⁻¹-homo homo
-
-p01 : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+hm : (G : Group c l ) → (f :  Group.Carrier G → Group.Carrier G )
+   → HomoMorphism G f
    → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f
-   → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f
-p01 G f homo = record {
-     isMonoidHomomorphism = record {
-          isMagmaHomomorphism = record {
-             isRelHomomorphism = record { cong = λ {x} {y} eq → p02 x y eq } 
-           ; homo = p03 
-          }
-        ; ε-homo = p04
-       }
-   ; ⁻¹-homo = p05
- } where
-    open Group G
-    p02 : (x y : Carrier ) → x ≈ y → f x ≈ f y
-    p02 x y =  f-cong G f homo 
-    p03 : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y
-    p03 =  f-homo G f homo 
-    p04 : f ( ε ) ≈ ε
-    p04 =  f-ε G f homo 
-    p05 : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹
-    p05 = f-inv G f homo
+hm G f hm = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record {
+             isRelHomomorphism = record { cong = λ {x} {y} eq → f-cong hm {x} {y} eq } 
+           ; homo =  f-homo hm } ; ε-homo =  f-ε hm } ; ⁻¹-homo = f-inv hm
+ } 
 
+--
+--  Coset : N : NormalSubGroup →  { a ∙ n | G ∋ a , N ∋ n }
+--
 
 data Coset (G : Group c l)  (K : NormalSubGroup G) :  Group.Carrier G → Set ( c  Level.⊔  l ) where
     coset : (a b : Group.Carrier G ) → Coset G K ( Group._∙_ G a (NormalSubGroup.sub K b) )
-    cscong : {a b : Group.Carrier G } → Group._≈_ G (NormalSubGroup.sub K a) (NormalSubGroup.sub K b) → Coset G K a → Coset G K b
 
 record CosetCarrier (G : Group c l)  (K : NormalSubGroup G) :  Set ( c  Level.⊔  l ) where  
   field
@@ -86,47 +74,60 @@
 
 open CosetCarrier 
 open NormalSubGroup 
+open import Relation.Binary.Structures
 
 φ :   {G : Group c l} →  {K : NormalSubGroup G} → Group.Carrier G → CosetCarrier G K
-φ {G} {K} x = record { r = sub K x ; isCoset = p1 } where
+φ {G} {K} x = record { r = ((x ∙ (sub K x) ⁻¹) ∙ sub K x) ; isCoset = coset (x ∙ (sub K x) ⁻¹) x }  where
    open Group G
-   p1 :  Coset G K (sub K x)
-   p1 = cscong 
-     (f-cong G (sub K) (subgroup K) (proj₁ (Group.identity G) (NormalSubGroup.sub K x ) ) )
-     (coset (Group.ε G) x )
 
 -- G / K : Quotient
-_/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) l
+_/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) l 
 G / K = record {
      Carrier        = CosetCarrier G K
      ; _≈_          = λ x y → sub K (r x) ≈ sub K (r y)
-     ; _∙_          = λ x y → record { r =  r x ∙ r y ; isCoset = q01 x y }
-     ; ε            = record { r =  ε ; isCoset = cscong {!!} (coset ε  ε) }
-     ; _⁻¹          = λ x → record { r = (r x) ⁻¹  ; isCoset = cscong {!!} ( coset ε ((r x) ⁻¹ )) }
+     ; _∙_          = λ x y → φ ( r x ∙ r y )
+     ; ε            = φ ε
+     ; _⁻¹          = λ x → φ ( (r x) ⁻¹ )
      ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = {!!}
-       ; ∙-cong = {!!} }
-       ; assoc = {!!} }
-       ; identity = {!!} }
+       isEquivalence = ise
+       ; ∙-cong = λ {x y u v} → ∙-cong1 {x} {y} {u} {v} }
+       ; assoc = assoc1 }
+       ; identity = identity1 }
        ; inverse   = {!!} 
        ; ⁻¹-cong   = {!!}
       } 
    } where 
       open Group G
       open EqReasoning (Algebra.Group.setoid G)
-      q01 : (x y : CosetCarrier G K ) → Coset G K (r x ∙ r y)
-      q01 x y with isCoset x | isCoset y
-      ... | coset a b | coset c d = cscong q02 ( coset (a ∙ c) (b ∙ d) ) where
-          q02 : sub K (a ∙ c ∙ sub K (b ∙ d)) ≈ sub K (a ∙ sub K b ∙ (c ∙ sub K d))
-          q02 = f-cong G (sub K) (subgroup K) ( begin
-             a ∙ c ∙ sub K (b ∙ d)  ≈⟨ {!!} ⟩
-             a ∙ c ∙ (sub K b ∙ sub K d)  ≈⟨ {!!} ⟩
-             a ∙ (c ∙ sub K b ) ∙ sub K d  ≈⟨ {!!} ⟩
-             a ∙ (sub K b ∙ c ) ∙ sub K d  ≈⟨ {!!} ⟩
-             a ∙ sub K b ∙ (c ∙ sub K d)  ∎  )
-      ... | coset a b | cscong eq x = {!!}
-      ... | cscong eq x | coset a b = {!!}
-      ... | cscong eqx x | cscong eqy y = {!!}
+      open HomoMorphism (HM G (sub K) (s-homo K ))
+      Eq =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
+             (IsGroup.isMonoid isGroup )))
+      ise : Relation.Binary.Structures.IsEquivalence _
+      ise = record { refl = IsEquivalence.refl Eq ; sym = IsEquivalence.sym Eq ; trans =  IsEquivalence.trans Eq } where
+      postulate   -- cheat
+        ∙-cong1 : {x y u v : CosetCarrier G K  }
+         → sub K (r x) ≈ sub K (r y)
+         → sub K (r u) ≈ sub K (r v)
+         → sub K (r ( φ {G} {K} (r x ∙ r u ) ))  ≈ sub K (r ( φ {G} {K} (r y ∙ r v ) ))  
+      -- ∙-cong1 {x} {y} {u} {v} x=y y=z = begin
+      --   sub K ((r x ∙ r u) ∙ sub K (r x ∙ r u) ⁻¹ ∙ sub K (r x ∙ r u)) ≈⟨ {!!} ⟩
+      --   sub K ((r y ∙ r v) ∙ sub K (r y ∙ r v) ⁻¹ ∙ sub K (r y ∙ r v)) ≈⟨ {!!} ⟩
+      --   sub K (r ( φ {G} {K} (r y ∙ r v ) )) ∎
+        assoc1 : (x y z : CosetCarrier G K )
+         → sub K (r (φ  {G} {K} (r (φ  {G} {K} (r x ∙ r y)) ∙ r z))) ≈ sub K (r (φ  {G} {K} (r x ∙ r (φ  {G} {K} (r y ∙ r z)))))
+      -- assoc1 x y z = begin
+      --     sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z ∙
+      --          sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z) ⁻¹ ∙
+      --          sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z)) ≈⟨ {!!} ⟩
+      --     sub K (r x ∙ r y ∙  r z ∙ sub K (r x ∙ r y ∙ r z) ⁻¹ ∙ sub K (r x ∙ r y ∙ r z))  ≈⟨ {!!} ⟩
+      --     sub K (r x ∙ r y ∙  r z )  ≈⟨ {!!} ⟩
+      --     sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z)) ∙
+      --          sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z))) ⁻¹ ∙
+      --          sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z)))) ∎
+        identity1 : ( (x : CosetCarrier G K ) → sub K (r (φ  {G} {K} (r (φ  {G} {K} ε) ∙ r x))) ≈ sub K (r x) )
+          × ( ( x : CosetCarrier G K ) → sub K (r (φ  {G} {K} (r x ∙ r (φ  {G} {K} ε)))) ≈ sub K (r x) )
+        inverse1 : Inverse (λ x y → sub K (r x) ≈ sub K (r y)) (φ  {G} {K}ε) (λ x → φ  {G} {K}(r x ⁻¹)) (λ x y → φ  {G} {K}(r x ∙ r y))
+        ⁻¹-cong1 :  Congruent₁ (λ x y → sub K (r x) ≈ sub K (r y)) (λ x → φ  {G} {K}(r x ⁻¹))
 
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
@@ -153,24 +154,25 @@
    ; unique = unique
   } where
     open Group H
+    EqH =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
+             (IsGroup.isMonoid isGroup )))
+    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 b
-    h1 (cscong eq t) = h1 t 
+    h1 (coset a b) = f (sub K b)
     h : CosetCarrier G K → Carrier   --  G / K → H
     h r = h1 (isCoset r) 
     _o_ = Group._∙_ G
+    open EqReasoning (Algebra.Group.setoid H )
     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 (φ {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 ⟩
+          h1 (coset a b) ∙ h1 (coset c d)  ∎
     h-homo :  IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) h 
     h-homo = record {
      isMonoidHomomorphism = record {
@@ -180,7 +182,9 @@
         ; ε-homo = {!!} }
        ; ⁻¹-homo = {!!} }
     unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
-    unique x = Algebra.Group.refl H
+    unique x = begin
+         f x ≈⟨ {!!} ⟩
+         f (sub K x ) ∎