Mercurial > hg > Members > kono > Proof > galois

changeset 302:3812936d52c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove lift
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 07 Sep 2023 11:45:11 +0900
parents 38f4e5d35c8b
children 061a0fd484c3
files src/NormalSubGroup.agda src/homomorphism.agda
diffstat 2 files changed, 131 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/NormalSubGroup.agda	Thu Sep 07 11:45:11 2023 +0900
@@ -0,0 +1,101 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+open import Level hiding ( suc ; zero )
+module NormalSubgroup  where
+
+open import Algebra
+open import Algebra.Structures
+open import Algebra.Definitions
+open import Data.Product
+open import Relation.Binary.PropositionalEquality 
+open import Algebra.Morphism.Structures
+open import Data.Empty
+open import Relation.Nullary
+
+open GroupMorphisms
+
+GR : {c l : Level } → Group c l → RawGroup c l
+GR G = record {
+     Carrier        = Carrier G
+     ; _≈_          = _≈_ G
+     ; _∙_          = _∙_ G
+     ; ε            = ε G
+     ; _⁻¹          = _⁻¹ G
+  } where open Group
+
+record GAxiom {c l : Level } (G : Group c l)  : Set ( c  Level.⊔  l ) where
+  open Group G
+  field
+     ∙-cong :  {x y u v : Carrier } → x ≈ y → u ≈ v →  x ∙ u ≈  y ∙ v 
+     assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈  x ∙ ( y ∙ z )
+     identity : ((y : Carrier) → ε ∙ y ≈ y ) ×  ((y : Carrier) → y ∙ ε ≈ y )
+     inverse   : ((y : Carrier) → y ⁻¹ ∙ y  ≈ ε ) ×  ((y : Carrier) → y ∙ y ⁻¹  ≈ ε )
+     ⁻¹-cong   : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹
+
+GA : {c l : Level } → (G : Group c l) → GAxiom G
+GA G = record {
+        ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)))
+     ;  assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))
+     ;  identity = IsMonoid.identity ( IsGroup.isMonoid isGroup)
+     ;  inverse   = IsGroup.inverse isGroup
+     ;  ⁻¹-cong   = IsGroup.⁻¹-cong isGroup
+   } where open Group G
+
+open import Relation.Binary.Structures
+
+Eq : {c l : Level } → (G : Group c l) → IsEquivalence _
+Eq G =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
+             (IsGroup.isMonoid (Group.isGroup G ))) )
+
+_<_∙_> : {c d : Level} (m : Group c d )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
+m < x ∙ y > =  Group._∙_ m x y
+
+_<_≈_> : {c d : Level} (m : Group c d )  →    (f  g : Group.Carrier m ) → Set d
+m < x ≈ y > =  Group._≈_ m x y
+
+infixr 9 _<_∙_>
+
+-- assuming Homomorphism is too strong
+--
+record NormalSubGroup {l c d : Level} (A : Group c d )  : Set (Level.suc (l Level.⊔ (c Level.⊔ d))) where
+   open Group A
+   field                           
+       P : Carrier  → Set l
+       Pε : P ε
+       P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
+       P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
+       P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
+       -- gN ≈ Ng
+       Pcomm : {a b : Carrier  }  → P a  →  P ( b ∙  ( a  ∙ b ⁻¹ ) )
+
+import Relation.Binary.Reasoning.Setoid as EqReasoning
+
+record Nelm {c d : Level} {A : Group c d } (n : NormalSubGroup {d} A) : Set  (Level.suc c ⊔ d)  where
+   open Group A
+   open NormalSubGroup n 
+   field                           
+       elm : Carrier
+       Pelm : P elm
+
+NGroup : {c d : Level} {A : Group c d } (n : NormalSubGroup A) → Group  (Level.suc c ⊔ d)  d
+NGroup {_} {_} {A} n = record {
+      Carrier        = Nelm n
+    ; _≈_            = λ x y → elm x ≈ elm y
+    ; _∙_            = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) }
+    ; ε              = record { elm = ε ; Pelm = Pε }
+    ; _⁻¹            = λ x → record { elm = (elm x) ⁻¹  ; Pelm = P⁻¹ (elm x) (Pelm x) }
+    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
+       isEquivalence = record { refl = IsEquivalence.refl (IsGroup.isEquivalence ga) 
+          ; sym =  IsEquivalence.sym (IsGroup.isEquivalence ga) 
+          ; trans = IsEquivalence.trans (IsGroup.isEquivalence ga)  }
+       ; ∙-cong = IsGroup.∙-cong ga }
+       ; assoc = λ a b c → IsGroup.assoc ga (elm a) (elm b) (elm c) }
+       ; identity = ( (λ q → proj₁ (IsGroup.identity ga) (elm q)) , (λ q → proj₂ (IsGroup.identity ga) (elm q)) ) }
+       ; inverse = ( (λ q → proj₁ (IsGroup.inverse ga) (elm q)) , (λ q → proj₂ (IsGroup.inverse ga) (elm q)) ) 
+       ; ⁻¹-cong   = IsGroup.⁻¹-cong ga }
+   }  where
+       open Group A
+       open NormalSubGroup n 
+       open Nelm 
+       ga = Group.isGroup A
+
+
--- a/src/homomorphism.agda	Thu Sep 07 10:51:30 2023 +0900
+++ b/src/homomorphism.agda	Thu Sep 07 11:45:11 2023 +0900
@@ -51,7 +51,7 @@
 -- Set of a ∙ ∃ n ∈ N
 --
 
-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
+data IsaN  {c d : Level} {A : Group c d }  (N : NormalSubGroup {d} 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 {c d : Level} {A : Group c d }  (N : NormalSubGroup A )  (a b : Group.Carrier A)  : Set (Level.suc c ⊔ d) where
@@ -59,7 +59,7 @@
         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 {c d : Level} (A : Group c d) (N : NormalSubGroup A  ) where
+module AN {c d : Level} (A : Group c d) (N : NormalSubGroup {d} A  ) where
     open Group A
     open NormalSubGroup N
     open EqReasoning (Algebra.Group.setoid A)
@@ -231,8 +231,8 @@
                  a ∎
 
 -- K ⊂ ker(f)
-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 : {c d : Level} (G H : Group c d)  (K : NormalSubGroup {d} G ) (f : Group.Carrier G → Group.Carrier H ) 
+   → Set (c ⊔ d)
 K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε   where
   open Group H
   open NormalSubGroup K
@@ -311,8 +311,8 @@
 
     Imf : NormalSubGroup G 
     Imf = record {
-          P = λ x → Lift (Level.suc c ⊔ d) (f x ≈ ε)
-        ; Pε = lift ε-homo 
+          P = λ x → f x ≈ ε
+        ; Pε = ε-homo 
         ; P⁻¹ = im01
         ; P≈ = im02
         ; P∙ = im03
@@ -320,54 +320,59 @@
        } 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
+           im01 : (a : Group.Carrier G) → f a ≈ ε → f ((G Group.⁻¹) a) ≈ ε
+           im01 a fa=e = 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
+           im02 : {a b : GC} → G < a ≈ b > → f a ≈ ε → f b ≈ ε
+           im02 {a} {b} a=b fa=e = begin
               f b ≈⟨ ⟦⟧-cong (GU.gsym a=b) ⟩
               f a ≈⟨ fa=e  ⟩
-              ε ∎ ) where
+              ε ∎  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
+           im04 :  {a b : Group.Carrier G} → f a ≈ ε → 
+                f ((G Group.∙ b) ((G Group.∙ a) ((G Group.⁻¹) b))) ≈ ε
+           im04 {a} {b} fa=e = 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
+               ε ∎  
+           im03 : {a b : Group.Carrier G} → f a ≈ ε → f b ≈ ε →
+                f ((G Group.∙ a) b) ≈ ε
+           im03 {a} {b} fa=e fb=e = begin
               f (G < a ∙ b > ) ≈⟨ homo _ _ ⟩
               f a ∙ f b  ≈⟨ ∙-cong fa=e fb=e ⟩
               ε ∙ ε  ≈⟨ proj₁ identity _ ⟩
-              ε ∎ ) 
+              ε ∎ 
+
+    h05 : Group _ _
+    h05 = G / Imf 
 
     h : Group.Carrier (G / K ) → Group.Carrier H
-    h r = f ( GK.inv-φ G K r )
+    h r = f r
     h03 : (x y : Group.Carrier (G / K ) ) →  h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
-    h03 = ?
+    h03 x y = homo _ _
+    h04 : {x y : Group.Carrier G} → aNeq K x y → h x ≈ h y 
+    h04 {x} {y} x=y = ?
     h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
     h-homo = record {
      isMonoidHomomorphism = record {
           isMagmaHomomorphism = record {
-             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} }
+             isRelHomomorphism = record { cong = λ {x} {y} eq → h04 eq  }
            ; homo = h03 }
-        ; ε-homo = {!!} }
-       ; ⁻¹-homo = {!!} }
+        ; ε-homo = ε-homo }
+       ; ⁻¹-homo = ⁻¹-homo }
     is-solution : (x : Group.Carrier G)  →  f x ≈ h ( GK.φ ? ? x )
     is-solution x = begin
          f x ≈⟨ ? ⟩