Abstract
Many facts about abelian groups and R-modules are proved using the technique of diagram chasing. For example, to prove that a certain map is surjective, one takes an element of the codomain and traces it through a diagram to eventually get a preimage. In more general abelian categories, the objects don’t have elements, so to make this technique possible, one often relies on embedding theorems that depend on classical principles. Mac Lane proposed a method that does not use an embedding theorem, but which had limitations. We show that a simple extension of this method works quite well in practice, with the aid of a tactic that makes it appear that we are dealing with elements in a naive way. We will illustrate this with proofs of some standard results that exactly parallel the traditional proofs.
This is joint work with Thomas Thorbjørnsen.
Talk Details
Speaker: Dan Christensen (University of Western Ontario, Canada)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Thursday 18 December 2025
Time: 16:25 (remote)
Key Topics
- Diagram chasing
- Abelian categories
- Coq-HoTT library
- Homotopy type theory
- R-modules
- Abelian groups
- Mac Lane’s method
- Embedding theorems
Collaborators
- Thomas Thorbjørnsen