Mercurial > hg > Members > kono > Proof > galois

changeset 265:1dbe1f357569

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 09:49:12 +0900
parents c4458b479a0f
children e6f9eb2bfc78
files src/Fundamental.agda
diffstat 1 files changed, 28 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/src/Fundamental.agda	Tue May 31 08:47:46 2022 +0900
+++ b/src/Fundamental.agda	Tue May 31 09:49:12 2022 +0900
@@ -28,8 +28,6 @@
 --    G/K
 --
 
--- open import Relation.Binary.Structures
--- open import Relation.Binary.Morphism.Structures
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
 open HomoMorphism
@@ -43,7 +41,6 @@
     cscong : {a b : Group.Carrier G } → Group._≈_ G a b  → Coset G K a → Coset G K b
 
 open NormalSubGroup  -- G has at least an element other than ε
--- open import Relation.Binary.Structures
 
 φ :   {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
@@ -54,26 +51,18 @@
          x ∙ ε ≈⟨ proj₂ identity  _  ⟩
          x   ∎ where open EqReasoning (Algebra.Group.setoid G )
 
+base1 : {G : Group c l}  {K : NormalSubGroup G} → {x : Group.Carrier G } → Coset G K x → Group.Carrier  G
+base1 {G} (coset a b) = a ⁻¹ ∙ b where open Group G
+base1 (cscong x y) = base1 y
+
 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
-    base1 : {x : Carrier} → Coset G K x → Carrier 
-    base1 (coset a b) = a ⁻¹ ∙ b 
-    base1 (cscong x y) = base1 y
 
 --  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
 
--- ceq : {G : Group c l } {K : NormalSubGroup G}  → {a b : Group.Carrier G } → (x : Coset G K a) (y : Coset G K b) → Set l
--- ceq {G} {K} (coset a b) (coset a₁ b₁) = Group._≈_ G (sub K b ) (sub K b₁)
--- ceq (coset a b) (cscong eq y) = ceq (coset a b) y
--- ceq (cscong eq x) (coset a b) = ceq x (coset a b)
--- ceq (cscong eqx x) (cscong eqy y) = ceq x y
-
--- _==_ : {G : Group c l}  {K : NormalSubGroup G} → (x y : (g : Group.Carrier G ) → Coset G K g ) → Set l
--- _==_ {G}  {K} x y = ceq (x ε) (y ε) 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
@@ -87,18 +76,21 @@
 -- import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 -- open HE
 
+import Axiom.Extensionality.Propositional
+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 ) ( c  Level.⊔  l )
+_/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) l
 G / K = record {
      Carrier        = (g : Group.Carrier G ) → Coset G K g
-     ; _≈_          = λ x y → x ≡ y
+     ; _≈_          = λ x y → Group._≈_ G (sub K (base x)) (sub K (base y))
      ; _∙_          = λ x y → mul x y
      ; ε            = φ (Group.ε G )
      ; _⁻¹          = λ x → inv x
      ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 
-       ; ∙-cong = λ {x y u v} → cresp }
-       ; assoc = {!!} }
+       isEquivalence = record { refl = grefl G ; sym = gsym G ; trans = gtrans G } 
+       ; ∙-cong = λ {x y u v} → cresp {x} {y} {u} {v} }
+       ; assoc = assoc1 }
        ; identity = {!!} }
        ; inverse   = {!!}
        ; ⁻¹-cong   = λ {x} {y} → {!!}
@@ -107,10 +99,22 @@
       open Group G hiding (refl ; sym ; trans )
       open EqReasoning (Algebra.Group.setoid G)
       open IsGroupHomomorphism (s-homo K )
-      cresp : {x y u v : COSET G K} → x ≡ y → u ≡ v → mul x u ≡ mul y v
-      cresp {x} {y} {u} {v} refl refl = refl
-      assoc1 : {x y z  : COSET G K} → mul x ( mul y z ) ≡ mul (mul x y ) z
-      assoc1 = {!!}
+      mbase :  {x y : COSET G K} → base (mul x y) ≈ sub K (base x ∙ base y)
+      mbase {x} {y} = mbase1 (x ε) (y ε) where
+         mbase1 : {a b : Carrier } → Coset G K a → Coset G K b → base (mul x y) ≈ sub K (base x ∙ base y)
+         mbase1 (coset a b) (coset a₁ b₁) = begin
+             (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε)) ≈⟨ {!!} ⟩
+             (sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε)) ≈⟨ {!!} ⟩
+             (sub K (base1 (x ε) ∙ base1 (y ε))) ∙ (base1 (x ε) ∙ base1 (y ε)) ≈⟨ {!!} ⟩
+             sub K (base1 (x ε) ∙ base1 (y ε)) ∎
+         mbase1 (coset a b) (cscong x t) = mbase1 (coset a b) t
+         mbase1 (cscong eq s) (coset a b) = mbase1 s (coset a b)
+         mbase1 (cscong eqs s) (cscong eqt t) = mbase1 s t
+      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 = {!!}
+      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
         -- crefl1 (coset a b) = ⟦⟧-cong (grefl G) 
 
 -- K ⊂ ker(f)