Towards constructivising the Freyd-Mitchell embedding theorem

TL;DR

This paper develops a constructive approach to the Freyd-Mitchell Embedding Theorem, adapting it to constructive set theories like CZF by embedding small abelian categories into sheaves of modules over ringed spaces.

Contribution

It introduces a constructive alternative embedding method for small abelian categories, extending the classical theorem to settings compatible with constructive mathematics.

Findings

Classical proof does not work in CZF

Constructive embedding into sheaves of modules over ringed spaces

Inspired by Erik Palmgren's intuitions

Abstract

The aim of the paper is to first point out that the classical proof of the Freyd-Mitchell Embedding Theorem does not work in CZF; then, to propose an alternative embedding of a small abelian category into the category of sheaves of modules over a ringed space, which works constructively. It is necessary to mention that this work has been initially inspired by Erik Palmgren, who unexpectedly passed away in November 2019: I'm very grateful to him for having shared with me his intuitions, and for having supervised the realization of the first half of the paper.