Mathematics In Leanから第7章 階層 7.1 基礎の勉強を続けます。
"At this stage we would like to move on to define rings"というあたりで、ここから環を定義していきます。
環を定義するにあたっての課題意識は環の２つの演算である加法群と乗法モノイドでは全ての乗法モノイドの定理は加法群でも成り立つことです。この部分を自動的に行う仕組みが必要になります。
使う道具立てはAdd, AddZero, Mul, MulOne, Neg, InvというLean標準定義済みのクラスです。ちなみに明示的には登場しませんが、これらのクラスの背後にはZeroとかOneという入れ物クラスも定義済みです。
Add 加法演算の入れ物クラス
AddZero 加法演算に単位元があるという属性クラス
Neg 加法演算の逆元の入れ物クラス
Mul 乗法演算の入れ物クラス
MulOne 乗法演算に単位元があるという属性クラス
Inv 乗法演算の逆元の入れ物クラス
これらを使って加法的半群、加法的モノイドを定義してみます。
class AddSemigroup₃ (α : Type) extends Add α where
/-- Addition is associative -/
add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)
class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α
class AddGroup₃ (G : Type) extends AddMonoid₃ G, Neg G where
neg_add : ∀ a : G, -a + a = 0
加法的半群AddSemigroup₃では加法クラスAddを拡張して加法が結合的であることを要請します。また加法的モノイドAddMonoid₃ では加法的半群とAddZeroClassを拡張して加法演算に単位元があることを要請します。さらに加法群AddGroup₃では全ての元に逆元が存在することを要請します。これで加法群の定義は完了です。
次に乗法演算に対する半群、モノイド、群を定義します。その際にto_additiveという仕組みを使うことで加法的半群、加法的モノイド、加法群へのリンクを張ることができます。これによって乗法側から加法側への定義のマッピングが確立します。
@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
/-- Multiplication is associative -/
mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)
@[to_additive AddMonoid₃]
class Monoid₃ (α : Type) extends Semigroup₃ α, MulOneClass α
@[to_additive AddGroup₃]
class Group₃ (G : Type) extends Monoid₃ G, Inv G where
inv_mul : ∀ a : G, a⁻¹ * a = 1
@[to_additive xxx]があること以外は加法演算側の定義と同じです。乗法側の定義から加法側の定義にリンクが@[to_additive xxx]で張ってあります。
ここまで準備してから乗法側で３つの補題を証明します。その際に補題の前にも@[to_additive]をつけると、自動で加法群にこれらの補題が変換されて付け加わります。VSCodeで自動付加された補題を見るには@[to_additive]の前にwhatsnew inをつけてマウスを重ねてください。ポップアップで表示されます。表示の中には変換された証明も表示されます。
@[to_additive (attr := simp)]
lemma Group₃.mul_inv {G : Type} [Group₃ G] {a : G} : a * a⁻¹ = 1 := by
rw [← Group₃.inv_mul a⁻¹]
have inv_inv : a⁻¹⁻¹=a := by
apply inv_eq_of_mul
exact Group₃.inv_mul a
rw [inv_inv]
whatsnew in
@[to_additive]
lemma mul_left_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : a * b = a * c) : b = c := by
have inv_mul_mul : a⁻¹ * (a * b) = a⁻¹ * (a * c) := by
rw [h]
rw [← mul_assoc₃, ← mul_assoc₃] at inv_mul_mul
rw [Group₃.inv_mul a] at inv_mul_mul
rw [one_mul, one_mul] at inv_mul_mul
exact inv_mul_mul
@[to_additive]
lemma mul_right_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : b*a = c*a) : b = c := by
have mul_mul_inv: b*a*a⁻¹=c*a*a⁻¹ := by
rw [h]
rw [mul_assoc₃, mul_assoc₃] at mul_mul_inv
rw [Group₃.mul_inv] at mul_mul_inv
rw [mul_one,mul_one] at mul_mul_inv
exact mul_mul_inv
上記３つの補題は自分で証明したのですが、久しぶりにやると最初の一歩をどうしようかと結構迷います。ゴールを変形して仮定にたどり着いてexactしたいのですが、上記の証明は仮定から同値変形でゴールに辿り着く、ということになっています。証明は正しいのですが自分としては流れはイマイチな感じです。
次回こそ環を定義します。
