Mercurial > hg > Members > kono > Proof > galois

changeset 274:691b2ee844ef

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 Thu, 26 Jan 2023 01:16:38 +0900
parents 9bee24b4017f
children 33d248c9081e
files src/Fundamental.agda
diffstat 1 files changed, 76 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/src/Fundamental.agda	Tue Jan 24 23:38:32 2023 +0900
+++ b/src/Fundamental.agda	Thu Jan 26 01:16:38 2023 +0900
@@ -70,35 +70,17 @@
 
 open import Tactic.MonoidSolver using (solve; solve-macro)
 
-qadd : (A : Group c c ) (N  : NormalSubGroup A ) → (f g : (x : Group.Carrier A  )  → aN N x ) → (x : Group.Carrier A  )  → aN N x
-qadd A N  f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where
-       open Group A
-       open aN
-       open NormalSubGroup N
-       open IsGroupHomomorphism normal 
-       q00 : ( x ⁻¹ ∙  a (f x) ∙ a (g x)  ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈ x
-       q00 = begin 
-          ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩
-          x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧  ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩
-          x ⁻¹ ∙ (a (f x) ∙ ((a (g x)  ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl A) (∙-cong (grefl A) (∙-cong comm (grefl A) ))  ⟩
-          x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧  ∙ a (g x)) ∙ ⟦ n (g x) ⟧ ))  ≈⟨ solve monoid ⟩
-          x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ )  ≈⟨ ∙-cong (grefl A) (aN=x (g x)  ) ⟩
-          x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x   ≈⟨ ∙-cong (∙-cong (grefl A) (aN=x (f x))) (grefl A)  ⟩
-          (x ⁻¹ ∙ x ) ∙ x   ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl A)  ⟩
-          ε ∙ x  ≈⟨ solve monoid  ⟩
-          x ∎ where 
-            open EqReasoning (Algebra.Group.setoid A)
 
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
     Carrier  = (x : Group.Carrier A  ) → aN N x
     ; _≈_      = _=n=_
-    ; _∙_      = qadd A N
-    ; ε        = λ x → record { a = x  ; n = ε  ; x=aN = ?  }
-    ; _⁻¹      = λ f x → record { a = x ∙ ⟦ n (f x) ⟧  ⁻¹  ; n = n (f x)  ; x=aN = ?  }
+    ; _∙_      = qadd 
+    ; ε        = qid
+    ; _⁻¹      = qinv
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
        isEquivalence = record {refl = grefl A  ; trans = ? ; sym = ? }
-       ; ∙-cong = ? }
+       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v {w} → qcong {x} {y} {u} {v} x=y u=v {w} }
        ; assoc = ? }
        ; identity =  idL , (λ q → ? )  }
        ; inverse   = ( (λ x → ? ) , (λ x → ? ))  
@@ -109,53 +91,93 @@
        open aN
        open NormalSubGroup N
        open IsGroupHomomorphism normal 
+       open EqReasoning (Algebra.Group.setoid A)
        _=n=_ : (f g : (x : Group.Carrier A  )  → aN N x ) →  Set c
        f =n= g = {x : Group.Carrier A  } → ⟦ n (f x) ⟧  ≈ ⟦ n (g x) ⟧  
+       qadd : (f g : (x : Group.Carrier A  )  → aN N x ) → (x : Group.Carrier A  )  → aN N x
+       qadd f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where
+           q00 : ( x ⁻¹ ∙  a (f x) ∙ a (g x)  ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈ x
+           q00 = begin 
+              ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩
+              x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧  ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩
+              x ⁻¹ ∙ (a (f x) ∙ ((a (g x)  ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl A) (∙-cong (grefl A) (∙-cong comm (grefl A) ))  ⟩
+              x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧  ∙ a (g x)) ∙ ⟦ n (g x) ⟧ ))  ≈⟨ solve monoid ⟩
+              x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ )  ≈⟨ ∙-cong (grefl A) (aN=x (g x)  ) ⟩
+              x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x   ≈⟨ ∙-cong (∙-cong (grefl A) (aN=x (f x))) (grefl A)  ⟩
+              (x ⁻¹ ∙ x ) ∙ x   ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl A)  ⟩
+              ε ∙ x  ≈⟨ solve monoid  ⟩
+              x ∎ 
        qid : ( x : Carrier ) → aN N x
-       qid x = record { a = x  ; n = ε  ; x=aN = ?  }
-       idL : (f : (x  : Carrier )→  aN N x) → (qadd A N qid f ) =n= f 
+       qid x = record { a = x  ; n = ε  ; aN=x = qid1 } where
+           qid1 : x ∙ ⟦ ε ⟧ ≈ x
+           qid1 = begin
+              x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl A) ε-homo ⟩
+              x ∙ ε  ≈⟨ solve monoid ⟩
+              x ∎ 
+       qinv : (( x : Carrier ) → aN N x) → ( x : Carrier ) → aN N x
+       qinv f x = record { a = x ∙ ⟦ n (f x) ⟧  ⁻¹  ; n = n (f x)  ; aN=x = qinv1  } where
+             qinv1 : x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈ x
+             qinv1 = begin
+              x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
+              x ∙ ⟦ (n (f x)) ⁻¹ ⟧  ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
+              x ∙ ⟦ ((n (f x)) ⁻¹ )  ∙ n (f x) ⟧ ≈⟨ ? ⟩
+              x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl A) ε-homo ⟩
+              x ∙ ε  ≈⟨ solve monoid ⟩
+              x ∎ 
+       qcong :  { x y u v : (x₁ : Carrier) → aN N x₁ } → (x=y : x =n= y) ( u=v : u =n= v ) →  qadd x u =n= qadd y v
+       qcong {x} {y} {u} {v} x=y u=v {w} = begin
+              ⟦ n (x w) ∙ n (u w) ⟧  ≈⟨ homo _ _ ⟩
+              ⟦ n (x w) ⟧ ∙ ⟦ n (u w) ⟧  ≈⟨ ∙-cong x=y u=v ⟩
+              ⟦ n (y w) ⟧ ∙ ⟦ n (v w) ⟧  ≈⟨ gsym A ( homo _ _) ⟩
+              ⟦ n (y w) ∙ n (v w) ⟧  ∎ 
+       idL : (f : (x  : Carrier )→  aN N x) → (qadd qid f ) =n= f 
        idL f = ?
 
-
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c c)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c
 K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε   where
   open Group H
   open NormalSubGroup K
 
-φ : (G : Group c c)  (K : NormalSubGroup G) → Group.Carrier G → Group.Carrier (G / K )
-φ G K g x = record { a = x ; n = ε ; aN=x = ? } where
-  open Group G
-  open NormalSubGroup K
-
-φ-homo : (G : Group c c)  (K : NormalSubGroup G) → IsGroupHomomorphism (GR G) (GR (G / K)) (φ G K)
-φ-homo = ?
-
 open import Function.Surjection
 open import Function.Equality
 
-φe : (G : Group c c)  (K : NormalSubGroup G) → (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
-φe G K = record { _⟨$⟩_ = φ G K   ; cong = φ-cong  }  where
-       open Group G
-       open aN
-       open NormalSubGroup K
-       open IsGroupHomomorphism normal 
-       φ-cong : {f g : Carrier } → f ≈ g  → {x : Carrier } →  ⟦ n (φ G K f x ) ⟧ ≈ ⟦ n (φ G K g x ) ⟧ 
-       φ-cong = ?
+module _ (G : Group c c) (K : NormalSubGroup G) where
+    open Group G
+    open aN
+    open NormalSubGroup K
+    open IsGroupHomomorphism normal 
+    open EqReasoning (Algebra.Group.setoid G)
+
+    φ : Group.Carrier G → Group.Carrier (G / K )
+    φ g x = record { a = g  ; n = g ⁻¹ ∙ x ; aN=x = ? } where
+        gk00 :  g ∙ ⟦ ? ⟧ ≈ x
+        gk00 = ?
+
+    φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ 
+    φ-homo = record {⁻¹-homo = λ g → ?  ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
+       record { cong = ? } }}}
 
-inv-φ : (G : Group c c)  (K : NormalSubGroup G) → Group.Carrier (G / K ) → Group.Carrier G
-inv-φ = ?
+    φe : (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
+    φe = record { _⟨$⟩_ = φ ; cong = φ-cong  }  where
+           φ-cong : {f g : Carrier } → f ≈ g  → {x : Carrier } →  ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ 
+           φ-cong = ?
+
+    inv-φ : Group.Carrier (G / K ) → Group.Carrier G
+    inv-φ f = ⟦ n (f ε) ⟧ 
 
-φ-surjective : (G : Group c c)  (K : NormalSubGroup G) → Surjective (φe G K )
-φ-surjective G K = record { from = record { _⟨$⟩_ = inv-φ G K ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse } where
-       open Group G
-       open aN
-       open NormalSubGroup K
-       open IsGroupHomomorphism normal 
-       cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ G K f ≈ inv-φ G K g
-       cong-i = ?
-       is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ G K (inv-φ G K f) y) ⟧ ≈ ⟦ n (f y) ⟧
-       is-inverse = ?
+    cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g
+    cong-i = ?
+
+    is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧
+    is-inverse f {y} = begin
+       ⟦ n (φ (inv-φ f) y) ⟧  ≈⟨ ? ⟩
+       ⟦ n (φ (n (f ε)) y) ⟧  ≈⟨ ? ⟩
+       ⟦ ε ⟧  ≈⟨ ? ⟩
+       ⟦ n (f y) ⟧ ∎ 
+
+    φ-surjective : Surjective φe 
+    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse } where
  
 record FundamentalHomomorphism (G H : Group c c )
     (f : Group.Carrier G → Group.Carrier H ) 
@@ -182,7 +204,7 @@
     open Group H
     h : Group.Carrier (G / K ) → Group.Carrier H
     h r = f ( aN.n (r (Group.ε G )  ))
-    h03 : (x y : Group.Carrier (G / K ) ) →  h ( qadd G K x y ) ≈ h x ∙ h y
+    h03 : (x y : Group.Carrier (G / K ) ) →  h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
     h03 x y = {!!}
     h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
     h-homo = record {