群にあってモノイドにないものは、、、そう、逆元です。モノイドにはすでに演算があり単位元があり演算は結合的でした。そこに全ての元に逆元があれば群になるわけです。
一旦前回までに定義した道具立てを再掲しておきます。
class Semigroup₂ (α : Type) extends Dia₁ α where
/-- Diamond is associative -/
dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)
class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where
/-- One is a left neutral element for diamond. -/
one_dia : ∀ a : α, 𝟙 ⋄ a = a
/-- One is a right neutral element for diamond -/
dia_one : ∀ a : α, a ⋄ 𝟙 = a
class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α
逆元を定義します。まずは入れ物クラスInv₁を定義します。Inv₁.invは関数で、⁻¹ で入力したり出力したり出来るようにします。
class Inv₁ (α : Type) where
/-- The inversion function -/
inv : α → α@[inherit_doc]
postfix:max "⁻¹" => Inv₁.inv
Monoid₁ クラスと上記のInv₁ クラスを拡張して群を定義します。その群の定義としてInv₁.invが演算diaに関する左逆元の属性を満たすことを要請します。
class Group₁ (G : Type) extends Monoid₁ G, Inv₁ G where
inv_dia : ∀ a : G, a⁻¹ ⋄ a = 𝟙
ここからいきなり群論を始めることができます。目標は左逆元は実は右逆元でもあることの証明です。その前に上記の定義の部分(DiaOneClass₁.one_diaとかInv₁.invとか)が証明で使うには長いのでクラス名を省いて使えるようにします。
export DiaOneClass₁ (one_dia dia_one)
export Semigroup₁ (dia_assoc)
export Group₁ (inv_dia)
最初に１つ補題を示します。
lemma left_inv_eq_right_inv₁ {M : Type} [Monoid₁ M] {a b c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
rw [← one_dia c, ← hba, dia_assoc, hac, dia_one b]
もう１つ補題を示します。
lemma inv_eq_of_dia [Group₁ G] {a b : G} (h : a ⋄ b = 𝟙) : a⁻¹ = b := by
apply left_inv_eq_right_inv₁
apply inv_dia
apply h
ここまでくれば左逆元が右逆元であることを示せます。
lemma dia_inv [Group₁ G] (a : G) : a ⋄ a⁻¹ = 𝟙 := by
rw [← inv_dia a⁻¹]
have inv_inv : a⁻¹⁻¹=a := by
apply inv_eq_of_dia
exact inv_dia a
rw [inv_inv]
ちょっとまとめます。classを使って入れ物を定義したり、その入れ物が満たすべき属性を定義します。その属性がいわゆる公理になっていて証明で使うことができます。そしてclassを組み合わせてより複雑なclass (Monoid₁やGroup₁など)を定義することができます。
