ガロア理論の続き

いろいろ面白かった。大半は Agda の流儀に苦労してただけだけど。

　　単純に順列を数え上げてリストにしても全部数え上げたことにはならない

まぁ、そうですよね。結局、concrete な数列表現との bijection (一対一対応)を作らないと。

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

Data.Fin の降順列にしてやると良いらしい。bijection では書きにくいので iso と書いてしまうが、isomorphism は演算の保存も含むので少し違うか。

順列は結局は具体的な数列なので、それが等しければ順列置換としても等しい。つまり、

　　FL-inject : {n : ℕ }　→ {g h : Permutation n n }　→ perm→FL g ≡　perm→FL h → g =p= h

変換した先が等しいなら元が等しいってのは、injection というらしい。これは圏の言葉だと equalizer だな。

もともと圏論はガロア理論から作られたらしいので、同じようなものが出てくるのでわかりやすい。

　　数学は一つ理解すると、他の物も理解しやすくなる

ってやつですね。

5次の対称群が可解でないのいのは、3次の対称群を含むから abc を含むのが反例という風に書けば良いらしい。

　　 counter-example :　¬ (abc 0<3 0<4　=p= pid )
　　 counter-example eq with ←pleq _ _ eq
　　 ...　| ()

　　 end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →　x =p= pid　
　　 end5 x der = end sol x der

abc あると、全部 pid になるという end5 の反例になるってわけ。

　　¬sym5solvable : ¬ ( solvable (Symmetric 5) )
　　¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) )

solvable ならend5 が成立するのだが、それには反例があるみたいにやるわけね。abc は以下の二つで作ります。

　　 dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ }　→ (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
　　　　　→ deriving n (abc i<3 j<4 )
　　 dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ }　→ (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
　　　　　→ deriving n (dba i<3 j<4 )

右向きと左向きがある。deriving は「その対称群が含む部分群の要素を判定する述語」だな。それは data Commutor で書かれていて

P g → P h　→ Commutator P [ g , h ]　この部分が、[ g　, h ] のかっこをしたものという制限になってます。


　　[_,_] :　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

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

uni は不要らしい。gen も交換子の積が必ず交換子になるなら不要だな。

三次の対称群は数え上げて record で書き下しました。20 x 2 。でも、そうすると Agda が死にやすい。停まらない。

いろいろ、bug っぽい挙動も見かけたが、正確に型を書くのが基本らしい。

　　https://github.com/shinji-kono/Galois