|
311
|
1 open import Level hiding ( suc ; zero )
|
|
|
2 open import Algebra
|
|
|
3 module sym5h where
|
|
|
4
|
|
|
5 open import Symmetric
|
|
|
6 open import Data.Unit using (⊤ ; tt )
|
|
|
7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
|
|
8 open import Function hiding (flip)
|
|
|
9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
|
|
|
10 open import Data.Nat.Properties
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Data.Empty
|
|
|
13 open import Data.Product
|
|
|
14
|
|
|
15 open import Gutil
|
|
|
16 open import NormalSubgroup
|
|
|
17 open import Putil
|
|
|
18 open import Solvable
|
|
|
19 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
20
|
|
|
21 import Algebra.Morphism.Definitions as MorphismDefinitions
|
|
|
22 open import Algebra.Morphism.Structures
|
|
|
23
|
|
|
24 open import Tactic.MonoidSolver using (solve; solve-macro)
|
|
|
25 import Algebra.Morphism.Definitions as MorphismDefinitions
|
|
|
26 open import Algebra.Morphism.Structures
|
|
|
27
|
|
|
28 open import Data.Fin hiding (_<_ ; _≤_ ; lift )
|
|
|
29 open import Data.Fin.Permutation hiding (_∘ₚ_)
|
|
|
30
|
|
|
31 infixr 200 _∘ₚ_
|
|
|
32 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
|
|
|
33
|
|
|
34 open import Data.List hiding ( [_] )
|
|
|
35 open import nat
|
|
|
36 open import fin
|
|
|
37 open import logic
|
|
|
38 open import FLutil
|
|
|
39 open import Putil
|
|
|
40
|
|
|
41 open _∧_
|
|
|
42
|
|
|
43 ¬sym5solvable : ¬ ( solvable (Symmetric 5) )
|
|
|
44 ¬sym5solvable sol = counter-example (dervied-length sol) (end5 _ (s02 (dervied-length sol))) where
|
|
|
45 --
|
|
|
46 -- dba 1320 d → b → a → d
|
|
|
47 -- (dba)⁻¹ 3021 a → b → d → a
|
|
|
48 -- aec 21430
|
|
|
49 -- (aec)⁻¹ 41032
|
|
|
50 -- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
|
|
|
51 -- so commutator always contains abc, dba and aec
|
|
|
52 -- All stage of Commutator Group of Sym5 contains a sym 3
|
|
|
53 --
|
|
|
54 -- if so, it contains arbitrary 3 different elements of Sym5 as a Sym 3
|
|
|
55 -- sym3' = p ∙ sym3 ∙ p⁻¹
|
|
|
56
|
|
|
57 open _=p=_
|
|
|
58 open ≡-Reasoning
|
|
|
59 open solvable
|
|
|
60 open import Data.Fin.Properties
|
|
|
61
|
|
|
62 -- a group contains Symmetric 3 as a normal subgroup
|
|
|
63
|
|
|
64 record HaveSym3 {c d : Level } (G : Group c d ) : Set (Level.suc c Level.⊔ Level.suc d) where
|
|
|
65 field
|
|
|
66 isSub : SubGroup {d} G
|
|
|
67 G→3 : RawGroup.Carrier (GR (SGroup G isSub)) → Permutation 3 3
|
|
|
68 is-sym3 : IsGroupIsomorphism (GR (SGroup G isSub)) (GR (Symmetric 3)) G→3
|
|
|
69
|
|
|
70 open _=p=_
|
|
|
71 -- Symmetric 3 is a normal subgroup of Symmetric 5
|
|
|
72 s00 : HaveSym3 (Symmetric 5)
|
|
|
73 s00 = record {
|
|
|
74 isSub = sub00
|
|
|
75 ; G→3 = s15
|
|
|
76 ; is-sym3 = ?
|
|
|
77 } where
|
|
|
78 open ≡-Reasoning
|
|
|
79 s10 : Permutation 5 5 → Set
|
|
|
80 s10 perm = (perm ⟨$⟩ˡ (# 0) ≡ # 0) × (perm ⟨$⟩ˡ (# 1) ≡ # 1)
|
|
|
81 s11 : s10 pid
|
|
|
82 s11 = refl , refl
|
|
|
83 s12 : (a : Permutation 5 5) → s10 a → s10 (pinv a)
|
|
|
84 s12 p (eq3 , eq4) = s12a , s12b where
|
|
|
85 s12a : pinv p ⟨$⟩ˡ # 0 ≡ # 0
|
|
|
86 s12a = begin
|
|
|
87 pinv p ⟨$⟩ˡ # 0 ≡⟨ cong (λ k → pinv p ⟨$⟩ˡ k) (sym eq3) ⟩
|
|
|
88 pinv p ⟨$⟩ˡ (p ⟨$⟩ˡ # 0) ≡⟨ inverseʳ p ⟩
|
|
|
89 # 0 ∎
|
|
|
90 s12b : pinv p ⟨$⟩ˡ # 1 ≡ # 1
|
|
|
91 s12b = begin
|
|
|
92 pinv p ⟨$⟩ˡ # 1 ≡⟨ cong (λ k → pinv p ⟨$⟩ˡ k) (sym eq4) ⟩
|
|
|
93 pinv p ⟨$⟩ˡ (p ⟨$⟩ˡ # 1) ≡⟨ inverseʳ p ⟩
|
|
|
94 # 1 ∎
|
|
|
95 s13 : {a b : Permutation 5 5} → a =p= b → s10 a → s10 b
|
|
|
96 s13 {a} {b} eq (eq3 , eq4) = trans (peqˡ (psym eq) (# 0)) eq3 , trans (peqˡ (psym eq) (# 1)) eq4
|
|
|
97 s14 : {a b : Permutation 5 5} → s10 a → s10 b → s10 (a ∘ₚ b)
|
|
|
98 s14 {a} {b} eqa eqb = s14a , s14b where
|
|
|
99 s14a : a ∘ₚ b ⟨$⟩ˡ # 0 ≡ # 0
|
|
|
100 s14a = begin
|
|
|
101 a ∘ₚ b ⟨$⟩ˡ # 0 ≡⟨ cong (λ k → a ⟨$⟩ˡ k) (proj₁ eqb) ⟩
|
|
|
102 a ⟨$⟩ˡ # 0 ≡⟨ proj₁ eqa ⟩
|
|
|
103 # 0 ∎
|
|
|
104 s14b : a ∘ₚ b ⟨$⟩ˡ # 1 ≡ # 1
|
|
|
105 s14b = begin
|
|
|
106 a ∘ₚ b ⟨$⟩ˡ # 1 ≡⟨ cong (λ k → a ⟨$⟩ˡ k) (proj₂ eqb) ⟩
|
|
|
107 a ⟨$⟩ˡ # 1 ≡⟨ proj₂ eqa ⟩
|
|
|
108 # 1 ∎
|
|
|
109 sub00 = record { P = s10 ; Pε = s11 ; P⁻¹ = s12 ; P≈ = s13 ; P∙ = λ {a} {b} → s14 {a} {b} }
|
|
|
110 s15 : Nelm (Symmetric 5) sub00 → Permutation 3 3
|
|
|
111 s15 record { elm = elm ; Pelm = Pelm } = shrink (shrink elm (proj₁ Pelm)) s16 where
|
|
|
112 s16 : shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0 ≡ # 0
|
|
|
113 s16 = begin
|
|
|
114 shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0 ≡⟨ Data.Fin.Properties.suc-injective (
|
|
|
115 suc (shrink elm (proj₁ Pelm) ⟨$⟩ˡ # 0) ≡⟨ ? ⟩
|
|
|
116 elm ⟨$⟩ˡ (suc (# 0)) ≡⟨ proj₂ Pelm ⟩
|
|
|
117 suc (# 0) ∎ ) ⟩
|
|
|
118 # 0 ∎
|
|
|
119 s01 : (i : ℕ ) → HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) i)))
|
|
|
120 s01 zero = ?
|
|
|
121 s01 (suc i) = record {
|
|
|
122 isSub = sub01
|
|
|
123 ; G→3 = s15
|
|
|
124 ; is-sym3 = record {
|
|
|
125 isGroupMonomorphism = record {
|
|
|
126 isGroupHomomorphism = record {
|
|
|
127 isMonoidHomomorphism = record {
|
|
|
128 isMagmaHomomorphism = record {
|
|
|
129 isRelHomomorphism = record { cong = λ {x} {y} eq → ? }
|
|
|
130 ; homo = ? }
|
|
|
131 ; ε-homo = ? }
|
|
|
132 ; ⁻¹-homo = ? }
|
|
|
133 ; injective = λ eq → ? }
|
|
|
134 ; surjective = λ nx → s16 nx , s17 nx }
|
|
|
135 } where
|
|
|
136 sym3 : HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) i)))
|
|
|
137 sym3 = s01 i
|
|
|
138 s10 : Nelm (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i))) → Set
|
|
|
139 s10 record { elm = perm ; Pelm = Pelm } = (perm ⟨$⟩ˡ (# 0) ≡ # 0) × (perm ⟨$⟩ˡ (# 1) ≡ # 1)
|
|
|
140 sub01 : SubGroup (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i))))
|
|
|
141 sub01 = record { P = s10 ; Pε = refl , refl ; P⁻¹ = ? ; P≈ = ? ; P∙ = λ {a} {b} → ? }
|
|
|
142 s15 : Nelm (SGroup (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i)))) sub01 → Permutation 3 3
|
|
|
143 s15 record { elm = record { elm = elm ; Pelm = ic } ; Pelm = Pelm } = shrink (shrink elm (proj₁ Pelm)) ?
|
|
|
144 s16 : Permutation 3 3 → Nelm (SGroup (Symmetric 5) (NormalSubGroup.Psub (CommNormal (Symmetric 5) (suc i)))) sub01
|
|
|
145 s16 abc = record { elm = record { elm = ? ; Pelm = ? } ; Pelm = ? } where
|
|
|
146 dba : Permutation 5 5
|
|
|
147 dba = ?
|
|
|
148 aec : Permutation 5 5
|
|
|
149 aec = ?
|
|
|
150 Cdba : deriving (Symmetric 5) i dba
|
|
|
151 Cdba = ?
|
|
|
152 Caec : deriving (Symmetric 5) i aec
|
|
|
153 Caec = ?
|
|
|
154 s18 : iCommutator (Symmetric 5) (suc i) (pprep (pprep abc))
|
|
|
155 s18 = iunit (ccong ? ( comm Cdba Caec ))
|
|
|
156 s17 : (abc : Permutation 3 3 ) → s15 (s16 abc) =p= abc
|
|
|
157 s17 = ?
|
|
|
158
|
|
|
159
|
|
|
160 -- if Symmetric 0 is a normal subgroup of Commutator Group of Symmetric 5
|
|
|
161 -- the next stagee contains Symmetric 0 as a normal subgroup
|
|
|
162
|
|
|
163 s03 : (i : ℕ) → Permutation 5 5
|
|
|
164 s03 0 = FL→perm (plist→FL (0 ∷ 1 ∷ 0 ∷ 1 ∷ 2 ∷ []))
|
|
|
165 s03 (suc zero) = FL→perm (plist→FL (0 ∷ 1 ∷ 1 ∷ 0 ∷ 2 ∷ []))
|
|
|
166 s03 (suc (suc i)) = s03 i
|
|
|
167
|
|
|
168 s02 : (i : ℕ) → deriving (Symmetric 5) i (s03 i)
|
|
|
169 s02 i = ? where
|
|
|
170 s04 : HaveSym3 (SGroup _ (NormalSubGroup.Psub (CommNormal (Symmetric 5) (dervied-length sol))))
|
|
|
171 s04 = s01 (dervied-length sol)
|
|
|
172
|
|
|
173 -- open Solvable ( Symmetric 5)
|
|
|
174 end5 : (x : Permutation 5 5) → deriving (Symmetric 5) (dervied-length sol) x → x =p= pid
|
|
|
175 end5 x der = end sol x der
|
|
|
176
|
|
|
177 counter-example : (i : ℕ) → ¬ (s03 i =p= pid )
|
|
|
178 counter-example zero eq with ←pleq _ _ eq
|
|
|
179 ... | ()
|
|
|
180 counter-example (suc zero) eq with ←pleq _ _ eq
|
|
|
181 ... | ()
|
|
|
182 counter-example (suc (suc i)) eq = counter-example i eq
|
|
|
183
|
