In this repository, I slowly work towards some form of homological algebra in the Lean theorem prover. For now, I'm busy proving basic facts about abelian categories.
- Preadditive categories and biproducts (this will hopefully be made obsolete soon by enriched categories in mathlib)
- The definitition of an abelian category
- We use a relatively low-tech definition while still requiring preadditivity
- Basic facts about abelian categories
- Image factorization
- mono + epi = iso
- The pullback of an epimorphism is an epimorphism
- The definition and basic facts about exactness
- Pseudoelements
- The definition and the usual characterizations of exactness etc.
- A buggy and inefficient tactic that chases pseudoelements
- Proofs of the four lemma, the kernels' lemma and the snake lemma (the general one) valid in any abelian category
- A proof that the category of modules is abelian
- and also that categorical exactness means precisely
f.range = g.ker - A proof of the four lemma for modules that works by specializing the four lemma for abelian categories to the category of modules
- and also that categorical exactness means precisely
There used to be some other things in here which I have since deleted. Some of these have since found their way into mathlib.