Mercurial > hg > Members > kono > Proof > galois

changeset 301:38f4e5d35c8b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Imf
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 07 Sep 2023 10:51:30 +0900
parents 3ca1d0e379d0
children 3812936d52c8
files src/homomorphism.agda
diffstat 1 files changed, 68 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/homomorphism.agda	Wed Sep 06 16:10:44 2023 +0900
+++ b/src/homomorphism.agda	Thu Sep 07 10:51:30 2023 +0900
@@ -1,9 +1,11 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 -- fundamental homomorphism theorem
 --
 
+module homomorphism where
+
 open import Level hiding ( suc ; zero )
-module homomorphism (c d : Level) where
-
 open import Algebra
 open import Algebra.Structures
 open import Algebra.Definitions
@@ -49,15 +51,15 @@
 -- Set of a ∙ ∃ n ∈ N
 --
 
-data IsaN  {A : Group c d }  (N : NormalSubGroup A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where
+data IsaN  {c d : Level} {A : Group c d }  (N : NormalSubGroup A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where
     an : (n x : Group.Carrier A ) →  A < A < a ∙ n > ≈ x > → (pn : NormalSubGroup.P N n) → IsaN N a x
 
-record aNeq {A : Group c d }  (N : NormalSubGroup A )  (a b : Group.Carrier A)  : Set (Level.suc c ⊔ d) where
+record aNeq {c d : Level} {A : Group c d }  (N : NormalSubGroup A )  (a b : Group.Carrier A)  : Set (Level.suc c ⊔ d) where
     field
         eq→  : {x : Group.Carrier A}  → IsaN N a x → IsaN N b x
         eq←  : {x : Group.Carrier A}  → IsaN N b x → IsaN N a x
 
-module AN (A : Group c d) (N : NormalSubGroup A  ) where
+module AN {c d : Level} (A : Group c d) (N : NormalSubGroup A  ) where
     open Group A
     open NormalSubGroup N
     open EqReasoning (Algebra.Group.setoid A)
@@ -140,7 +142,7 @@
     anxn=yn {x} {y} {n} x=y pn with ayxi x=y pn
     ... | an n₁ .((A Group.∙ x) n) eq1 pn₁ = gsym eq1
 
-_/_ : (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
+_/_ : {c d : Level} (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
 _/_ A N  = record {
     Carrier  = Group.Carrier A
     ; _≈_      = aNeq N
@@ -229,7 +231,7 @@
                  a ∎
 
 -- K ⊂ ker(f)
-K⊆ker : (G H : Group c d)  (K : NormalSubGroup G ) (f : Group.Carrier G → Group.Carrier H ) 
+K⊆ker : {c d : Level} (G H : Group c d)  (K : NormalSubGroup G ) (f : Group.Carrier G → Group.Carrier H ) 
    → Set (Level.suc c ⊔ d)
 K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε   where
   open Group H
@@ -238,7 +240,7 @@
 open import Function.Surjection
 open import Function.Equality
 
-module GK (G : Group c d) (K : NormalSubGroup G  ) where
+module GK {c d : Level} (G : Group c d) (K : NormalSubGroup G  ) where
     open Group G
     open NormalSubGroup K
     open EqReasoning (Algebra.Group.setoid G)
@@ -248,13 +250,13 @@
     gkε : Group.Carrier (G / K)
     gkε = Group.ε (G / K) 
 
-    φ : Group.Carrier G → Group.Carrier (G / K )
+    φ : Group.Carrier G → Group.Carrier (G / K )  -- a → aN
     φ g = g
 
     φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
     φ-homo = record {⁻¹-homo = λ x → aneq grefl ; isMonoidHomomorphism = record { ε-homo = aneq grefl
            ; isMagmaHomomorphism = record { homo = λ x y → aneq grefl ; isRelHomomorphism =
-       record { cong = λ eq → aneq eq } }}} where
+       record { cong = λ eq → aneq eq } }}} 
 
 
     φe : (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
@@ -262,8 +264,8 @@
           gk40 : {i j : Carrier} → i ≈ j → (G / K ) < φ i ≈ φ j >
           gk40 {i} {j} i=j = aneq i=j
 
-    inv-φ : Group.Carrier (G / K ) → Carrier 
-    inv-φ x = ?
+    inv-φ : Group.Carrier (G / K ) → Carrier   -- P (inv-ψ x)
+    inv-φ x = x
 
     φ-surjective : Surjective φe
     φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → gk50 f g }
@@ -277,7 +279,7 @@
     gk01 = ?
 
 
-record FundamentalHomomorphism (G H : Group c d )
+record FundamentalHomomorphism {c d : Level} (G H : Group c d )
     (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 (Level.suc c ⊔ d) where
@@ -290,11 +292,11 @@
     unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
        → ( (x : Group.Carrier G)  →  f x ≈ h1 ( GK.φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
 
-FundamentalHomomorphismTheorm : (G H : Group c d)
+FundamentalHomomorphismTheorm : {c d : Level} (G H : Group c d)
     (f : Group.Carrier G → Group.Carrier H )
-    (homo : IsGroupHomomorphism (GR G) (GR H) f )
-    (K : NormalSubGroup G  ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f homo K kf
-FundamentalHomomorphismTheorm G H f homo K kf = record {
+    (f-homo : IsGroupHomomorphism (GR G) (GR H) f )
+    (K : NormalSubGroup G  ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f f-homo K kf
+FundamentalHomomorphismTheorm {c} {d} G H f f-homo K kf = record {
      h = h
    ; h-homo = h-homo
    ; is-solution = is-solution
@@ -304,8 +306,56 @@
     open Group H
     open Gutil H
     -- open NormalSubGroup K ?
-    open IsGroupHomomorphism homo
+    open IsGroupHomomorphism f-homo
     open EqReasoning (Algebra.Group.setoid H)
+
+    Imf : NormalSubGroup G 
+    Imf = record {
+          P = λ x → Lift (Level.suc c ⊔ d) (f x ≈ ε)
+        ; Pε = lift ε-homo 
+        ; P⁻¹ = im01
+        ; P≈ = im02
+        ; P∙ = im03
+        ; Pcomm = im04
+       } where
+           open NormalSubGroup K
+           GC = Group.Carrier G
+           im01 : (a : Group.Carrier G) → Lift (Level.suc c ⊔ d) (f a ≈ ε) → Lift (Level.suc c ⊔ d) (f ((G Group.⁻¹) a) ≈ ε)
+           im01 a (lift fa=e) = lift (begin
+               f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _  ⟩
+               f a ⁻¹  ≈⟨ ⁻¹-cong fa=e ⟩
+               ε ⁻¹  ≈⟨ gsym ε≈ε⁻¹ ⟩
+               ε ∎  )
+           im00 : (a : GC) → f a ≈ ε  → f ((G Group.⁻¹) a) ≈ ε
+           im00 a fa=e = begin 
+              f ((G Group.⁻¹) a) ≈⟨ ⁻¹-homo _ ⟩  
+              f a ⁻¹ ≈⟨ ⁻¹-cong fa=e ⟩  
+              ε ⁻¹  ≈⟨ gsym ε≈ε⁻¹ ⟩  
+              ε  ∎ 
+           im02 : {a b : GC} → G < a ≈ b > → Lift (Level.suc c ⊔ d) (f a ≈ ε) → Lift (Level.suc c ⊔ d) (f b ≈ ε)
+           im02 {a} {b} a=b (lift fa=e) = lift ( begin
+              f b ≈⟨ ⟦⟧-cong (GU.gsym a=b) ⟩
+              f a ≈⟨ fa=e  ⟩
+              ε ∎ ) where
+               open import Gutil G as GU
+           im04 :  {a b : Group.Carrier G} → Lift (Level.suc c ⊔ d) (f a ≈ ε) → Lift (Level.suc c ⊔ d)
+                (f ((G Group.∙ b) ((G Group.∙ a) ((G Group.⁻¹) b))) ≈ ε)
+           im04 {a} {b} (lift fa=e) = lift ( begin
+               f ( G < b ∙ G < a ∙ (G Group.⁻¹) b > > ) ≈⟨ homo _ _ ⟩
+               f  b ∙ f ( G < a ∙ (G Group.⁻¹) b >  ) ≈⟨ cdr (homo _ _) ⟩
+               f  b ∙ ( f a ∙ f ((G Group.⁻¹) b )) ≈⟨ cdr (cdr (⁻¹-homo _))  ⟩
+               f  b ∙ ( f a ∙ f b ⁻¹ ) ≈⟨ cdr (car fa=e) ⟩
+               f  b ∙ ( ε ∙ f b ⁻¹ ) ≈⟨ solve monoid ⟩
+               f  b ∙ f b ⁻¹ ≈⟨ proj₂ inverse _ ⟩
+               ε ∎ ) 
+           im03 : {a b : Group.Carrier G} → Lift (Level.suc c ⊔ d) (f a ≈ ε) → Lift (Level.suc c ⊔ d) (f b ≈ ε) →
+                Lift (Level.suc c ⊔ d) (f ((G Group.∙ a) b) ≈ ε)
+           im03 {a} {b} (lift fa=e) (lift fb=e) = lift (begin
+              f (G < a ∙ b > ) ≈⟨ homo _ _ ⟩
+              f a ∙ f b  ≈⟨ ∙-cong fa=e fb=e ⟩
+              ε ∙ ε  ≈⟨ proj₁ identity _ ⟩
+              ε ∎ ) 
+
     h : Group.Carrier (G / K ) → Group.Carrier H
     h r = f ( GK.inv-φ G K r )
     h03 : (x y : Group.Carrier (G / K ) ) →  h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y