$\alpha$が$\rm{Type}\ \mathit{u}$の型を持つ時、$\rm{Mul}\ \alpha$で$\alpha$は積を持つということは既知とします。ここで$u$はuniverseです。
この時$\alpha$は(推移律すら満たすと限らない)積を持つマグマとなります。
半群とは、推移律を満たす積を持つマグマのことです。
/- ### 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
モノイド(亜群)とは、単位元を持つ半群のことです。
/- ### 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
群とは、逆元対応を持つモノイドのことです。
新しく追加される情報は逆元対応と、それが逆元である性質です。
モノイド$G$に対し、逆元対応を$\iota:G\to G$とする時、逆元対応逆元の性質は
/- ### 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
/- ### 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]
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
/- ### 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
コードの冒頭に下記のマクロを記述することで、theoremの他、lemmaが使えるようになります。
lemmaの挙動はtheoremと全く同じですが、theoremと組み合わせて使い分けることで、主張の重要度の目安等になると思います。
macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command =>
`($mods:declModifiers theorem $n $sig $val)
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