lean4上の代数

lean4上の代数

Some Definitions

$\alpha$が$\rm{Type}\ \mathit{u}$の型を持つ時、$\rm{Mul}\ \alpha$で$\alpha$は積を持つということは既知とします。ここで$u$はuniverseです。
　この時$\alpha$は（推移律すら満たすと限らない）積を持つマグマとなります。

Semigroup

半群とは、推移律を満たす積を持つマグマのことです。

      /- ### Semigroups -/
class Semigroup (G : Type u) extends Mul G where
  mul_assoc (a b c : G) : (a * b) * c = a * (b * c)
lemma mul_assoc {G : Type u} [Semigroup G] :
    ∀ a b c : G, (a * b) * c = a * (b * c) :=
  Semigroup.mul_assoc
    

Monoid

モノイド（亜群）とは、単位元を持つ半群のことです。

      /- ### prerequires -/
class One (α : Type u) where
  one : α
notation "e" => One.one

/- ### Monoids -/
class Monoid (M : Type u) extends Semigroup M, One M where
  mul_one (m : M) : m * e = m
  one_mul (m : M) : e * m = m
@[simp] lemma mul_one {M : Type u} [Monoid M] : ∀ (m : M), m * e = m :=
  Monoid.mul_one
@[simp] lemma one_mul {M : Type u} [Monoid M] : ∀ (m : M), e * m = m :=
  Monoid.one_mul
    

Group

群とは、逆元対応を持つモノイドのことです。
　新しく追加される情報は逆元対応と、それが逆元である性質です。
　モノイド$G$に対し、逆元対応を$\iota:G\to G$とする時、逆元対応逆元の性質は

$a * \iota(a) = e,\ \ \iota(a) * a = e$
　の2種類ですが実際には片方のみを公理に含めれば十分です。後ほど示します。

      /- ### prerequires -/
class Inv (α : Type u) where
  inv : α → α
postfix:max "⁻¹" => Inv.inv

/- ### Groups -/
class Group (G : Type u) extends Monoid G, Inv G where
  mul_left_inv (a : G) : a⁻¹ * a = e

    

Some Theorems

Monoid

      /- ### monoid -/
-- 逆元が存在すれば一意
theorem left_inv_eq_right_inv {M : Type u} [Monoid M] {a b c : M}
    (hba : b * a = e) (hac : a * c = e) : b = c := by
  rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]
    

Group

      /- ### group -/
variable {G : Type u} [Group G] {a b c : G}
@[simp] lemma mul_left_inv : ∀ a : G, a⁻¹ * a = e :=
  Group.mul_left_inv
-- 逆元の一意性
@[simp] theorem inv_eq_of_mul_eq_one (h : a * b = e) : a⁻¹ = b :=
  left_inv_eq_right_inv (mul_left_inv a) h
-- 逆元の逆元
@[simp] theorem inv_inv (a : G) : (a⁻¹)⁻¹ = a :=
  inv_eq_of_mul_eq_one (mul_left_inv a)
-- 公理の削減
@[simp] theorem mul_right_inv (a : G) : a * a⁻¹ = e := by
  rw [←mul_left_inv (a⁻¹), inv_inv]
    

Another Definition

      class Group' (G : Type u) extends Monoid G, Inv G where
  mul_left_inv (a : G) : a⁻¹ * a = e
  mul_right_inv (a : G) : a * a⁻¹  = e
variable {G : Type u} [Group G]
instance : Group' G where
  mul_left_inv  := Group.mul_left_inv
  mul_right_inv := mul_right_inv
    

Appendix

Magma

      /- ### Magma -/
class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ
infixl:70 " * "  => HMul.hMul
class Mul (α : Type u) where
  mul : α → α → α
instance [Mul α] : HMul α α α where
  hMul a b := Mul.mul a b
    

参考： Prelude.lean

Macro

コードの冒頭に下記のマクロを記述することで、theoremの他、lemmaが使えるようになります。

lemmaの挙動はtheoremと全く同じですが、theoremと組み合わせて使い分けることで、主張の重要度の目安等になると思います。

      macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command =>
  `($mods:declModifiers theorem $n $sig $val)
    

References

• lean (latest version := v4.0.0-m2 )
• leanprover/lean4
• leanprover-community/mathlib4

Complete Code

      macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command =>
  `($mods:declModifiers theorem $n $sig $val)
/- ### ---------------------------------------------------------------------- ### -/
/- ### prerequires -/
class One (α : Type u) where
  one : α
notation "e" => One.one
-- instance [One α] : OfNat α (nat_lit 1) where
--   ofNat := One.one
class Inv (α : Type u) where
  inv : α → α
postfix:max "⁻¹" => Inv.inv

/- ### ---------------------------------------------------------------------- ### -/
/- ### Semigroups -/
class Semigroup (G : Type u) extends Mul G where
  mul_assoc (a b c : G) : (a * b) * c = a * (b * c)
lemma mul_assoc {G : Type u} [Semigroup G] :
    ∀ a b c : G, (a * b) * c = a * (b * c) :=
  Semigroup.mul_assoc
/- ### Monoids -/
class Monoid (M : Type u) extends Semigroup M, One M where
  mul_one (m : M) : m * e = m
  one_mul (m : M) : e * m = m
@[simp] lemma mul_one {M : Type u} [Monoid M] : ∀ (m : M), m * e = m :=
  Monoid.mul_one
@[simp] lemma one_mul {M : Type u} [Monoid M] : ∀ (m : M), e * m = m :=
  Monoid.one_mul
/- ### Groups -/
class Group (G : Type u) extends Monoid G, Inv G where
  mul_left_inv (a : G) : a⁻¹ * a = e

section lemmas
  -- ### monoid
  -- 逆元が存在すれば一意
  theorem left_inv_eq_right_inv {M : Type u} [Monoid M] {a b c : M}
      (hba : b * a = e) (hac : a * c = e) : b = c := by
    rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]
  -- ### group
  variable {G : Type u} [Group G] {a b c : G}
  @[simp] lemma mul_left_inv : ∀ a : G, a⁻¹ * a = e :=
    Group.mul_left_inv
  -- 逆元の一意性
  @[simp] theorem inv_eq_of_mul_eq_one (h : a * b = e) : a⁻¹ = b :=
    left_inv_eq_right_inv (mul_left_inv a) h
  -- 逆元の逆元
  @[simp] theorem inv_inv (a : G) : (a⁻¹)⁻¹ = a :=
    inv_eq_of_mul_eq_one (mul_left_inv a)
  -- 群の公理の削減
  @[simp] theorem mul_right_inv (a : G) : a * a⁻¹ = e := by
    rw [←mul_left_inv (a⁻¹), inv_inv]
end lemmas

/- ### ---------------------------------------------------------------------- ### -/
class Group' (G : Type u) extends Monoid G, Inv G where
  mul_left_inv (a : G) : a⁻¹ * a = e
  mul_right_inv (a : G) : a * a⁻¹  = e
section Group_axioms
  variable {G : Type u} [Group G]
  instance : Group' G where
    mul_left_inv  := Group.mul_left_inv
    mul_right_inv := mul_right_inv
end Group_axioms