Mercurial > hg > Members > kono > Proof > galois

comparison sym3.agda @ 70:32004c9a70b1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sym2 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Aug 2020 22:37:21 +0900
parents sym5.agda@fb1ccedf5853
children 405c1f727ffe
comparison
equal deleted inserted replaced
69:fb1ccedf5853 70:32004c9a70b1
1 open import Level hiding ( suc ; zero )
2 open import Algebra
3 module sym3 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
21
22 sym3solvable : solvable (Symmetric 3)
23 solvable.dervied-length sym3solvable = 2
24 solvable.end sym3solvable x d = solved1 x d where
25
26 open import Data.List using ( List ; [] ; _∷_ )
27
28 open Solvable (Symmetric 3)
29 -- open Group (Symmetric 2) using (_⁻¹)
30
31 p0 : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid
32 p0 = record { peq = p00 } where
33 p00 : (q : Fin 3) → (FL→perm ((# 0) :: ((# 0) :: ((# 0) :: f0))) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
34 p00 zero = refl
35 p00 (suc zero) = refl
36 p00 (suc (suc zero)) = refl
37
38 open _=p=_
39
40 solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
41 solved1 = {!!}