🙄

ヨビノリ群論入門③をLean4で形式化 ~ 対称群 ~

2025/03/06に公開

math

この記事について

以下のヨビノリの群論入門③をLean4で形式化していきます。

ヨビノリ群論入門をLean4で形式化の一つです。

Mathlibの実装を参考にしています。

この動画のトピックは対称群と置換や互換についてですが、私がその辺に詳しくないので対称群が群になることを示して終えます。

おまじない

import Mathlib.Tactic
import YobinoriGroupTheoryInLean4.MyGroup
import YobinoriGroupTheoryInLean4.MyBijective

noncomputable section

ファイル名によって自作ファイルもインポートできます。

対称群の定義

まず1以上n以下の自然数の型が必要なのでそれ(MyOmega)を定義します。

structure MyOmega (n : ℕ) where
  val : ℕ
  one_le_val : 1 ≤ val
  val_le_n : val ≤ n

Subtypeを用いて{x : ℕ // 1 ≤ x ∧ x ≤ n}でも良いと思うのですが、各条件に名前がついていた方がいいだろうと思いこうしました。

n次対称群(となるはずだがまだ群であるかはわからない)型SymmGroupも定義します。

structure MySymmGroup (n : ℕ) where
  func : MyOmega n → MyOmega n
  isbij : MyBijective func

この後、全単射に関する定義を使うのでLean4で全単射や逆関数の性質を証明で作った名前空間MyBijectiveを開いておきます。

open MyBijective

対称群用の名前空間内で作業します。

namespace MySymmGroup

対称群が群であることを確認

MyGroupのinstanceを作ることで確認しますが、その前に写像の合成を定義しておきましょう。

def symmgroup_op {n : ℕ} (A : MySymmGroup n) (B : MySymmGroup n) : MySymmGroup n :=
    ⟨A.func ∘ B.func, bij_comp_is_bij B.func A.func B.isbij A.isbij⟩

MySymmGroup nは関数funcとそれが全単射であるという命題isbijを持つので、合成関数を返したかったら合成関数が全単射である証明を組にして返さなくてはなりません。

これを使ってinstanceを作っていきます。

instance {n : ℕ} : MyGroup (MySymmGroup n) where
  op := symmgroup_op
  id_elem := ⟨(fun x ↦ x), idFun_is_bij⟩
  inv A := ⟨inv_bij A.func A.isbij, inv_bij_is_bij A.func A.isbij⟩
  op_assoc A B C := by
    simp only [symmgroup_op, mk.injEq]
    rfl
  op_e A := rfl
  e_op A := rfl
  op_inv A := by
    simp only [symmgroup_op, mk.injEq]
    ext x
    exact inv_bij_is_right_inv A.func A.isbij x

見慣れないmk.injEqは私もよくわかっていませんが、構造体同士の相当をその各メンバ同士の相当に置き換えることができるようです。({A := A1, B := B1} = {A := A2, B := B2}をA1 = A2 ∧ B1 = B2のように)
その上で、前記の例であればメンバ変数BがAに依存する場合、B1 = B2を削除してA1 = A2だけ残すところまでやってくれるようです。

ヨビノリ群論入門③をLean4で形式化 ~ 対称群 ~

この記事について

おまじない

対称群の定義

対称群が群であることを確認

参考文献

Discussion