Questions tagged [abelian-category]
The notion of abelian category is an abstraction of basic properties of the category Ab of abelian groups, more generally of the category RMod of modules over some ring, and still more generally of categories of sheaves of abelian groups and of modules. It is such that much of the homological algebra of chain complexes can be developed inside every abelian category. (from nLab)
1
question
20
votes
1
answer
314
views
Examples of formalisation of abelian categories
The question
I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and ...
- 2,500