Mercurial > hg > Members > kono > Proof > galois
comparison sym4.agda @ 88:405c1f727ffe
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 28 Aug 2020 11:05:45 +0900 |
| parents | sym3.agda@32004c9a70b1 |
| children | d3da6e2c0d90 |
comparison
equal
deleted
inserted
replaced
| 87:c68956f6c3ad | 88:405c1f727ffe |
|---|---|
| 1 open import Level hiding ( suc ; zero ) | |
| 2 open import Algebra | |
| 3 module sym4 where | |
| 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 | |
| 20 open import Data.Fin.Permutation hiding (_∘ₚ_) | |
| 21 | |
| 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 | |
| 28 | |
| 29 open import Data.List using ( List ; [] ; _∷_ ) | |
| 30 | |
| 31 open Solvable (Symmetric 4) | |
| 32 -- open Group (Symmetric 2) using (_⁻¹) | |
| 33 | |
| 34 p0 : FL→perm ((# 0) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))) =p= pid | |
| 35 p0 = {!!} -- record { peq = p00 } where | |
| 36 | |
| 37 open _=p=_ | |
| 38 | |
| 39 -- Klien | |
| 40 -- | |
| 41 -- 1 (1,2),(3,4) (1,3),(2,4) (1,4),(2,3) | |
| 42 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] , 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] , 2 ∷ 3 ∷ 0 ∷ 1 ∷ [] , 3 ∷ 2 ∷ 1 ∷ 0 ∷ [] , | |
| 43 | |
| 44 | |
| 45 data Klein : (x : Permutation 4 4 ) → Set where | |
| 46 kid : Klein pid | |
| 47 ka : Klein (pswap (pswap pid)) | |
| 48 kb : Klein (pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) ) | |
| 49 kc : Klein (pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2})) | |
| 50 | |
| 51 a0 = pid {4} | |
| 52 a1 = pswap (pswap (pid {0})) | |
| 53 a2 = pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) | |
| 54 a3 = pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2}) | |
| 55 | |
| 56 -- 1 0 | |
| 57 -- 2 1 0 | |
| 58 -- 3 2 1 0 | |
| 59 | |
| 60 k1 : { x : Permutation 4 4 } → Klein x → List ℕ | |
| 61 k1 {x} kid = plist x | |
| 62 k1 {x} ka = plist x | |
| 63 k1 {x} kb = plist x | |
| 64 k1 {x} kc = plist x | |
| 65 | |
| 66 k2 = k1 kid ∷ k1 ka ∷ k1 kb ∷ k1 kc ∷ [] | |
| 67 k3 = plist (a1 ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3) ∷ plist (a2 ∘ₚ a1 ) ∷ [] | |
| 68 | |
| 69 solved1 : (x : Permutation 4 4) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid | |
| 70 solved1 = {!!} |