A Lean Companion to Conceptual Mathematics

This Companion, which shamelessly steals its title and a fair bit of its approach from Terence Tao's formalisation of his Analysis I textbook, is intended to be used alongside the second edition of Lawvere and Schanuel's Conceptual Mathematics. The Companion aims to formalise most of the definitions, theorems, and exercises in Conceptual Mathematics using Lean 4 and mathlib, but reproduces almost none of the text from the book itself and consequently has little value on its own.

When formalising the definitions in the book, I have tried to use the corresponding definitions in mathlib where I was able to find them, rather than reinventing too many wheels. For the exercises, I have generally stayed faithful to the wording in the book, but I have taken some small liberties where I felt doing so would allow a solution to reflect more clearly the core concerns of the question (for instance, by a frequent use of types instead of sets). I have flagged any such deviations in the comments.

I have attempted to strike a balance throughout between ease of reading and optimised, idiomatic Lean code, but wherever needed have erred (I hope!) on the side of readability. In particular, I have largely avoided the use of the simp tactic and other automation, in order to make the logical steps in the proofs as explicit as possible.

This Companion is the result of a project I undertook to learn both Lean and some elementary category theory at the same time (and ultimately a decent amount about Verso too). It remains a work in progress. It will contain plenty of opportunities for improvement and more than a few errors! I welcome any comments, suggestions, corrections, or contributions. Please feel free to open an issue or a pull request on the GitHub repository.

To learn more about Lean and mathlib, please visit the wonderful Lean community website.

Of particular relevance to this Companion is the high-level overview of category theory in mathlib hosted on the community site, which provides a helpful jumping-off point and also covers some of the key notation.

Regarding notation, it is worth mentioning that composition of morphisms in mathlib uses the notation ≫ (\gg), as in f ≫ g, which means "f followed by g". To align with the book and to follow the usual convention, however, we introduce the notation ⊚ (\oo), as in f ⊚ g, which means "f following g":

local notation:80 g " ⊚ " f:80 => CategoryStruct.comp f g

(This approach is suggested on the high-level overview page mentioned in the previous paragraph as well as elsewhere in the mathlib documentation.)

All page references given in this Companion are to Lawvere, F.W. and Schanuel, S.H. (2009) Conceptual mathematics: a first introduction to categories. 2nd edn. Cambridge: Cambridge University Press.