-title: ガロア理論

xの多項式は 

　 (x - α)(x - β)(x - γ)

の形だとαβγを置換しても同じ式になります。

なので多項式には順列の群である対称群が対応することになります。

　 f x => (x - α)(g x)

の変換は、f xの対称群からg xの対称群への変換になるわけ。具体的には三次の対称群から二次の対称群だな。

三次の対称群、つまり三つの数の入れ替えは、αβγはγ..と.γ.と..γからなるわけですが、

三次式を二次式に変換できるなら、αβγとβαγの二つの形にならないとおかしい。つまり、

　αγβ = αβγ

とγを移動できる必要がある。ということは、

　γβ=βγ

でないとダメ。逆元をかけて

　 β γ βh = e

になれば良い。左辺が交換子というのだけど、これを繰り返し作って e になれば解ける。5次だと解けないってわけ。

--対称群

   Data.Fin.Permutation

というのがあるので、それを使う

    -- Data.Fin.Permutation.id
    pid : {p : ℕ } → Permutation p p
    pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }

    -- Data.Fin.Permutation.flip
    pinv : {p : ℕ } → Permutation p p → Permutation p p
    pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }

    record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
        field
           peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q

という感じで簡単に逆元と単位元が求まる。

    Symmetric : ℕ → Group  Level.zero Level.zero

という形で簡単に群になる。

--交換子群

交換子は積に閉じてないので生成する必要がある。

    [_,_] :  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 ε
      comm  : {g h : Carrier} → P g → P h  → Commutator P [ g , h ] 
      gen   : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙  g  )
      ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g

Commutator は Symmetric Group の部分群を P : Carrier → Set (Level.suc n ⊔ m)) で定義している。
Set を返す関数は要素が存在するかどうかを判定する。

これを繰り返すのが次の述語。これも Set (Level.suc n ⊔ m) を返してる。つまり証明するべき命題を返すような関数。

    deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
    deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
    deriving (suc i) x = Commutator (deriving i) x 


これを

    record solvable : Set (Level.suc n ⊔ m) where
      field 
         dervied-length : ℕ
         end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε  

dervied-length 回繰り返すと、単位元のみになる群を可解群という。方程式に対応する群が可解群の時に方程式は代数解を持つ。

--Permutation

有限な自然数

    Fin 

というのを使う。これの一対一対応 Bijection が Permutation になる。

関数なので見えない。もっと具体的なものはないのか? 単なるリストでも良いのだが、

　同じ数字が入らない
　長さが固定

などの制約が入らない。

--Permutatioに対応するデータ構造

やっていけば良いのだが割と面倒。Permutation を以下の data 構造に対応させる。

    data  FL : (n : ℕ )→ Set where
       f0 :  FL 0 
       _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)

Fin の減少列になる。最初の挿入の選択肢はゼロ、次は一つ、次は二つなどとなる。

       ((# 3) :: ((# 1) :: ((# 0 ) :: f0))) 

このListに大小関係を入れる。

    data _f<_  : {n : ℕ } (x : FL n ) (y : FL n)  → Set  where
       f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn →   (xn :: xt) f< ( yn :: yt )
       f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt →   (xn :: xt) f< ( xn :: yt )

--Fresh List

各要素の大小関係がすべて入っている sort された List 。これを使うと重複要素を排除できる。

<center><img src="fig/fresh.svg"></center>

  data List# : Set (a ⊔ r)
  fresh : (a : A) (as : List#) → Set r

  data List# where
    []   : List#
    cons : (a : A) (as : List#) → fresh a as → List#

  infixr 5 _∷#_
  pattern _∷#_ x xs = cons x xs _

  fresh a []        = ⊤
  fresh a (x ∷# xs) = R a x × fresh a xs

これを使うと

FList : {n : ℕ } → Set
FList {n} = List# (FL n) ⌊ _f<?_ ⌋

    fr1 : FList
    fr1 =
       ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
       ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) ∷# 
       ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) ∷# 
       []

などとできる。

--Fresh List insert

    fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1

とできれば。

    FLinsert : {n : ℕ } → FL n → FList {n}  → FList {n}
    FLinsert {zero} f0 y = f0 ∷# []
    FLinsert {suc n} x [] = x ∷# []
    FLinsert {suc n} x (cons a y x₁) with total x a
    ... | inj₁ (case1 eq) = cons a y x₁
    FLinsert {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( Level.lift (ttf<  lt ) , ttf a y  x₁) where
       ttf : (a : FL (suc n)) → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
       ttf a [] fr = Level.lift tt
       ttf a (cons a₁ y x1) (lift lt1 , _ ) = (Level.lift (ttf< {!!} )) , ttf a₁ y x1
    ... | inj₂ (case1 eq) = cons a y x₁
    ... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!}

--Permuation の数え上げ

全部のPermutationをListにする。全部入っていることをデータ構造として表す

  data Any : List# A R → Set (p ⊔ a ⊔ r) where
    here  : ∀ {x xs pr} → P x → Any (cons x xs pr)
    there : ∀ {x xs pr} → Any xs → Any (cons x xs pr)

ここにある、あそこにあるみたいな感じ。

    AnyFList : (n : ℕ )  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)

が示せれば、∀Flist fmax に全部の FL n が入っていることがわかる。

--数え上げの方法

    Flist1 :  {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n)
    Flist1 zero i<n [] _ = []
    Flist1 zero i<n (a ∷# x ) z  = FLinsert ( zero :: a ) (Flist1 zero i<n x z )
    Flist1 (suc i) (s≤s i<n) [] z  = Flist1 i (Data.Nat.Properties.<-trans i<n a<sa) z z 
    Flist1 (suc i) i<n (a ∷# x ) z  = FLinsert ((fromℕ< i<n ) :: a ) (Flist1 (suc i) i<n x z )

    ∀Flist : {n : ℕ } → FL n → FList n
    ∀Flist {zero} f0 = f0 ∷# [] 
    ∀Flist {suc n} (x :: y)  = Flist1 n a<sa (∀Flist y) (∀Flist y)   

しかし、Any を示しにくい。あと、もう少しだが...

    fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n 
    fsuc {n} (x :: y) (f<n lt) = fromℕ< fsuc1 :: y where
        fsuc1 : suc (toℕ x) < n
        fsuc1 =  Data.Nat.Properties.≤-trans (s≤s lt) ( s≤s ( toℕ≤pred[n] (fromℕ< a<sa)) )
    fsuc (x :: y) (f<t lt) = x :: fsuc y lt

この時に、x f< fsuc x が成立する。

    ∀Flist' : (n : ℕ ) → FList n
    ∀Flist' n = ∀Flist0' n n FL0 {!!} where
       ∀Flist0' : (i j : ℕ) → (x : FL n) → x f< fmax → FList n
       ∀Flist0' zero zero x _ = []
       ∀Flist0' zero (suc j) x lt = ∀Flist0' j j fmax {!!}
       ∀Flist0' (suc i) j x lt = cons (fsuc x lt) (∀Flist0' i j (fsuc x lt) {!!} ) {!!}

なのだが、fsuc は最大を越えないことを示す必要がある。めんどい。

--coinduction?

   record  CFresh {n : ℕ } (i : Size) : Set  where
      coinductive
      field
         δ : ∀{j : Size< i} → (y : FL n) → CFresh {n} j 
         -- δ : ∀{j : Size< i} → (y : FL n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ y x) → CFresh {n} j (cons y x xr)
   
   open CFresh
   ∀CF : ∀{i} {n : ℕ } → FL n → CFresh {n} i ?
   δ (∀CF x) y fr = {!!}

良くわからん。