Mercurial > hg > Members > kono > Proof > galois
view sym4.agda @ 88:405c1f727ffe
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 28 Aug 2020 11:05:45 +0900 (2020-08-28) |
parents | sym3.agda@32004c9a70b1 |
children | d3da6e2c0d90 |
line wrap: on
line source
open import Level hiding ( suc ; zero ) open import Algebra module sym4 where open import Symmetric open import Data.Unit open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) open import Function open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) open import Relation.Nullary open import Data.Empty open import Data.Product open import Gutil open import Putil open import Solvable using (solvable) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Data.Fin open import Data.Fin.Permutation hiding (_∘ₚ_) infixr 200 _∘ₚ_ _∘ₚ_ = Data.Fin.Permutation._∘ₚ_ sym4solvable : solvable (Symmetric 4) solvable.dervied-length sym4solvable = 3 solvable.end sym4solvable x d = solved1 x {!!} where open import Data.List using ( List ; [] ; _∷_ ) open Solvable (Symmetric 4) -- open Group (Symmetric 2) using (_⁻¹) p0 : FL→perm ((# 0) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))) =p= pid p0 = {!!} -- record { peq = p00 } where open _=p=_ -- Klien -- -- 1 (1,2),(3,4) (1,3),(2,4) (1,4),(2,3) -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] , 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] , 2 ∷ 3 ∷ 0 ∷ 1 ∷ [] , 3 ∷ 2 ∷ 1 ∷ 0 ∷ [] , data Klein : (x : Permutation 4 4 ) → Set where kid : Klein pid ka : Klein (pswap (pswap pid)) kb : Klein (pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) ) kc : Klein (pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2})) a0 = pid {4} a1 = pswap (pswap (pid {0})) a2 = pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) a3 = pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2}) -- 1 0 -- 2 1 0 -- 3 2 1 0 k1 : { x : Permutation 4 4 } → Klein x → List ℕ k1 {x} kid = plist x k1 {x} ka = plist x k1 {x} kb = plist x k1 {x} kc = plist x k2 = k1 kid ∷ k1 ka ∷ k1 kb ∷ k1 kc ∷ [] k3 = plist (a1 ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3) ∷ plist (a2 ∘ₚ a1 ) ∷ [] solved1 : (x : Permutation 4 4) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid solved1 = {!!}