Lean4: 環の定義と証明 - Maxima で綴る数学の旅

Mathematics in Lean4を読んでいます。第7章1節で環の定義のあたりを勉強しています。前回は半群、モノイド、群などを定義し、また環の定義に備えて、乗法モノイドの性質を加法群に自動変換する方法なども説明しました。

ここまでくれば環を定義することができます。

class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
/-- Multiplication is left distributive over addition -/
left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
/-- Multiplication is right distributive over addition -/
right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

とてもシンプルです。加法群と乗法モノイド、0をかけると0になる、をベースにして右と左の分配法則を公理として加えたものが環です。

「あれ、加法群は可換のはずだけど、、、」と思ったのは私だけでしょうか。実は環としての定義に加法群の可換は不要です。なぜなら加法群の可換性は証明できるからです。ここでは環Rの加法群が可換であることを次の形で示すことにします。

instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
{ Ring₃.toAddGroup₃ with
add_comm := by -- ⊢ ∀ (a b : R), a + b = b + a

　ここの証明を埋めたい。

証明を埋める必要があるのはadd_comm := byのところです。add_commは（前回や今回の記事では定義を与えていませんが）AddCommGroup₃で定義された∀ (a b : R), a + b = b + aという公理です。環の加法群がこの公理を満たすことを示せばよいわけです。

埋めたものがこちらです。証明の方針は、(1+a)*(1+b)を２通りに展開すること（下記のh2, h3）でh1:1+a+b+a*b=1+b+a+a*bを示し、ここからa+b=b+aを示します。

instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
{ Ring₃.toAddGroup₃ with
add_comm := by -- ⊢ ∀ (a b : R), a + b = b + a
intro a b
have h1 : 1+a+b+a*b = 1+b+a+a*b := by
have h2 : (1+a)*(1+b)=1+b+a+a*b := calc
(1+a)*(1+b)=1*(1+b)+a*(1+b) := by exact Ring₃.right_distrib 1 a (1 + b)
_= 1+b+a*(1+b) := by simp
_= 1+b+a+a*b := by
have: a*(1+b)=a*1+a*b := by exact Ring₃.left_distrib a 1 b
rw [this,add_assoc₃,add_assoc₃,add_assoc₃,]
simp
have h3 : (1+a)*(1+b)=1+a+b+a*b := calc
(1+a)*(1+b)=(1+a)*1+(1+a)*b := by exact Ring₃.left_distrib (1 + a) 1 b
_= 1+a+(1+a)*b := by simp
_= 1+a+b+a*b := by
have: (1+a)*b=1*b+a*b := by exact Ring₃.right_distrib 1 a b
rw [this,add_assoc₃,add_assoc₃,add_assoc₃,]
simp

rw [← h2, ← h3] -- QED of h1.

-- h1 : 1 + a + b + a * b = 1 + b + a + a * b
apply add_right_cancel₃ at h1 -- h1 : 1 + a + b = 1 + b + a
rw [add_assoc₃, add_assoc₃] at h1 -- h1 : 1 + (a + b) = 1 + (b + a)
apply add_left_cancel₃ at h1 -- h1 : a + b = b + a
exact h1
}