Freyd–Mitchell 嵌入定理

说明

⭐ 它的意义是：追元素这件事为什么是合法的。 小阿贝尔范畴里的命题，都可以先沿一个全忠实正合函子嵌进 $A\text{-}\mathbf{Mod}$，在那边（元素有意义的地方）证完再搬回来。「在一个具体的范畴里追元素」因此是一种合法的推广手段。

⚠️ 但它不是证蛇引理、五引理的常规手段 —— 那是大定理，标准证明本身就要在阿贝尔范畴里先搭一套正合性工具，拿它去证那两条是杀鸡用牛刀。那两条有初等的泛性质 / 泛元证明（见各自节点）。

为什么要求小：证明要把 $\mathcal{C}$ 里的对象做成模，用的正是「全体 $\hom$ 集合」的余极限构造；范畴不小的话这些集合是真类，做不成模。

⚠️ 对偶版本：同样的论证给一个嵌进 $\mathbf{Mod}\text{-}A$（右模）的版本；$A$ 不唯一，构造依赖选定的生成元。

与 Giraud 定理对照：Giraud 是把拓扑斯说成「预层范畴的正合反射子范畴」，Freyd–Mitchell 是把小阿贝尔范畴说成「模范畴的全忠实正合子范畴」—— 两条定理是同一个思路（「找一个具体的大范畴把自己装进去」）在不同结构上的版本。