Algebraic Structures

Mathematics organizes operations into hierarchies. A group is more than a set with an operation: it is a semigroup with identity and inverses, and a semigroup is a set with an associative operation. These hierarchies matter because theorems proved at one level apply to all structures below it. Prove something about groups, and it holds for integers, permutations, and matrix transformations alike.

Lean captures these hierarchies through type classes. Each algebraic structure becomes a type class, and instances register specific types as members. The type class system then automatically provides the right theorems and operations wherever they apply. The notation is convenient, but the real value is the machinery underneath: generic mathematical code that works across any conforming type.

Semigroups

A semigroup is the simplest algebraic structure: a type with a binary operation that is associative. Nothing more. No identity element, no inverses, just the guarantee that \((a \cdot b) \cdot c = a \cdot (b \cdot c)\).

-- A semigroup has an associative binary operation
class Semigroup (α : Type) where
  op : α → α → α
  op_assoc : ∀ a b c : α, op (op a b) c = op a (op b c)

-- Notation for our operation
infixl:70 " ⋆ " => Semigroup.op

The op_assoc field is a proof that clients can use directly. Any theorem about semigroups can invoke this associativity without asking whether a particular type satisfies it. The type class instance guarantees it.

Monoids

A monoid extends a semigroup with an identity element. The identity must satisfy two laws: left identity (\(e \cdot a = a\)) and right identity (\(a \cdot e = a\)). Natural numbers under addition form a monoid with identity 0. Natural numbers under multiplication form a different monoid with identity 1. Same type, different structures.

-- A monoid adds an identity element to a semigroup
class Monoid (α : Type) extends Semigroup α where
  e : α
  e_op : ∀ a : α, op e a = a
  op_e : ∀ a : α, op a e = a

The extends Semigroup α clause means every monoid is automatically a semigroup. Lean’s type class inheritance handles this: any function expecting a semigroup accepts a monoid. The hierarchy is operational, not merely conceptual.

Groups

A group adds inverses to a monoid. Every element \(a\) has an inverse \(a^{-1}\) such that \(a^{-1} \cdot a = e\) and \(a \cdot a^{-1} = e\). Integers under addition form a group. Positive rationals under multiplication form a group. Permutations under composition form a group. The examples proliferate across mathematics.

-- A group adds inverses to a monoid
class Group (α : Type) extends Monoid α where
  inv : α → α
  inv_op : ∀ a : α, op (inv a) a = e
  op_inv : ∀ a : α, op a (inv a) = e

-- Notation for inverse
postfix:max "⁻¹" => Group.inv

With this definition, we can prove fundamental group theorems that apply to any group. These are not approximations or heuristics; they are mathematical facts verified by the type checker.

Group Theorems

From just the group axioms, many properties follow. Cancellation laws let us simplify equations. The identity is unique, as are inverses. The inverse of a product reverses the order. These theorems are mechanical consequences of the axioms, and Lean verifies each step.

-- Now we prove fundamental group theorems from the axioms

variable {G : Type} [Group G]

-- Left cancellation: if a ⋆ b = a ⋆ c then b = c
theorem op_left_cancel (a b c : G) (h : a ⋆ b = a ⋆ c) : b = c := by
  have : a⁻¹ ⋆ (a ⋆ b) = a⁻¹ ⋆ (a ⋆ c) := by rw [h]
  simp only [← Semigroup.op_assoc, Group.inv_op, Monoid.e_op] at this
  exact this

-- Right cancellation: if b ⋆ a = c ⋆ a then b = c
theorem op_right_cancel (a b c : G) (h : b ⋆ a = c ⋆ a) : b = c := by
  have : (b ⋆ a) ⋆ a⁻¹ = (c ⋆ a) ⋆ a⁻¹ := by rw [h]
  simp only [Semigroup.op_assoc, Group.op_inv, Monoid.op_e] at this
  exact this

-- The identity is unique
theorem e_unique (e' : G) (h : ∀ a : G, e' ⋆ a = a) : e' = Monoid.e := by
  have : e' ⋆ Monoid.e = Monoid.e := h Monoid.e
  rw [Monoid.op_e] at this
  exact this

-- Inverses are unique
theorem inv_unique (a b : G) (h : b ⋆ a = Monoid.e) : b = a⁻¹ := by
  have step1 : b ⋆ a ⋆ a⁻¹ = Monoid.e ⋆ a⁻¹ := by rw [h]
  simp only [Semigroup.op_assoc, Group.op_inv, Monoid.op_e, Monoid.e_op] at step1
  exact step1

-- Double inverse: (a⁻¹)⁻¹ = a
theorem inv_inv (a : G) : (a⁻¹)⁻¹ = a := by
  symm
  apply inv_unique
  exact Group.op_inv a

-- Inverse of product: (a ⋆ b)⁻¹ = b⁻¹ ⋆ a⁻¹
theorem op_inv_rev (a b : G) : (a ⋆ b)⁻¹ = b⁻¹ ⋆ a⁻¹ := by
  symm
  apply inv_unique
  calc b⁻¹ ⋆ a⁻¹ ⋆ (a ⋆ b)
      = b⁻¹ ⋆ (a⁻¹ ⋆ (a ⋆ b)) := by rw [Semigroup.op_assoc]
    _ = b⁻¹ ⋆ (a⁻¹ ⋆ a ⋆ b) := by rw [← Semigroup.op_assoc a⁻¹ a b]
    _ = b⁻¹ ⋆ (Monoid.e ⋆ b) := by rw [Group.inv_op]
    _ = b⁻¹ ⋆ b := by rw [Monoid.e_op]
    _ = Monoid.e := Group.inv_op b

The theorem op_inv_rev shows that \((a \cdot b)^{-1} = b^{-1} \cdot a^{-1}\). The order reverses because we need to undo the operations in reverse sequence. The proof uses our inv_unique theorem: to show two things are equal to an inverse, show they act as that inverse.

Integers Mod 2

Theory without examples is suspect. Let us build a concrete group: integers modulo 2. This group has exactly two elements (zero and one) with addition wrapping around: \(1 + 1 = 0\).

-- Example: Integers mod 2 form a group under addition

inductive Z2 : Type where
  | zero : Z2
  | one : Z2
  deriving DecidableEq, Repr

def Z2.add : Z2 → Z2 → Z2
  | .zero, a => a
  | .one, .zero => .one
  | .one, .one => .zero

def Z2.neg : Z2 → Z2
  | a => a  -- In Z2, every element is its own inverse

Every element is its own inverse (\(0 + 0 = 0\) and \(1 + 1 = 0\)), which simplifies the structure. Now we register this as a group instance:

instance : Group Z2 where
  op := Z2.add
  op_assoc := by
    intro a b c
    cases a <;> cases b <;> cases c <;> rfl
  e := Z2.zero
  e_op := by
    intro a
    cases a <;> rfl
  op_e := by
    intro a
    cases a <;> rfl
  inv := Z2.neg
  inv_op := by
    intro a
    cases a <;> rfl
  op_inv := by
    intro a
    cases a <;> rfl

-- Test computation
#eval (Z2.one ⋆ Z2.one : Z2)  -- zero
#eval (Z2.one ⋆ Z2.zero : Z2) -- one

Each proof obligation is discharged by case analysis. With only two elements, Lean can verify each law by exhaustively checking all combinations.

-- Verify our theorems work on the concrete example
example : (Z2.one)⁻¹ = Z2.one := rfl
example : Z2.one ⋆ Z2.one⁻¹ = Z2.zero := rfl

theorem z2_self_inverse (a : Z2) : a ⋆ a = Monoid.e := by
  cases a <;> rfl

-- Z2 is commutative
theorem z2_comm (a b : Z2) : a ⋆ b = b ⋆ a := by
  cases a <;> cases b <;> rfl

Because Z2 is now a Group, all our general theorems apply. The op_left_cancel and inv_unique theorems work on Z2 without modification. Generic mathematics, specific verification.

Commutative Groups

Some groups satisfy an additional property: commutativity. In a commutative (or Abelian) group, \(a \cdot b = b \cdot a\) for all elements. Integer addition is commutative; matrix multiplication is not.

-- Commutative (Abelian) groups
class CommGroup (α : Type) extends Group α where
  op_comm : ∀ a b : α, Semigroup.op a b = Semigroup.op b a

instance : CommGroup Z2 where
  op_comm := z2_comm

Vector Spaces

Groups appear everywhere, including in linear algebra. A vector space is an Abelian group (vectors under addition) equipped with scalar multiplication satisfying certain compatibility laws. Let us build a simple 2D vector space over the integers.

-- A simple 2D vector space over integers

structure Vec2 where
  x : Int
  y : Int
  deriving DecidableEq, Repr

def Vec2.add (v w : Vec2) : Vec2 :=
  ⟨v.x + w.x, v.y + w.y⟩

def Vec2.neg (v : Vec2) : Vec2 :=
  ⟨-v.x, -v.y⟩

def Vec2.zero : Vec2 := ⟨0, 0⟩

def Vec2.smul (c : Int) (v : Vec2) : Vec2 :=
  ⟨c * v.x, c * v.y⟩

infixl:65 " +ᵥ " => Vec2.add
prefix:100 "-ᵥ" => Vec2.neg
infixl:70 " •ᵥ " => Vec2.smul

The vectors form a group under addition. Each vector \((x, y)\) has inverse \((-x, -y)\), and the zero vector is the identity.

-- Vec2 forms a group under addition
theorem vec2_inv_op (a : Vec2) : Vec2.add (Vec2.neg a) a = Vec2.zero := by
  simp only [Vec2.add, Vec2.neg, Vec2.zero, Int.add_comm, Int.add_right_neg]

theorem vec2_op_inv (a : Vec2) : Vec2.add a (Vec2.neg a) = Vec2.zero := by
  simp only [Vec2.add, Vec2.neg, Vec2.zero, Int.add_right_neg]

instance : Group Vec2 where
  op := Vec2.add
  op_assoc := by
    intro a b c
    simp only [Vec2.add, Int.add_assoc]
  e := Vec2.zero
  e_op := by
    intro a
    simp only [Vec2.add, Vec2.zero, Int.zero_add]
  op_e := by
    intro a
    simp only [Vec2.add, Vec2.zero, Int.add_zero]
  inv := Vec2.neg
  inv_op := vec2_inv_op
  op_inv := vec2_op_inv

-- Vec2 is commutative
theorem vec2_comm (a b : Vec2) : a ⋆ b = b ⋆ a := by
  show Vec2.add a b = Vec2.add b a
  simp only [Vec2.add, Int.add_comm]

instance : CommGroup Vec2 where
  op_comm := vec2_comm

Scalar multiplication satisfies the expected laws. These are the axioms that make scalar multiplication “compatible” with the vector space structure.

-- Scalar multiplication properties
theorem smul_zero (c : Int) : c •ᵥ Vec2.zero = Vec2.zero := by
  simp only [Vec2.smul, Vec2.zero, Int.mul_zero]

theorem zero_smul (v : Vec2) : (0 : Int) •ᵥ v = Vec2.zero := by
  simp only [Vec2.smul, Vec2.zero, Int.zero_mul]

theorem one_smul (v : Vec2) : (1 : Int) •ᵥ v = v := by
  simp only [Vec2.smul, Int.one_mul]

theorem smul_add (c : Int) (v w : Vec2) :
    c •ᵥ (v +ᵥ w) = (c •ᵥ v) +ᵥ (c •ᵥ w) := by
  simp only [Vec2.smul, Vec2.add, Int.mul_add]

theorem add_smul (c d : Int) (v : Vec2) :
    (c + d) •ᵥ v = (c •ᵥ v) +ᵥ (d •ᵥ v) := by
  simp only [Vec2.smul, Vec2.add, Int.add_mul]

theorem smul_smul (c d : Int) (v : Vec2) :
    c •ᵥ (d •ᵥ v) = (c * d) •ᵥ v := by
  simp only [Vec2.smul, Int.mul_assoc]

Concrete computations confirm the definitions work:

-- Concrete computations
def v1 : Vec2 := ⟨1, 2⟩
def v2 : Vec2 := ⟨3, 4⟩

#eval v1 +ᵥ v2           -- { x := 4, y := 6 }
#eval 2 •ᵥ v1            -- { x := 2, y := 4 }
#eval v1 +ᵥ (-ᵥv1)       -- { x := 0, y := 0 }

-- The group inverse works correctly
example : v1 +ᵥ (-ᵥv1) = Vec2.zero := by rfl

Rings

A ring has two operations: addition forming an Abelian group, and multiplication forming a monoid. Distributivity connects them: \(a \cdot (b + c) = a \cdot b + a \cdot c\). Integers, polynomials, and matrices all form rings.

-- A ring combines two structures: an abelian group under addition
-- and a monoid under multiplication, linked by distributivity

class Ring (α : Type) where
  -- Additive abelian group
  add : α → α → α
  zero : α
  neg : α → α
  add_assoc : ∀ a b c, add (add a b) c = add a (add b c)
  zero_add : ∀ a, add zero a = a
  add_zero : ∀ a, add a zero = a
  neg_add : ∀ a, add (neg a) a = zero
  add_comm : ∀ a b, add a b = add b a
  -- Multiplicative monoid
  mul : α → α → α
  one : α
  mul_assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)
  one_mul : ∀ a, mul one a = a
  mul_one : ∀ a, mul a one = a
  -- Distributivity connects the two structures
  left_distrib : ∀ a b c, mul a (add b c) = add (mul a b) (mul a c)
  right_distrib : ∀ a b c, mul (add a b) c = add (mul a c) (mul b c)

The integers satisfy all ring axioms:

-- The integers form a ring
instance intRing : Ring Int where
  add := (· + ·)
  zero := 0
  neg := (- ·)
  mul := (· * ·)
  one := 1
  add_assoc := Int.add_assoc
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  neg_add := Int.add_left_neg
  add_comm := Int.add_comm
  mul_assoc := Int.mul_assoc
  one_mul := Int.one_mul
  mul_one := Int.mul_one
  left_distrib := Int.mul_add
  right_distrib := Int.add_mul

From these axioms, one can prove that \(0 \cdot a = 0\) for any ring element \(a\). This follows from distributivity: \(0 \cdot a + 0 \cdot a = (0 + 0) \cdot a = 0 \cdot a\), and cancellation gives \(0 \cdot a = 0\). See ring_zero_mul and ring_mul_zero in AlgebraicStructures.lean for the full proofs.

The Hierarchy

The structures we have defined form a hierarchy. At the base sits Semigroup, requiring only an associative operation. Monoid extends Semigroup by adding an identity element. Group extends Monoid by adding inverses. From Group, two paths diverge: CommGroup adds commutativity, while Ring combines an abelian group (for addition) with a monoid (for multiplication) linked by distributivity.

Each extension relationship means theorems flow downward. Prove something about semigroups, and it applies to monoids, groups, and rings. Lean’s type class inheritance makes this operational: any function expecting a Semigroup instance automatically accepts a Monoid, Group, or Ring.

Mathlib takes this much further. The full algebraic hierarchy includes semirings, division rings, fields, modules, algebras, and dozens of ordered variants. Each structure captures a precise set of assumptions, and theorems are proved at exactly the level of generality where they hold.

First Principles to Mathlib

We built these structures from scratch to understand how they work. In practice, you would use Mathlib’s definitions, which are battle-tested and integrated with thousands of theorems. Our Group is Mathlib’s Group. Our MyRing is Mathlib’s Ring. The concepts are identical; the implementations are industrial-strength.

The value of building from first principles is understanding. When Mathlib’s ring tactic solves a polynomial identity, it is applying theorems like our ring_zero_mul millions of times per second. When type class inference finds a CommGroup instance, it is navigating a hierarchy like the one we drew. The abstraction is real, and so is the machinery underneath.

Constraints Beget Structure

One of the beautiful facts in group theory is that strong constraints force unexpected structure. Consider a group where every element is its own inverse: \(g^2 = e\) for all \(g\). Such groups must be abelian. The proof is a gem of algebraic reasoning.

-- If every element is its own inverse, the group must be abelian.
-- The proof: ab = (ab)⁻¹ = b⁻¹a⁻¹ = ba. Constraints beget structure.
theorem involutive_imp_comm {G : Type} [Group G]
    (h : ∀ g : G, g ⋆ g = Monoid.e) : ∀ a b : G, a ⋆ b = b ⋆ a := by
  intro a b
  -- Key insight: if g² = e then g = g⁻¹
  have inv_self : ∀ g : G, g = g⁻¹ := fun g => by
    have := h g
    calc g = g ⋆ Monoid.e := (Monoid.op_e _).symm
      _ = g ⋆ (g ⋆ g⁻¹) := by rw [Group.op_inv]
      _ = (g ⋆ g) ⋆ g⁻¹ := (Semigroup.op_assoc _ _ _).symm
      _ = Monoid.e ⋆ g⁻¹ := by rw [this]
      _ = g⁻¹ := Monoid.e_op _
  -- Now: ab = (ab)⁻¹ = b⁻¹a⁻¹ = ba
  calc a ⋆ b
      = (a ⋆ b)⁻¹ := inv_self (a ⋆ b)
    _ = b⁻¹ ⋆ a⁻¹ := op_inv_rev a b
    _ = b ⋆ a := by rw [← inv_self a, ← inv_self b]

The key insight is that \(g^2 = e\) implies \(g = g^{-1}\). From there, \(ab = (ab)^{-1} = b^{-1}a^{-1} = ba\). The constraint on squares forces commutativity. Our Z2 group is an example: every element squares to zero, and the group is indeed abelian.

Squaring Distributes

A related result: if squaring distributes over the group operation, meaning \((ab)^2 = a^2 b^2\) for all elements, then the group must be abelian. This is left as an exercise.

-- Exercise: If squaring distributes, the group is abelian.
-- Hint: expand (ab)² = a²b² and cancel to get ab = ba.
theorem square_distrib_imp_comm {G : Type} [Group G]
    (h : ∀ a b : G, (a ⋆ b) ⋆ (a ⋆ b) = (a ⋆ a) ⋆ (b ⋆ b)) :
    ∀ a b : G, a ⋆ b = b ⋆ a := by
  sorry

The hint is to expand both sides. On the left, \((ab)^2 = abab\). On the right, \(a^2 b^2 = aabb\). The equality \(abab = aabb\) lets you cancel \(a\) on the left and \(b\) on the right, yielding \(ba = ab\). The machinery we built in this chapter forms the foundation for the full algebraic hierarchy, including Galois theory in Mathlib.