Anna Montaruli: A constructive perplexity on the Freyd-Mitchell Embedding Theorem

Abstract

The Freyd-Mitchell Embedding Theorem asserts that every small abelian category admits a full exact embedding into a category of modules over a certain ring. At this point, one can ask: which logical setting allows the proof of the theorem? Is the theorem still true in CZF (Constructive Set Theory)?

In this talk, after a brief introduction to CZF and Category Theory, we show that part of the proof of the Theorem seems to not work unless we suppose the axiom of Power Set, which is not included in CZF.