|
68
|
1 open import Level hiding ( suc ; zero )
|
|
|
2 open import Algebra
|
|
88
|
3 module sym4 where
|
|
68
|
4
|
|
|
5 open import Symmetric
|
|
|
6 open import Data.Unit
|
|
|
7 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
|
|
8 open import Function
|
|
|
9 open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
|
|
|
10 open import Relation.Nullary
|
|
|
11 open import Data.Empty
|
|
|
12 open import Data.Product
|
|
|
13
|
|
|
14 open import Gutil
|
|
|
15 open import Putil
|
|
|
16 open import Solvable using (solvable)
|
|
|
17 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
18
|
|
|
19 open import Data.Fin
|
|
88
|
20 open import Data.Fin.Permutation hiding (_∘ₚ_)
|
|
68
|
21
|
|
88
|
22 infixr 200 _∘ₚ_
|
|
|
23 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
|
|
|
24
|
|
|
25 sym4solvable : solvable (Symmetric 4)
|
|
|
26 solvable.dervied-length sym4solvable = 3
|
|
|
27 solvable.end sym4solvable x d = solved1 x {!!} where
|
|
68
|
28
|
|
70
|
29 open import Data.List using ( List ; [] ; _∷_ )
|
|
|
30
|
|
88
|
31 open Solvable (Symmetric 4)
|
|
68
|
32 -- open Group (Symmetric 2) using (_⁻¹)
|
|
|
33
|
|
70
|
34 open _=p=_
|
|
88
|
35
|
|
|
36 -- Klien
|
|
|
37 --
|
|
|
38 -- 1 (1,2),(3,4) (1,3),(2,4) (1,4),(2,3)
|
|
|
39 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] , 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] , 2 ∷ 3 ∷ 0 ∷ 1 ∷ [] , 3 ∷ 2 ∷ 1 ∷ 0 ∷ [] ,
|
|
|
40
|
|
|
41
|
|
|
42 data Klein : (x : Permutation 4 4 ) → Set where
|
|
|
43 kid : Klein pid
|
|
|
44 ka : Klein (pswap (pswap pid))
|
|
|
45 kb : Klein (pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) )
|
|
|
46 kc : Klein (pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2}))
|
|
|
47
|
|
|
48 a0 = pid {4}
|
|
|
49 a1 = pswap (pswap (pid {0}))
|
|
|
50 a2 = pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 )
|
|
|
51 a3 = pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2})
|
|
|
52
|
|
|
53 -- 1 0
|
|
|
54 -- 2 1 0
|
|
|
55 -- 3 2 1 0
|
|
|
56
|
|
|
57 k1 : { x : Permutation 4 4 } → Klein x → List ℕ
|
|
|
58 k1 {x} kid = plist x
|
|
|
59 k1 {x} ka = plist x
|
|
|
60 k1 {x} kb = plist x
|
|
|
61 k1 {x} kc = plist x
|
|
|
62
|
|
|
63 k2 = k1 kid ∷ k1 ka ∷ k1 kb ∷ k1 kc ∷ []
|
|
|
64 k3 = plist (a1 ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3) ∷ plist (a2 ∘ₚ a1 ) ∷ []
|
|
111
|
65
|
|
|
66 p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
|
|
|
67 p0id = pleq _ _ refl
|
|
|
68
|
|
127
|
69 -- stage 1 (A4)
|
|
|
70 p0 = (zero :: zero :: zero :: zero :: f0 )
|
|
|
71 p1 = (zero :: suc zero :: suc zero :: zero :: f0 )
|
|
|
72 p2 = (zero :: suc (suc zero) :: zero :: zero :: f0 )
|
|
|
73 p3 = (suc zero :: zero :: suc zero :: zero :: f0 )
|
|
|
74 p4 = (suc zero :: suc zero :: zero :: zero :: f0 )
|
|
|
75 p5 = (suc zero :: suc (suc zero) :: suc zero :: zero :: f0 )
|
|
|
76 p6 = (suc (suc zero) :: zero :: zero :: zero :: f0 )
|
|
|
77 p7 = (suc (suc zero) :: suc zero :: suc zero :: zero :: f0 )
|
|
|
78 p8 = (suc (suc zero) :: suc (suc zero) :: zero :: zero :: f0 )
|
|
|
79 p9 = (suc (suc (suc zero)) :: zero :: suc zero :: zero :: f0 )
|
|
|
80 pa = (suc (suc (suc zero)) :: suc zero :: zero :: zero :: f0 )
|
|
|
81 pb = (suc (suc (suc zero)) :: suc (suc zero) :: suc zero :: zero :: f0 )
|
|
|
82
|
|
|
83 t0 = plist (FL→perm p0 ) ∷ plist (FL→perm p1 ) ∷ plist (FL→perm p2 ) ∷ plist (FL→perm p3 ) ∷ plist (FL→perm p4 ) ∷ plist (FL→perm p5 ) ∷
|
|
|
84 plist (FL→perm p6 ) ∷ plist (FL→perm p7 ) ∷ plist (FL→perm p8 ) ∷ plist (FL→perm p9 ) ∷ plist (FL→perm pa ) ∷ plist (FL→perm pb ) ∷ []
|
|
111
|
85
|
|
127
|
86 t1 : List (FL 4) → List (FL 4)
|
|
|
87 t1 x = tl2 x x [] where
|
|
|
88 tl3 : (FL 4) → ( z : List (FL 4)) → List (FL 4) → List (FL 4)
|
|
|
89 tl3 h [] w = w
|
|
|
90 tl3 h (x ∷ z) w = tl3 h z (( perm→FL [ FL→perm h , FL→perm x ] ) ∷ w )
|
|
|
91 tl2 : ( x z : List (FL 4)) → List (FL 4) → List (FL 4)
|
|
|
92 tl2 [] _ x = x
|
|
|
93 tl2 (h ∷ x) z w = tl2 x z (tl3 h z w)
|
|
|
94
|
|
|
95 stage1 : List (FL 4)
|
|
|
96 stage1 = t1 ( ∀-FL 3 )
|
|
|
97
|
|
|
98 -- stage2 ( Kline )
|
|
|
99 -- k0 p0 zero :: zero :: zero :: zero :: f0 ∷ (0 ∷ 1 ∷ 2 ∷ 3 ∷ []) ∷
|
|
|
100 -- k1 p3 suc zero :: zero :: suc zero :: zero :: f0 ∷ (1 ∷ 0 ∷ 3 ∷ 2 ∷ []) ∷
|
|
|
101 -- k2 p8 suc (suc zero) :: suc (suc zero) :: zero :: zero :: f0 ∷ (2 ∷ 3 ∷ 0 ∷ 1 ∷ [])
|
|
|
102 -- k3 pb suc (suc (suc zero)) :: suc (suc zero) :: suc zero :: zero :: f0 ∷ (3 ∷ 2 ∷ 1 ∷ 0 ∷ [])
|
|
|
103
|
|
|
104 tb = plist ( FL→perm p0) ∷ plist ( FL→perm p3) ∷ plist ( FL→perm p8) ∷ plist ( FL→perm pb) ∷ []
|
|
|
105
|
|
|
106 stage2 : List (FL 4)
|
|
|
107 stage2 = t1 ( p0 ∷ p1 ∷ p2 ∷ p3 ∷ p4 ∷ p5 ∷ p6 ∷ p7 ∷ p8 ∷ p9 ∷ pa ∷ pb ∷ [] )
|
|
70
|
108
|
|
88
|
109 solved1 : (x : Permutation 4 4) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
|
|
70
|
110 solved1 = {!!}
|
