Mercurial > hg > Members > kono > Proof > galois

changeset 315:a067959c1799

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
check sym5h requires very long time...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 16 Sep 2023 13:14:17 +0900
parents 891869ead775
children d712d2a1f8bb 77f01da94c4e fff18d4a063b
files src/sym5h.agda
diffstat 1 files changed, 46 insertions(+), 153 deletions(-) [+]
line wrap: on
line diff
--- a/src/sym5h.agda	Sat Sep 16 11:40:13 2023 +0900
+++ b/src/sym5h.agda	Sat Sep 16 13:14:17 2023 +0900
@@ -15,7 +15,7 @@
 open import Gutil 
 open import NormalSubgroup
 open import Putil 
-open import Solvable 
+open import Solvable (Symmetric 5)
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
 import Algebra.Morphism.Definitions as MorphismDefinitions
@@ -40,19 +40,23 @@
 
 open _∧_
 
-¬sym5solvable : ¬ ( solvable (Symmetric 5) )
-¬sym5solvable sol = counter-example (dervied-length sol) (end5 _ (s02 (dervied-length sol))) where
+¬sym5solvable : ¬ ( solvable  )
+¬sym5solvable sol = counter-example (end5 _ (s02 (dervied-length sol))) where
 --
 --    dba       1320      d → b → a → d
 --    (dba)⁻¹   3021      a → b → d → a
 --    aec       21430
 --    (aec)⁻¹   41032
 --    [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
---      so commutator always contains abc, dba and aec
---      All stage of Commutator Group of Sym5 contains a sym 3 
+--
+--    dba = (dc)(cba)(cd) = (dc)(abc)⁻¹(cd)     covariant of (abc)⁻¹
+--    aec = (eb)(abc) (be)                      covariant of abc
 --
---      if so, it contains arbitrary 3 different elements of Sym5 as a Sym 3
---           sym3' = p ∙ sym3 ∙ p⁻¹ 
+--      so commutator always contains abc
+--
+--      this is not true on commutator group because it is finite generated and it may not a commutator
+--      that is even if a commutator group contains abc,  it may not ba commutaor.
+--
 
      open _=p=_
      open ≡-Reasoning
@@ -61,161 +65,50 @@
 
      -- a group contains Symmetric 3 as a normal subgroup
 
-     record HaveSym3 {c d : Level } (G : Group c d ) : Set (Level.suc c Level.⊔ Level.suc d) where
-        field 
-           isSub :  SubGroup {d} G 
-           G→3 :  RawGroup.Carrier (GR (SGroup G isSub)) → Permutation 3 3
-           is-sym3 : IsGroupIsomorphism (GR (SGroup G isSub)) (GR (Symmetric 3)) G→3
+     open _=p=_
 
-     record sym3elms (abc : Permutation 3 3) : Set where 
-        field
-           sa sb sc : ℕ
-           abc=sym3 : plist0 abc ≡ (sa ∷ sb ∷ sc ∷ [])
-
-     sym3→elm : (abc : Permutation 3 3) → sym3elms abc 
-     sym3→elm abc = record { sa = _ ; sb = _ ; sc = _ ; abc=sym3 = refl }   
+     -- d   e   b   c   a
+     -- 0 ∷ 1 ∷ 3 ∷ 4 ∷ 2 ∷ []
+     abc : FL 5
+     abc = (# 0) :: ((# 0) :: ((# 2) :: ((# 0) :: ((# 0 ) :: f0))))
+     abc-test : plist (FL→perm abc) ≡ 0 ∷ 1 ∷ 3 ∷ 4 ∷ 2 ∷ []
+     abc-test = refl
 
-     open _=p=_
-     -- Symmetric 3 is a normal subgroup of Symmetric 5
-     s00 : HaveSym3 (Symmetric 5) 
-     s00 = record {
-           isSub = sub00
-         ; G→3 = s15
-         ; is-sym3 = ?
-        } where
-           open ≡-Reasoning
-           s10 : Permutation 5 5 → Set
-           s10 perm = (perm  ⟨$⟩ˡ (# 0) ≡ # 0) ×  (perm  ⟨$⟩ˡ (# 1) ≡ # 1)
-           s11 : s10 pid
-           s11 = refl , refl 
-           s12 : (a : Permutation 5 5) → s10 a → s10 (pinv a)
-           s12 p (eq3 , eq4) = s12a , s12b where
-               s12a : pinv p ⟨$⟩ˡ # 0 ≡ # 0
-               s12a = begin
-                 pinv p ⟨$⟩ˡ # 0 ≡⟨ cong (λ k → pinv p ⟨$⟩ˡ k) (sym eq3) ⟩
-                 pinv p ⟨$⟩ˡ (p ⟨$⟩ˡ # 0) ≡⟨ inverseʳ p ⟩
-                 # 0 ∎ 
-               s12b : pinv p ⟨$⟩ˡ # 1 ≡ # 1
-               s12b = begin
-                 pinv p ⟨$⟩ˡ # 1 ≡⟨ cong (λ k → pinv p ⟨$⟩ˡ k) (sym eq4) ⟩
-                 pinv p ⟨$⟩ˡ (p ⟨$⟩ˡ # 1) ≡⟨ inverseʳ p ⟩
-                 # 1 ∎ 
-           s13 : {a b : Permutation 5 5} → a =p= b → s10 a → s10 b
-           s13 {a} {b} eq (eq3 , eq4) = trans (peqˡ (psym eq) (# 0)) eq3  , trans (peqˡ (psym eq) (# 1)) eq4  
-           s14 : {a b : Permutation 5 5} → s10 a → s10 b → s10 (a ∘ₚ b)
-           s14 {a} {b} eqa eqb = s14a , s14b where
-               s14a : a ∘ₚ b ⟨$⟩ˡ # 0 ≡ # 0
-               s14a = begin
-                  a ∘ₚ b ⟨$⟩ˡ # 0 ≡⟨ cong (λ k →  a ⟨$⟩ˡ k) (proj₁ eqb) ⟩
-                  a ⟨$⟩ˡ # 0 ≡⟨ proj₁ eqa  ⟩
-                  # 0 ∎
-               s14b : a ∘ₚ b ⟨$⟩ˡ # 1 ≡ # 1
-               s14b = begin
-                  a ∘ₚ b ⟨$⟩ˡ # 1 ≡⟨ cong (λ k →  a ⟨$⟩ˡ k) (proj₂ eqb) ⟩
-                  a ⟨$⟩ˡ # 1 ≡⟨ proj₂ eqa  ⟩
-                  # 1 ∎
-           sub00 = record { P = s10 ; Pε  = s11  ; P⁻¹ = s12 ; P≈ = s13 ; P∙ = λ {a} {b} → s14 {a} {b} }
-           s15 : Nelm (Symmetric 5) sub00 → Permutation 3 3
-           s15 record { elm = elm ; Pelm = Pelm } = shrink (shrink elm (proj₁ Pelm)) s16 where
-               s16 :  shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0 ≡ # 0
-               s16 = begin
-                 shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0 ≡⟨ Data.Fin.Properties.suc-injective (
-                    suc (shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0) ≡⟨ ? ⟩ 
-                    elm  ⟨$⟩ˡ (suc (# 0))  ≡⟨ proj₂ Pelm ⟩ 
-                    suc (# 0) ∎ ) ⟩
-                 # 0 ∎
-     s01 : (i : ℕ ) → HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) i))) 
-     s01 zero = ?
-     s01 (suc i) = record {
-           isSub = sub01
-         ; G→3 = s15
-         ; is-sym3 =  record {
-              isGroupMonomorphism = record {    
-                 isGroupHomomorphism = record {
-                     isMonoidHomomorphism = record {
-                          isMagmaHomomorphism = record {
-                             isRelHomomorphism = record { cong = λ {x} {y} eq → ? }
-                           ; homo = ? }
-                        ; ε-homo = ? }
-                       ; ⁻¹-homo = ?  }
-                   ; injective = λ eq → ? }
-           ;  surjective = λ nx → s16 nx , s17 nx  }
-        } where
+     dc : FL 5
+     dc = (# 4) :: ((# 1) :: ((# 1) :: ((# 1) :: ((# 0 ) :: f0))))
+     dc-test : plist (FL→perm dc) ≡ 4 ∷ 1 ∷ 2 ∷ 3 ∷ 0 ∷ []
+     dc-test = refl
+
+     be : FL 5
+     be = (# 0) :: ((# 2) :: ((# 1) :: ((# 0) :: ((# 0 ) :: f0))))
+     be-test : plist (FL→perm be) ≡ 0 ∷ 3 ∷ 2 ∷ 1 ∷ 4 ∷ []
+     be-test = refl
+
+     s02 : (i : ℕ ) → deriving  i ( FL→perm abc )
+     s02 zero = lift tt
+     s02 (suc i) = s17 where
            -- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
            --    dba = (dc)(cba)(cd) = (dc)(abc)⁻¹(cd) 
            --    aec = (eb)(abc) (be)
-           sym3 : HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) i))) 
-           sym3 = s01 i
-           s10 : Nelm (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i))) → Set
-           s10 record { elm = perm ; Pelm = Pelm } = (perm  ⟨$⟩ˡ (# 0) ≡ # 0) ×  (perm  ⟨$⟩ˡ (# 1) ≡ # 1)
-           sub01 :  SubGroup (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i))))
-           sub01 = record { P = s10 ; Pε  = refl , refl   ; P⁻¹ = ? ; P≈ = ? ; P∙ = λ {a} {b} → ? }
-           s15 : Nelm (SGroup (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i)))) sub01 → Permutation 3 3
-           s15 record { elm = record { elm = elm ; Pelm = ic } ; Pelm = Pelm } = shrink (shrink elm (proj₁ Pelm)) ? 
-           s16 : Permutation 3 3  → Nelm (SGroup (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i)))) sub01
-           s16 abc = record { elm = record { elm = ? ; Pelm = ? } ; Pelm = ? } where
-              ABC : sym3elms abc
-              ABC = sym3→elm abc
-              sa = sym3elms.sa ABC
-              sb = sym3elms.sb ABC
-              sc = sym3elms.sc ABC
-              dc : Permutation 5 5
-              dc = ?
-              eb : Permutation 5 5
-              eb = ?
-              dba : Permutation 5 5
-              dba = dc ∘ₚ (pprep (pprep abc)) ∘ₚ pinv dc
-              aec : Permutation 5 5
-              aec = eb ∘ₚ (pprep (pprep abc)) ∘ₚ pinv eb
-              Cdba : deriving (Symmetric 5) i dba
-              Cdba = Pcomm _ {pprep (pprep abc)} {dc} i s26 where
-                  s22 : Group.Carrier (SGroup _ (HaveSym3.isSub sym3))
-                  s22 = proj₁ (IsGroupIsomorphism.surjective (HaveSym3.is-sym3 sym3) abc)
-                  s23 : HaveSym3.G→3 sym3 s22 =p= abc
-                  s23 = proj₂ (IsGroupIsomorphism.surjective (HaveSym3.is-sym3 sym3) abc)
-                  s24 : deriving (Symmetric 5) i (pprep (pprep abc))
-                  s24 with Nelm.Pelm (Nelm.elm s22 )
-                  ... | t = ?
-                  s25 : SubGroup.P (NormalSubGroup.Psub (CommNormal (Symmetric 5) i)) ?
-                  s25 = ?
-                  s26 : deriving (Symmetric 5) i (pprep (pprep abc))
-                  s26 = ?
-                  -- s22 is finitely generated element from commutor 
-                  -- what we need is a Commutator not iCommutator
-                  -- so this method is no good
-                  s27 : iCommutator (Symmetric 5) i (Nelm.elm (Nelm.elm s22))
-                  s27 = Nelm.Pelm (Nelm.elm s22 )
-                  s28 : SubGroup.P (HaveSym3.isSub sym3) (Nelm.elm s22)
-                  s28 = Nelm.Pelm s22
-              Caec : deriving (Symmetric 5) i aec
-              Caec = Pcomm _ {pinv (pprep (pprep abc))} {eb} i ?
-              s18 :  iCommutator (Symmetric 5) (suc i) (pprep (pprep abc))
-              s18 = iunit (ccong ? ( comm Cdba Caec ))
-           s17 : (abc : Permutation 3 3 ) →  s15 (s16 abc) =p= abc
-           s17 = ?
+           s10 : deriving  i ( FL→perm abc )
+           s10 = s02 i
+           dba : Permutation 5 5
+           dba = FL→perm dc ∘ₚ (pinv (FL→perm  abc) ∘ₚ pinv (FL→perm dc) )
+           aec : Permutation 5 5
+           aec = FL→perm be ∘ₚ (FL→perm abc ∘ₚ pinv (FL→perm be))
+           s12 : abc ≡ perm→FL [ dba , aec ]  
+           s12 = refl
+           s11 : FL→perm abc =p= [ dba , aec ]  
+           s11 = ptrans (pcong-Fp s12 ) (FL←iso _)
+           s17 : deriving  (suc i) ( FL→perm abc )
+           s17 = ccong (psym s11) (comm (Pcomm {_} {FL→perm dc} i (deriving-inv s10)) (Pcomm {_} {FL→perm be} i s10) )
 
 
-     -- if Symmetric 0 is a normal subgroup of Commutator Group of Symmetric 5
-     -- the next stagee contains Symmetric 0 as a normal subgroup
-
-     s03 : (i : ℕ) → Permutation 5 5
-     s03 0 = FL→perm (plist→FL (0 ∷ 1 ∷ 0 ∷ 1 ∷ 2 ∷ []))
-     s03 (suc zero) = FL→perm (plist→FL (0 ∷ 1 ∷ 1 ∷ 0 ∷ 2 ∷ []))
-     s03 (suc (suc i)) = s03 i
-
-     s02 : (i : ℕ) → deriving (Symmetric 5) i (s03 i)
-     s02 i = ? where
-        s04 : HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) (dervied-length sol)))) 
-        s04 = s01 (dervied-length sol)
-
      -- open Solvable ( Symmetric 5) 
-     end5 : (x : Permutation 5 5) → deriving (Symmetric 5) (dervied-length sol) x →  x =p= pid  
+     end5 : (x : Permutation 5 5) → deriving  (dervied-length sol) x →  x =p= pid  
      end5 x der = end sol x der
 
-     counter-example :  (i : ℕ) → ¬ (s03 i  =p= pid )
-     counter-example zero eq with ←pleq _ _ eq
+     counter-example : ¬ ( FL→perm abc  =p= pid )
+     counter-example eq with ←pleq _ _ eq
      ... | ()
-     counter-example (suc zero) eq with ←pleq _ _ eq
-     ... | ()
-     counter-example (suc (suc i)) eq = counter-example i eq