Fredom-Mitchell嵌入定理的构造化
Towards constructivising the Freyd-Mitchell embedding theorem
摘要：
本文的目的是首先指出经典的证明Freelanc-Mitchell嵌入定理不工作的CZF，然后，提出一个替代嵌入的小阿贝尔范畴到范畴的层模在戴环空间，它的工作建设性。有必要提到的是，这项工作最初受到Erik Palmgren的启发，他于2019年11月意外去世：我非常感谢他与我分享了他的直觉，并监督了论文前半部分的实现。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
