Basics

General Group

There is only one operator and one object (or set) in group, where the operator is abstracted as $\diamond$ and identity as $\mathbf{1}$. But they are not specified concretely, the operator $\diamond$ can be $+$ or $\ast$, and the identity $\text{bold}1$ can be $0$ or $1$ for addition and multiplication respectively. So group with $(+,0)$ is called AddGroup, and group with $(\ast ,1)$ is called MulGroup. In lean4, the default Group is MulGroup.

One Class

class One₁ (α : Type) where
  /-- The element one -/
  one : α

@[inherit_doc]
notation "𝟙" => One₁.one

example {α : Type} [One₁ α] : α := 𝟙

example {α : Type} [One₁ α] : (𝟙 : α) = 𝟙 := rfl

One class, denoted as "𝟙", is used to show the existence of identity, $\text{bold}1$ for multplicative, and $\text{bold}0$ for additive, note that $one\ne 1$.

Dia Class

class Dia₁ (α : Type) where
  dia : α → α → α

infixl:70 " ⋄ "   => Dia₁.dia

Dia class, denoted as diamond operator $\diamond$, defines the function of binary operation of type $\alpha \to \alpha \to \alpha$.

Semigroup Class

class Semigroup₁ (α : Type) extends toDia₁ : Dia₁ α where
  /-- Diamond is associative -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

Semigroup class is used to define the associative property on operator $\diamond$, so we need to extend Dia class first.

DiaOneClass Class

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

DiaOneClass class is specially used to define binary operation properties of $\diamond$ specially with identity element $\text{bold}1$, so we also need to extend Dia class and One class first.

Monoid Class

class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α

Monoid class is a combination of Semigroup and DiaOneClass, which has axioms:

• operation closure on operator $\diamond$ with type $\alpha \to \alpha \to \alpha$.
• identity and its binary operations, $1\diamond a=a\diamond 1$.
• associative, $a\cdot b\cdot c=a\diamond (b\diamond c)$.

Inv Class

class Inv₁ (α : Type) where
  /-- The inversion function -/
  inv : α → α

@[inherit_doc]
postfix:max "⁻¹" => Inv₁.inv

Inv class, denoted as ${}^{-1}$,defines the inverse function $\alpha \to \alpha$.

Group

class Group₁ (G : Type) extends Monoid₁ G, Inv₁ G where
  inv_dia : ∀ a : G, a⁻¹ ⋄ a =

Group class defines the inverse property $a^{-1}\cdot a=1$, it is a function of $\alpha \to \alpha \to \alpha$ on operator $\diamond$, and has inverse function $\alpha \to \alpha$ on ${}^{-1}$. So we need to extend Monoid and Inv class first.

Addition Group

Group with $(\diamond ,\text{bold}1)$ cannot be used directly, operator and identiy must be specified respectively, so Group with $(+,0)$ is called AddGroup.

AddSemigroup Class

class AddSemigroup₃ (α : Type) extends Add α where
  /-- Addition is associative -/
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

Add is a concrete operator class of type $\alpha \to \alpha \to \alpha$, denoted as $+$. It is corresponded with Dia class in general Group structure. In this case, AddSemigroup is corresponded with Semigroup in general Group structure, in which the operator $\diamond$ of association is replaced with $+$.

Semigroup Class

@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
  /-- Multiplication is associative -/
  mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)

In lean4, multipliation $\ast$ is the default operator, so Semingroup is $\ast$ versioned of AddSemigroup.

AddMonoid Class

class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α

Similar with Monoid in general Group class structure, AddMonoid must extend AddSemigroup and AddZeroClass, where AddZeroClass corresponds with DiaOneClass specially for operator $+$ and identity $0$.

AddCommSemigroup Class

class AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ α where
  add_comm : ∀ a b : α, a + b = b + a

AddCommSemigroup define the commutative property of AddSemigroup.

AddCommMonoid Class

class AddCommMonoid₃ (α : Type) extends AddMonoid₃ α, AddCommSemigroup₃ α

AddCommMonoid is a combination of AddMonoid and AddCommSemigroup.

AddGroup Class

class AddGroup₃ (G : Type) extends AddMonoid₃ G, Neg G where
  neg_add : ∀ a : G, -a + a = 0

Similar with general Group class, Neg class is corresponded with Inv specially for operator $+$, and $a^{-1}\diamond a=\text{bold}1$ in inv_dia is replaced with $-a+a=0$ in neg_add.

Multiplicative Group

@[to_additive AddGroup₃]
class Group₃ (G : Type) extends Monoid₃ G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1

In lean4, the default operator in group is $\ast$, so actually (multiplicative) Group is implemented, and then use @[to_...] to automatically generate code for AddGroup.

Additive Commutative Group

Additive commutative group is an additive group with commutative property.

class AddCommGroup₃ (G : Type) extends AddGroup₃ G, AddCommMonoid₃ G

In this case, we need to inherit additive group property from AddGroup and commutative property from AddCommMonoid. Usually we have a beautiful name for AddCommGroup, that is Abelian Group. But in lean4 $\ast$ is the default one, so we might see that Abelian Group is used to refer multiplicative Group.

Ring

Ring is composed of two components, one is object, the other one is scalar, but both of them are defined by the same set $R$ :

• the object is an AddCommGroup (abelian group) with operator $+$. But below we extend AddGroup instead of AddCommGroup as commutative property can be derived from the distributive property, $(1+1)\ast (a+b)=(a+b)+(a+b)=(a+a)+(b+b)$. We can see that the add_comm is derived in Additive Commutative Group.
• the scalar is an (multiplicative) Monoid with operator $\ast$.
• operations on $\ast$ with $0$ will be absorbed into $0$.
• mixed operations on $+$ and $\ast$ satisfy distributive property.

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

In general, Ring does not have multiplicative commutative property.

Additive Commutative Group

Additive commutative group (also known as abelian group) is a additive group with commutative property.

class AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ α where
  add_comm : ∀ a b : α, a + b = b + a

@[to_additive AddCommSemigroup₃]
class CommSemigroup₃ (α : Type) extends Semigroup₃ α where
  mul_comm : ∀ a b : α, a * b = b * a

class AddCommMonoid₃ (α : Type) extends AddMonoid₃ α, AddCommSemigroup₃ α

@[to_additive AddCommMonoid₃]
class CommMonoid₃ (α : Type) extends Monoid₃ α, CommSemigroup₃ α

class AddCommGroup₃ (G : Type) extends AddGroup₃ G, AddCommMonoid₃ G

Note that, in general AddSemigroup does not have additive commutative property, so we need to add its definition manually in AddCommSemigroup. It is clear to see that AddSemigroup is also an abstract class, we need to instantiate it before using. We can see an instance of AddCommGroup with type $\alpha$ instantiated with Ring, and the commutative property will be instantiated by utilizing Ring's basic properties (additive association, distribution, etc...):

instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
{
  add_comm := by
    intro a b
    have : a + (a + b + b) = a + (b + a + b) := calc
      a + (a + b + b) = (a + a) + (b + b) := by simp [add_assoc₃, add_assoc₃]
      _ = (1 * a + 1 * a) + (1 * b + 1 * b) := by simp
      _ = (1 + 1) * a + (1 + 1) * b := by simp [Ring₃.right_distrib]
      _ = (1 + 1) * (a + b) := by simp [Ring₃.left_distrib]
      _ = 1 * (a + b) + 1 * (a + b) := by simp [Ring₃.right_distrib]
      _ = (a + b) + (a + b) := by simp
      _ = a + (b + a + b) := by simp [add_assoc₃]
    exact add_right_cancel₃ (add_left_cancel₃ this)
}

Module

Similar with Ring, Module also consists of two components, one is an object, the other one is a scalar. The difference is that they are defined on two different sets $M$ and $R$ respectively. And there are three operators amond them :

• the object $M$ is a AddCommGroup (or additive abelian group) with operator $+$
• the scalar $R$ is a Ring with two operators, $\ast$ and $+$
• operation between object and scalar is often abstracted as scalar-mul SMul symbol $\cdot$ with type $\alpha \to \beta \to \beta$ . That is, any element from Ring is absorbed in AddCommGroup. A few operations of scalar-mul SMul are listed below :
  • $(a\ast b)\cdot m=a\cdot b\cdot m$
  • $(a+b)\cdot m=a\cdot m+b\cdot m$
  • $a\cdot (m+n)=a\cdot m+a\cdot n$

class SMul₃ (α : Type) (β : Type) where
  /-- Scalar multiplication -/
  smul : α → β → β

infixr:73 " • " => SMul₃.smul

class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M where
  zero_smul : ∀ m : M, (0 : R) • m = 0
  one_smul : ∀ m : M, (1 : R) • m = m
  mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
  add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
  smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

Notice that Module class is also an abstract one, not instantiated yet, specially including a few operations of $\cdot$ :

1. SMul operator $\cdot$, need to implement smul function
2. $1\cdot m$ operation, need to implement one_mul function
3. $m\cdot 1$ operation, need to implement mul_one function
4. $(a\ast b)\cdot m$ operation, need to implement mul_smul function
5. $(a+b)\cdot m$ operation, need to implement add_smul function
6. $a\cdot (m+n)$ operation, need to implement smul_add function

Another typical example of Module is, Ring itself is a module over iteself, that is, $R$ is a module over $R$. In this case, we can instantiate Module class with :

• SMul operator $\cdot$ with multiplication $\ast$
• object $M$ of AddCommGroup in Module is instantiated with Ring, since Ring extends AddCommGroup.
• scalar $R$ of Semiring in Module is instantiated with Ring itself, even though Ring does not inherit Semiring directly, but it has all properties of Semiring.

So all relevent functions will be instantiated with:

1. smul $\alpha \to \alpha \to \alpha$ is instantiated with $\text{AddCommGroup Ring}\to \text{Ring}\to \text{Ring}$
2. one_mul $1\cdot m$ is instantiated with $1\ast m$
3. mul_one $m\cdot 1$ is instantiated with $m\ast 1$
4. mul_smul $(a\ast b)\cdot m$ is instantiated with $(a\ast b)\ast m$
5. add_mul $(a+b)\cdot m$ is instantiated with $(a+b)\ast m$
6. mul_add $a\cdot (m+n)$ is instantiated with $a\ast (m+n)$

instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
  smul := fun r s ↦ r*s
  zero_smul := zero_mul
  one_smul := one_mul
  mul_smul := mul_assoc₃
  add_smul := Ring₃.right_distrib
  smul_add := Ring₃.left_distrib

Notice that selfModule is not a fully instantiated instance of Module, since AddCommGroup Ring and Ring are still abstract classes. For example, Ring can be further instantiated with $\text{Z}$, $\mathbb{F}[X]$, etc ...

Export

Similar with some other programming languages, by export Class (func1, func2, ...),

export DiaOneClass₁ (one_dia dia_one)
export Semigroup₁ (dia_assoc)
export Group₁ (inv_dia)

we can directly us one_dia instead of DiaOneClass.one_dia, similarly for dia_one, dia_assoc, and inv_dia .

Mophism

Monoid Homomorphism

Homomorphism on Monoid which is operator-identity pair of $(\ast ,1)$,

@[ext]
structure MonoidHom₁ (G H : Type) [Monoid G] [Monoid H]  where
  toFun : G → H
  map_one : toFun 1 = 1
  map_mul : ∀ g g', toFun (g * g') = toFun g * toFun g'

is defined with :

• toFunc is one function of $\text{Monoid}\to \text{Monoid}$
• map_one shows identity map
• map_mul shows operation preservation of map

Below shows homomorphism on AddMonoid with operator-identity pair of $(+,0)$,

@[ext]
structure AddMonoidHom₁ (G H : Type) [AddMonoid G] [AddMonoid H]  where
  toFun : G → H
  map_zero : toFun 0 = 0
  map_add : ∀ g g', toFun (g + g') = toFun g + toFun g'

Ring Homomorphism

@[ext]
structure RingHom₁ (R S : Type) [Ring R] [Ring S] extends MonoidHom₁ R S, AddMonoidHom₁ R S

Ring has two operators $+$ and $\ast$, so RingHom can be easily obtained by extending MonoidHom and AddMonoidHom :

• $1\mapsto 1$ from MonoidHom
• $f(a\ast b)=f(a)\ast f(b)$ from MonoidHom
• $0\mapsto 0$ from AddMonoidHom
• $g(a+b)=g(a)+g(b)$ from AddMonoidHom

Homomorphism Class

class MonoidHomClass₁ (F : Type) (M N : Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

MonoidHomClass is a class (group) of MonoidHom with type $\text{Monoid}\to \text{Monoid}$.

Another kind of definition of MonoidHomClass and RingHomClass :

instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₂ (MonoidHom₁ M N) M N where
  toFun := MonoidHom₁.toFun
  map_one := fun f ↦ f.map_one
  map_mul := fun f ↦ f.map_mul

instance (R S : Type) [Ring R] [Ring S] : MonoidHomClass₂ (RingHom₁ R S) R S where
  toFun := fun f ↦ f.toMonoidHom₁.toFun
  map_one := fun f ↦ f.toMonoidHom₁.map_one
  map_mul := fun f ↦ f.toMonoidHom₁.map_mul

Since already RingHom extends MonoidHom, we can directly use toMonoidHom to get the functionality of monoid homomorphism.

Order Preserve Homomorphism

Let's see an example of order preserve homomorphism on monoid,

@[ext]
structure OrderPresHom (α β : Type) [LE α] [LE β] where
  toFun : α → β
  le_of_le : ∀ a a', a ≤ a' → toFun a ≤ toFun a'

@[ext]
structure OrderPresMonoidHom (M N : Type) [Monoid M] [LE M] [Monoid N] [LE N] extends
MonoidHom₁ M N, OrderPresHom M N

OrderPresMonoidHom preserves order operation $\le$ on Monoid.

class OrderPresHomClass (F : Type) (α β : outParam Type) [LE α] [LE β]

instance (α β : Type) [LE α] [LE β] : OrderPresHomClass (OrderPresHom α β) α β where

instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
    OrderPresHomClass (OrderPresMonoidHom α β) α β where

instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
    MonoidHomClass₃ (OrderPresMonoidHom α β) α β
  where
    coe := fun f ↦ f.toOrderPresHom.toFun
    coe_injective' _ _ := OrderPresMonoidHom.ext
    map_one := fun f ↦ f.toMonoidHom₁.map_one
    map_mul := fun f ↦ f.toMonoidHom₁.map_mul

OrderPresHomClass is the class (group) of order preserve homomorphism, and MonoidHomClass is the class (group) of order preseve homomorphism on Monoid.