Mercurial > hg > Members > kono > Proof > galois

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sym5h.agda	Fri Sep 15 21:55:32 2023 +0900
@@ -0,0 +1,183 @@
+open import Level hiding ( suc ; zero )
+open import Algebra
+module sym5h where
+
+open import Symmetric
+open import Data.Unit using (⊤ ; tt )
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function hiding (flip)
+open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
+open import Data.Nat.Properties
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Product
+
+open import Gutil
+open import NormalSubgroup
+open import Putil
+open import Solvable
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+import Algebra.Morphism.Definitions as MorphismDefinitions
+open import Algebra.Morphism.Structures
+
+open import Tactic.MonoidSolver using (solve; solve-macro)
+import Algebra.Morphism.Definitions as MorphismDefinitions
+open import Algebra.Morphism.Structures
+
+open import Data.Fin hiding (_<_ ; _≤_  ; lift )
+open import Data.Fin.Permutation  hiding (_∘ₚ_)
+
+infixr  200 _∘ₚ_
+_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
+
+open import Data.List  hiding ( [_] )
+open import nat
+open import fin
+open import logic
+open import FLutil
+open import Putil
+
+open _∧_
+
+¬sym5solvable : ¬ ( solvable (Symmetric 5) )
+¬sym5solvable sol = counter-example (dervied-length sol) (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
+--
+--      if so, it contains arbitrary 3 different elements of Sym5 as a Sym 3
+--           sym3' = p ∙ sym3 ∙ p⁻¹
+
+     open _=p=_
+     open ≡-Reasoning
+     open solvable
+     open import Data.Fin.Properties
+
+     -- 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=_
+     -- 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
+           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
+              dba : Permutation 5 5
+              dba = ?
+              aec : Permutation 5 5
+              aec = ?
+              Cdba : deriving (Symmetric 5) i dba
+              Cdba = ?
+              Caec : deriving (Symmetric 5) i aec
+              Caec = ?
+              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 = ?
+
+
+     -- 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 der = end sol x der
+
+     counter-example :  (i : ℕ) → ¬ (s03 i  =p= pid )
+     counter-example zero eq with ←pleq _ _ eq
+     ... | ()
+     counter-example (suc zero) eq with ←pleq _ _ eq
+     ... | ()
+     counter-example (suc (suc i)) eq = counter-example i eq
+