# 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)$. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:semigroup}} ``` 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. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:monoid}} ``` 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. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:group_def}} ``` 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. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:group_theorems}} ``` 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$. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:int2_def}} ``` 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: ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:int2_group}} ``` Each proof obligation is discharged by case analysis. With only two elements, Lean can verify each law by exhaustively checking all combinations. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:int2_theorems}} ``` 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. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:comm_group}} ``` ## Vector Spaces and Modules Groups appear everywhere, including in linear algebra. A **vector space** is an Abelian group (vectors under addition) equipped with **scalar multiplication** by elements of a field, satisfying certain compatibility laws. When the scalars come from a ring that is not a field, the same axioms define a **module**. Let us build a simple 2D example with integer scalars. Since $\mathbb{Z}$ is not a field, this is strictly speaking a $\mathbb{Z}$-module, but every law below is exactly the vector space law. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:vector_space_def}} ``` The vectors form a group under addition. Each vector $(x, y)$ has inverse $(-x, -y)$, and the zero vector is the identity. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:vector_space_group}} ``` Scalar multiplication satisfies the expected laws. These are the axioms that make scalar multiplication "compatible" with the vector space structure. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:vector_space_theorems}} ``` Concrete computations confirm the definitions work: ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:vector_examples}} ``` ## 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. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:ring_def}} ``` The integers satisfy all ring axioms: ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:integers_ring}} ``` 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](https://github.com/sdiehl/zero-to-qed/blob/main/src/ZeroToQED/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. **CommGroup** adds commutativity to Group. A **Ring** instead combines an abelian group for addition with a monoid for multiplication, linked by distributivity. Inheritance makes theorems available through the declared parent instances: our `Monoid` extends `Semigroup`, and our `Group` extends `Monoid`. The custom `Ring` above is a separate class with addition and multiplication fields; it does not extend these classes or automatically provide a `Semigroup` instance. Its additive group and multiplicative monoid structure must be connected by explicit instances if we want to reuse this custom hierarchy.
Algebraic Structure Hierarchy
A simplified mathematical hierarchy: arrows indicate underlying structures, not the parent declarations of our custom classes.
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 custom `Group` and `Ring` illustrate the same mathematical concepts as Mathlib’s classes, but they are separate declarations with different interfaces and inheritance. Building from first principles explains the laws behind Mathlib’s machinery, but our custom `Ring` does not include `mul_comm`. Mathlib’s `ring` tactic normalizes expressions in commutative semirings or rings, which supply multiplication commutativity in addition to the laws illustrated here. The custom classes are teaching examples, not replacements for Mathlib’s hierarchy. ## 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. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:involutive_abelian}} ``` 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. ```lean {{#include ../../src/ZeroToQED/AlgebraicStructures.lean:exercise_square_commutes}} ``` 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 here forms the foundation for the full algebraic hierarchy, including [Galois theory in Mathlib](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Galois/Basic.html).