今天又看了一遍，这次总算是理清楚了，从头推到尾，没有跳过。
只能说，要看懂证明不容易啊。
开始的一部分是一些准备工作，给出问题的背景，定义一些要用的符号，比如双射，和自然变换
。标记的两个式子将会多次使用。
对于定义的自然变换，要验证自然性，也就是下图的交换性。这个通过函子F的性质可证。
接下来证明了的互逆性。其实就是同构。运算过程中用到了他们的定义，还有就是标红的那一步使用了自然变换
的自然性，这个没有给出，不过可以仿照着写出。于是，双射就证明完毕了，同构限制在集合范畴中就是双射。
然后是证明双射是自然的，因为定义里提及这个双射可视为A索引的自然变换。首先构造出所需的函子，毕竟自然变换是从函子到函子，定义中只给出了函子F，所以这里要把缺失的函子N定义出来。
接着定义了自然变换，
即双射关于A是自然变换，同样，要验证自然性。自然性成立，所以结论就成立了。
最后，当A是小范畴时，函子范畴是有意义的，开始证明双射关于F也是自然变换，首先，依然是定义所需的两个函子
。
然后，定义自然变换，
。验证自然性。
证明虽然是看懂了，但是对理解似乎没什么帮助。并且，从这个证明的复杂性而言，图形化的表示反而是一种累赘，因为涉及的范畴不是常见的类型，也很难提供什么直观的见解。不过，对于每一小块而言还是很有意义的。
网友评论