# HG changeset patch # User Shinji KONO # Date 1694837657 -32400 # Node ID a067959c1799ca84947cd831fd8235c0ad3cfcdd # Parent 891869ead77511648d632862342aff61dfb4462a check sym5h requires very long time... diff -r 891869ead775 -r a067959c1799 src/sym5h.agda --- 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