Mercurial > hg > Members > kono > Proof > galois

changeset 270:0081e1ed5ead

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
grefl
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 31 May 2022 18:45:43 +0900
parents 0452e7021054
children c209aebeab2a
files src/Fundamental.agda
diffstat 1 files changed, 45 insertions(+), 84 deletions(-) [+]
line wrap: on
line diff
--- a/src/Fundamental.agda	Tue May 31 13:34:40 2022 +0900
+++ b/src/Fundamental.agda	Tue May 31 18:45:43 2022 +0900
@@ -38,43 +38,46 @@
 --  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 a b  → Coset G K a → Coset G K b
+record GSet (G : Group c l) : Set (Level.suc ( c  Level.⊔  l) ) where
+    field
+       def : ( x : Group.Carrier G ) → Set ( c  Level.⊔ l )
+
+open GSet
+
+record _==_ { G :  Group c l } (x y : GSet G ) : Set ( c  Level.⊔  (Level.suc l )) where
+    open Group G
+    field
+       eq→ : {g : Carrier } → def x g → def y g
+       eq← : {g : Carrier } → def y g → def x g
 
 open NormalSubGroup  -- G has at least an element other than ε
 
-φ :   {G : Group c l} →  {K : NormalSubGroup G} → (g x : Group.Carrier G ) → Coset G K x
-φ {G} {K} g x = cscong p01 ( coset (x ∙ (sub K g) ⁻¹ )  g)  where
-   open Group G
-   p01 : x ∙ sub K g ⁻¹ ∙ sub K g ≈ x
-   p01 = begin x ∙ sub K g ⁻¹ ∙ sub K g ≈⟨ assoc x _ _  ⟩
-         x ∙ (  sub K g ⁻¹ ∙ sub K g ) ≈⟨  ∙-cong (grefl G) (proj₁ inverse  _ ) ⟩
-         x ∙ ε ≈⟨ proj₂ identity  _  ⟩
-         x   ∎ where open EqReasoning (Algebra.Group.setoid G )
+record GCoset (G : Group c l)  (K : NormalSubGroup G) (base x : Group.Carrier G ) : Set ( c  Level.⊔  l)  where
+    open Group G
+    field
+       factor : Carrier
+       isCoset : x ≈ base ∙ sub K factor
 
-base1 : {G : Group c l}  {K : NormalSubGroup G} → {x : Group.Carrier G } → Coset G K x → Group.Carrier  G
-base1 {G} {K} {x} (coset a b) = a ⁻¹ ∙ x where open Group G   -- x ≡ a ∙ sub K b
-base1 (cscong x y) = base1 y
+record Coset (G : Group c l)  (K : NormalSubGroup G) : Set ( c  Level.⊔  l)  where
+    open Group G
+    field
+       base : Carrier
 
-base :  {G : Group c l}  {K : NormalSubGroup G} → ( (g : Group.Carrier G )→ Coset G K g)  → Group.Carrier G
-base {G} {K} x = base1 (x ε) where     -- with x ε won't work why?
-    open Group G
+open Coset
 
+φset :   {G : Group c l} →  {K : NormalSubGroup G} → (g : Group.Carrier G ) → GSet G
+φset {G} {K} g = record { def = λ x → GCoset G K g x }
+
+φ :   {G : Group c l} →  {K : NormalSubGroup G} → (g : Group.Carrier G ) → Coset G K
+φ {G} {K} g = record { base = g }
 
 --  Na ∙ Nb = Nab
-mul : {G : Group c l}  {K : NormalSubGroup G} → (x y : (g : Group.Carrier G ) → Coset G K g ) → (g : Group.Carrier G ) → Coset G K g
-mul {G} {K} x y g = φ (base x ∙ base y) g where open Group G
 
-inv : {G : Group c l}  {K : NormalSubGroup G} → ( (g : Group.Carrier G )→ Coset G K g)  → ( (g : Group.Carrier G )→ Coset G K g)
-inv {G} {K} x g = inv1 (x g) where
-    open Group G
-    inv1 : {a : Carrier} → (x : Coset G K a) → Coset G K g
-    inv1 (coset a b) = φ  (a ⁻¹) g 
-    inv1 (cscong eq x) = inv1 x
+mul : {G : Group c l}  {K : NormalSubGroup G} → (x y :  Coset G K ) → Coset G K 
+mul {G} {K} x y  = record { base = base x ∙ base y } where open Group G
 
-COSET : (G : Group c l)  (K : NormalSubGroup G) →  Set ( c  Level.⊔  l )
-COSET G K = (g : Group.Carrier G ) → Coset G K g
+inv : {G : Group c l}  {K : NormalSubGroup G} →  Coset G K   →  Coset G K 
+inv {G} {K} x = record { base  = (base x) ⁻¹ } where open Group G
 
 -- import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 -- open HE
@@ -83,17 +86,17 @@
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
 -- 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 ) (c ⊔ Level.suc l)
 G / K = record {
-     Carrier        = (g : Group.Carrier G ) → Coset G K g
-     ; _≈_          = λ x y → Group._≈_ G (sub K (base x)) (sub K (base y))
+     Carrier        = Coset G K 
+     ; _≈_          = λ x y → φset {G} {K} (base x) == φset {G} {K} (base y)
      ; _∙_          = λ x y → mul x y
-     ; ε            = φ (Group.ε G )
+     ; ε            = record { base = ε }
      ; _⁻¹          = λ x → inv x
      ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record { refl = grefl G ; sym = gsym G ; trans = gtrans G } 
-       ; ∙-cong = λ {x y u v} → cresp {x} {y} {u} {v} }
-       ; assoc = assoc1 }
+       isEquivalence = record { refl = {!!} ; sym = {!!} ; trans = {!!} } 
+       ; ∙-cong = λ {x y u v} → {!!} }
+       ; assoc = {!!} }
        ; identity = {!!} }
        ; inverse   = {!!}
        ; ⁻¹-cong   = λ {x} {y} → {!!}
@@ -102,40 +105,6 @@
       open Group G hiding (refl ; sym ; trans )
       open EqReasoning (Algebra.Group.setoid G)
       open IsGroupHomomorphism (s-homo K )
-      mbase :  {x y : COSET G K} → sub K (base (mul x y)) ≈ sub K (base x ∙ base y)
-      mbase {x} {y} = begin
-              sub K ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙
-                        (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹ ∙
-                         sub K (base1 (x ε) ∙ base1 (y ε)))) ≈⟨  {!!} ⟩
-                         {!!} ≈⟨  ⟦⟧-cong (solve (Algebra.Group.monoid G)) ⟩
-              sub K ( ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙
-                        (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹ )) ∙
-                         (base1 (x ε) ∙ base1 (y ε))) ≈⟨  ⟦⟧-cong ( ∙-cong (
-                     begin (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩
-                     sub K ((base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩
-                     sub K (((base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩
-                     sub K ε ≈⟨ {!!} ⟩
-                     ε  ∎ ) (grefl G) ) ⟩
-                  sub K (ε ∙ (base1 {G} {K} (x ε) ∙ base1 {G} {K} (y ε)))  ≈⟨ {!!} ⟩
-                  sub K (base1 {G} {K} (x ε) ∙ base1 {G} {K} (y ε)) ∎
-      cresp : {x y u v : COSET G K} → sub K (base x) ≈ sub K (base y) → sub K (base u )≈ sub K (base v)
-         → sub K (base (mul x u)) ≈ sub K (base (mul y v))
-      cresp {x} {y} {u} {v} x=y u=v =  begin
-          sub K (base (mul x u)) ≈⟨ {!!} ⟩
-          sub K (base x ∙ base u) ≈⟨ {!!} ⟩
-          sub K (base x ) ∙ sub K (base u) ≈⟨ {!!} ⟩
-          sub K (base y ) ∙ sub K (base v) ≈⟨ {!!} ⟩
-          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 =  begin
-          sub K (base (mul (mul x y ) z)) ≈⟨ {!!} ⟩
-          sub K (base (mul x y ) ∙ base  z) ≈⟨ {!!} ⟩
-          sub K ((base x ∙ base y ) ∙ base  z) ≈⟨ {!!} ⟩
-          sub K (base x ∙ ( base y  ∙ base  z)) ≈⟨ {!!} ⟩
-          sub K (base x ∙ base (mul x  y )) ≈⟨ {!!} ⟩
-          sub K (base (mul x ( mul y z ))) ∎
-        -- crefl1 (coset a b) = ⟦⟧-cong (grefl G) 
 
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
@@ -145,10 +114,10 @@
 record FundamentalHomomorphism (G H : Group c l)  
     (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  Level.⊔  l ) where
+    (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set ( c  Level.⊔ ( Level.suc l) ) where
   open Group H
   field
-    h : COSET G K → Group.Carrier H
+    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 )
 
@@ -162,19 +131,12 @@
    ; 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 a 
-    h1 (cscong a b) = h1 b
-    h : COSET G K → Carrier   --  G / K → H
-    h r = h1 {Group.ε G} (r (Group.ε G))
+    h : Coset G K → Carrier   --  G / K → H
+    h r = f (base r)
     _o_ = Group._∙_ G
     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) {!!} 
+    h03 x y = {!!}
+    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
     h-homo = record {
      isMonoidHomomorphism = record {
           isMagmaHomomorphism = record {
@@ -184,9 +146,8 @@
        ; ⁻¹-homo = {!!} }
     unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
     unique x = begin
-         f x ≈⟨ {!!} ⟩
-         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 )
+         f x ≈⟨ grefl H ⟩
+         h ( φ x ) ∎ where open EqReasoning (Algebra.Group.setoid H )