Mercurial > hg > Members > kono > Proof > galois
view Solvable.agda @ 5:92a164e1f6b6
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 16 Aug 2020 22:08:46 +0900 |
parents | 121213cfc85a |
children | c1b3c25d7cef |
line wrap: on
line source
open import Level hiding ( suc ; zero ) open import Algebra module Solvable {n m : Level} (G : Group n m ) where open import Data.Unit open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) open import Data.Nat using (ℕ; suc; zero) open import Relation.Nullary open import Data.Empty open import Data.Product open import Relation.Binary.PropositionalEquality hiding ( [_] ) open Group G [_,_] : Carrier → Carrier → Carrier [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where uni : Commutator P ε gen : {f g h : Carrier} → P g → P h → Commutator P f → Commutator P ( f ∙ [ g , h ] ) ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m) deriving 0 x = Lift (Level.suc n ⊔ m) ⊤ deriving (suc i) x = Commutator (deriving i) x -- deriving stage is closed on multiplication and inversion deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y → deriving i ( x ∙ y ) deriving-mul {zero} {x} {y} (lift tt) (lift tt) = lift tt deriving-mul {suc i} {ε} {ε} uni uni = ccong (Algebra.Group.sym G (proj₁ identity ε)) uni deriving-mul {suc i} {ε} {_} uni (gen x x₁ iy) = ccong (Algebra.Group.sym G (proj₁ identity _)) (gen x x₁ iy) deriving-mul {suc i} {_} {ε} (gen x x₁ ix) uni = ccong (Algebra.Group.sym G (proj₂ identity _)) (gen x x₁ ix) deriving-mul {suc i} {_} {_} (gen x x₁ ix) (gen x₂ x₃ iy) = ccong {!!} (gen x₂ x₃ (gen x x₁ iy)) deriving-mul {suc i} {_} {_} _ _ = {!!} deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ ) deriving-inv {i} {x} ix = ? record Solvable : Set (Level.suc n ⊔ m) where field dervied-length : ℕ end : (x : Carrier ) → deriving dervied-length x → x ≈ ε