Moving to Mathlib

Everything here was reinvented on purpose instead of imported, so that every moving part would be visible. Mathlib, Lean’s community mathematics library, already has much more general and well-tested versions of all of this:

Mathlib.Algebra.Group.Defs — Group, CommGroup, built with Lean’s type class mechanism (class ... extends ...) instead of a plain structure. This lets notation like a * b, a⁻¹, 1 work the same way across every group, without threading a Grp : argument through every definition by hand, and lets Lean find instances automatically through typeclass search.
Mathlib.Algebra.Ring.Defs — Ring, CommRing, Field, and the whole hierarchy in between (Semiring, NonUnitalRing, …).
Mathlib.Algebra.Module.Defs — Module, much more general than Chapter 10’s hand-built version, with the entire linear-algebra library (Mathlib.LinearAlgebra.*: bases, dimension, tensor products, exact sequences) built on top.
Mathlib.Combinatorics.Quiver.Basic and Mathlib.Algebra.Category.* — quivers as the underlying data of a category (a category is “a quiver plus identities and composition satisfying associativity,” the same free-category construction from Chapter 11), and Mathlib.CategoryTheory more broadly.
Path algebras specifically show up in representation-theory-oriented corners of Mathlib and in dedicated Lean projects on quiver representations. Searching Mathlib’s docs for “quiver” and “path” is a good starting point once the type-class style is familiar.

The jump from this book’s structure-based definitions to Mathlib’s class-based ones is mostly about ergonomics: automatic instance resolution, shared notation, and inheritance diamonds (the ambiguity that arises when a structure extends two parents with a common ancestor) already resolved. It is not really about mathematical content — the axioms already learned are the same axioms, merely packaged so Lean’s elaborator can find them without a Grp argument named in every theorem.

Two theorems for free

Everything above is a promise that Mathlib is more general. Here are two concrete payoffs — things this book explicitly could not state, using exactly the examples already built.

ZMod 3 is a field, not just a ring. Chapter 8, Section 5 built fin3Ring and said in so many words that a Field would need every nonzero element to be invertible, “true for $\mathbb{Z}/3$ precisely because $3$ is prime, but not part of Ring’s axioms and not checked here.” Mathlib already has this instance, for real:

example : Field (ZMod 3) := inferInstance

-- A fact `fin3Ring` (a mere `Ring`) genuinely cannot state: every
-- nonzero element has a multiplicative inverse.
example : ∀ a : ZMod 3, a ≠ 0 → ∃ b, a * b = 1 := by decide

Lagrange’s theorem, applied to the non-abelian example from Chapters 6-7. Equiv.Perm (Fin 3) (Chapter 6, Section 4’s Mathlib analogue of perm3Group) never had subgroups defined for it — the book built one group, not the lattice of its subgroups. Mathlib’s Subgroup type already comes with Lagrange’s theorem attached, so applying it to a real subgroup costs nothing beyond naming the subgroup:

-- Lagrange's theorem, fully generic: a subgroup's size divides the
-- ambient group's size.
example (s : Subgroup (Equiv.Perm (Fin 3))) :
    Nat.card s ∣ Nat.card (Equiv.Perm (Fin 3)) :=
  Subgroup.card_subgroup_dvd_card s

-- Concretely: |S_3| = 3! = 6...
example : Nat.card (Equiv.Perm (Fin 3)) = 6 := by
  rw [Nat.card_eq_fintype_card, Fintype.card_perm, Fintype.card_fin]
  rfl

-- ...and the cyclic subgroup generated by the 3-cycle finRotate 3 has
-- order 3, since (finRotate 3)^3 = 1 and finRotate 3 ≠ 1 with 3 prime.
example : Nat.card (Subgroup.zpowers (finRotate 3)) = 3 := by
  rw [Nat.card_zpowers]
  apply orderOf_eq_prime
  · decide
  · decide

Thus $3 \mid 6$ — not asserted, but derived, by instantiating a theorem Mathlib already proved once, generically, for every group. Neither of these two facts required a single new definition: both reuse objects this book already built, and both are facts this book’s own from-scratch Ring/Group genuinely could not have stated, since it never built the surrounding machinery (invertibility, subgroups) that Mathlib already has. This is the concrete shape of “moving to Mathlib”: not different mathematics, merely a much larger stock of already-proved consequences to draw on.

← What we built

Index

Next: Suggested next projects →