Towards constructivising the Freyd-Mitchell Embedding Theorem

Anna Giulia Montaruli

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 show how to embed in a constructive way a small abelian category into the category of sheaves of modules over a ringed space.

Keywords: abelian categories, embedding, CZF, IZF, constructive mathematics

2020 MSC: 18E10, 03G30, 18E20, 03F65

Theory and Applications of Categories, Vol. 41, 2024, No. 40, pp 1416-1438.

Published 2024-10-08.

http://www.tac.mta.ca/tac/volumes/41/40/41-40.pdf

TAC Home