Mathematics In Leanから第7章 階層 7.1 基礎を勉強中です。
ここでは代数構造の階層を構成する方法を知ります。目的はその仕組みの概要を知ることで階層を使えるようになることだそうです。なので完全な理解というよりも主要な言葉や考え方などが理解できれば良いと思います。
実は夏前に7.1 基礎を読んだ時には何をやっているのかいまいちわからず、ちょっと困っていました。夏の暑い間はLean 4はお休みしていたのですが、最近勉強を復活しつつあります。まだ理解が足りていないところが多そうなのですが、まあそこは上記のように割り切って進めることにします。
具体的には7.1では半群、モノイド、群、環を階層の仕組みを使って定義していきます。階層の仕組みとして使う道具はclassとextendsです。
でいきなりデータの入れ物を定義します。定義されたクラスOne₁ は、型$\alpha$には特定の要素oneがあることを定義します。また特に何も属性は定義されていません。またOne₁.oneを短く𝟙と表示し入力できるようにします。
class One₁ (α : Type) where
/-- The element one -/
one : α@[inherit_doc]
notation "𝟙" => One₁.one
同じように(カリー化された)２項演算の入れ物を定義します。定義されたクラスDia₁ には演算要素diaがあります。ここでも特に演算diaに属性は定義されていません。またDia₁ .diaを、短く⋄と表示し入力できるようにします。
class Dia₁ (α : Type) where
dia : α → α → αinfixl:70 " ⋄ " => Dia₁.dia
いよいよちょっと見知った構造を定義します。それは半群(Semigroup)です。半群とは集合に２項演算が定義されていてそれが結合的であることです。クラスDia₁ を拡張し属性として演算diaが結合的であることを定義します。
class Semigroup₂ (α : Type) extends Dia₁ α where
/-- Diamond is associative -/
dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)
（半群のことは忘れて）𝟙が演算⋄の左右単位元であるようなクラスをDiaOneClass₁ として定義します。
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
そしていよいよモノイドを定義します。モノイドは結合的な２項演算と単位元がある集合です。つまり半群でかつ単位元がある、ということです。したがって今までに定義したSemigroup₂ とDiaOneClass₁を使って定義できますね。
class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α
ここまで来れば群を定義するのまであと一歩です。群にあってモノイドにないものを思い出してそれを定義して、class と extendsで継承すればよいのです。次回は群を定義して簡単な命題を証明することにします。
