ガロア理論

中学生の時にガロアの夢とか読まされたが、あやうく数学嫌いになるところだったような。アルティンの方が良いが、今は数学ガールがあるから。

順列やってたのは、このためなんだけど。割と話は簡単で、

xの多項式は

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

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

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

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

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

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

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

　αγβ = αβγ

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

　γβ=βγ

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

　 β⁻¹ γ⁻¹ βγ= e

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

すったもんだしたんですが、2次まではできた。でも、これ、ちょっと順列でやるにはきついな。

lemma4 : (g h : Carrier ) → [ h , g ] ≈ [ g , h ] ⁻¹
lemma4 g h = begin
　　　 [ h , g ]　　　　　　　　　　　　　　　 ≈⟨ grefl ⟩
　　　 (h ⁻¹ ∙ g ⁻¹ ∙　 h ) ∙ g　　　　　　　　≈⟨ assoc _ _ _ ⟩
　　　 h ⁻¹ ∙ g ⁻¹ ∙　(h ∙ g)　　　　　　　　　≈⟨ ∙-cong grefl (gsym (∙-cong lemma6 lemma6))　⟩
　　　 h ⁻¹ ∙　g ⁻¹ ∙ ((h ⁻¹) ⁻¹ ∙ (g ⁻¹) ⁻¹)　≈⟨　∙-cong grefl (lemma5 _ _ )　⟩
　　　 h ⁻¹ ∙　g ⁻¹ ∙　(g ⁻¹ ∙ h ⁻¹) ⁻¹　　　　≈⟨ assoc _ _ _ ⟩
　　　 h ⁻¹ ∙ (g ⁻¹ ∙　(g ⁻¹ ∙ h ⁻¹) ⁻¹)　　　 ≈⟨ ∙-cong grefl (lemma5 (g ⁻¹ ∙ h ⁻¹ ) g ) ⟩
　　　 h ⁻¹ ∙ (g ⁻¹ ∙　 h ⁻¹ ∙ g) ⁻¹　　　　　 ≈⟨ lemma5 (g ⁻¹ ∙ h ⁻¹ ∙ g) h ⟩
　　　 (g ⁻¹ ∙ h ⁻¹ ∙　 g ∙ h) ⁻¹　　　　　　　≈⟨ grefl ⟩
　　　 [ g , h ]　⁻¹　　　　　　　　　
　　 ∎ where open EqReasoning (Algebra.Group.setoid G)

ってな感じ。

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