米田引理的证明过程

今天又看了一遍，这次总算是理清楚了，从头推到尾，没有跳过。

只能说，要看懂证明不容易啊。

开始的一部分是一些准备工作，给出问题的背景，定义一些要用的符号，比如双射，和自然变换。标记的两个式子将会多次使用。

对于定义的自然变换，要验证自然性，也就是下图的交换性。这个通过函子F的性质可证。

接下来证明了的互逆性。其实就是同构。运算过程中用到了他们的定义，还有就是标红的那一步使用了自然变换的自然性，这个没有给出，不过可以仿照着写出。于是，双射就证明完毕了，同构限制在集合范畴中就是双射。

然后是证明双射是自然的，因为定义里提及这个双射可视为A索引的自然变换。首先构造出所需的函子，毕竟自然变换是从函子到函子，定义中只给出了函子F，所以这里要把缺失的函子N定义出来。

接着定义了自然变换，即双射关于A是自然变换，同样，要验证自然性。自然性成立，所以结论就成立了。

最后，当A是小范畴时，函子范畴是有意义的，开始证明双射关于F也是自然变换，首先，依然是定义所需的两个函子。

然后，定义自然变换，。验证自然性。

---

证明虽然是看懂了，但是对理解似乎没什么帮助。并且，从这个证明的复杂性而言，图形化的表示反而是一种累赘，因为涉及的范畴不是常见的类型，也很难提供什么直观的见解。不过，对于每一小块而言还是很有意义的。