<譯>米田嵌入

上一篇：米田引理

原文地址：https://bartoszmilewski.com/2...

咱們以前已經看到，固定範疇C的一個對象，映射C(a, -)是一個從C到Set的（協變）函子。

x -> C(a, x)

(上域是Set是由於hom集C(a, x)是個集合。)咱們把這個映射叫hom函子——咱們以前也已經定義了它在態射上的行爲。

如今讓咱們變化這個映射中的a。咱們獲得了一個新的映射：給任意的a分配一個hom函子C(a, -)。

a -> C(a, -)

這是個從範疇C的對象到函子的映射，而函子是函子範疇的對象（參見天然變換有關函子範疇的部分）。讓咱們用記號[C, Set]表示從C到Set的函子範疇。你也可能會回憶起hom函子就是那些本來的可表函子。

咱們每有一個兩範疇的對象之間的映射的時候，就會很天然地問它是不是個函子。換句話說咱們是否能夠把一個範疇的態射提高到另外一個範疇。C的態射就只是一個C(a, b)的元素，但函子範疇[C, Set]的態射是天然變換。因此咱們想要找一個從態射到天然變換之間的映射。

讓咱們看看可否根據一個態射f :: a->b找到一個天然變換。首先，咱們得看看a和b被映爲了什麼。它們被映爲了兩個函子：C(a, -)和C(b, -)。咱們須要這兩個函子間的一個天然變換。

接下來就是技巧了：咱們使用米田引理：

[C, Set](C(a, -), F) ≅ F a

把通常的F帶成hom函子C(b, -)，咱們就獲得了：

[C, Set](C(a, -), C(b, -)) ≅ C(b, a)

這剛好就是咱們要找的那兩個函子間的天然變換，不過有點扭曲：咱們獲得了一個天然變換和態射間的映射——這個態射是C(b, a)的一個元素——這傢伙的方向「錯」了。但這沒有什麼問題；這只是意味着咱們處理的這個函子是逆變的。

實際上，咱們比所希求的獲得了更多。這個從C到[C, Set]的映射可不僅是個逆變函子——它是個徹底忠實函子。徹底性和忠實性是描述函子映射hom集時的性質。

忠實函子是說它在hom集上表現爲單射，也就是它把不一樣的態射映爲不一樣的態射。換句話說，它不會合並它們。

徹底函子是說它在hom集上表現爲滿射，也就是它把一個hom集滿映爲另外一個，徹底覆蓋後者。

數學中的滿射在英文中有兩種表達：一種是 surjective（滿射），另外一種是maps A onto B。也就是 onto在數學中有特殊的含義。這一句話就是做者把兩種說法都說了一遍，以解釋地更清楚。譯者注。

徹底忠實函子是說F在hom集上表現爲雙射——一個兩集合元素間的一一映射。對於源範疇C的每一對對象a和b，都有一個C(a, b)和D(F a, F b)間的雙射，其中D是F的靶範疇（咱們這裏就是函子範疇[C, Set]）。注意這並非說F就是個對象間的雙射。可能會有些D中的對象並不在F的像裏，從而咱們不能對這些對象的hom集說任何事情。

嵌入

咱們剛剛所說的這個把C的對象映爲了[C, Set]的函子的（逆變）函子：

a -> C(a, -)

就定義了米田嵌入。它把一個範疇C(嚴格地說，是範疇C^op，由於它是逆變的)嵌入到了函子範疇[C, Set]。這不只僅是把C的對象映爲了函子，並且它忠實地維持了它們之間的全部聯繫。

由於數學家們對函子範疇瞭解的不少，尤爲是那些上域爲Set的函子，因此這是個很是有用的結果。咱們能夠經過把任意範疇C嵌入它的函子範疇而獲得不少關於它的洞見。

固然米田嵌入也有一個對偶版本，它有時叫作逆米田嵌入。注意咱們能夠從固定每一個hom集的靶對象（而不是源對象）開始，也就是C(-, a)。這給了咱們一個逆變的hom函子。從C到Set的逆變函子就是咱們熟悉的預層（例如參見極限與餘極限）。逆米田嵌入定義了範疇C到預層範疇的嵌入。它在態射上的行爲由下式給出：

[C, Set](C(-, a), C(-, b)) ≅ C(a, b)

一樣地，數學家們對預層範疇也瞭解不少，因此能把任意範疇嵌入其中實在是個好事。

在Haskell中的應用

Haskell中，米田嵌入被表示成reader函子間的天然變換和（反向）函數的同構：

forall x . (a -> x) -> (b -> x) ≅ b -> a

（記住，reader函子等價於((->) a)。）

等價的左邊是個多態函數，給定一個a到x的函數和一個b類型的值，就能獲得一個類型x的值（我沒有用柯里化——也就是去掉了函數b -> x上的那個括號）。要對全部的x都能作這件事，惟一的方式就是咱們的函數知道如何把一個b類型的值轉換成一個a類型的值。這必然就隱晦地使用了函數b -> a。

給定這樣的一個轉換，btoa，就能夠定義左邊了，讓咱們叫它fromY：

fromY :: (a -> x) -> b -> x
fromY :: f b = f (btoa b)

反過來，給定一個函數fromY，咱們能夠經過用fromY調用恆等函數重構出這個轉換：

fromY id :: b -> a

這構建了類型爲fromY的函數到btoa的雙射。

審視這個同構的另外一個可能的方式就是它是一個從b到a的函數的CPS編碼。參數a->x就是延繼（那個處理器）。結果是個從b到x的函數，它須要一個b類型的值，它執行的是延繼前複合上被編碼的那個函數。

米田嵌入也解釋了一些Haskell中數據結構的其餘可能的表示方式。尤爲是，它根據Control.Lens庫提供了一種很是有用的representation of lenses。

這一篇 representation of lenses我沒有翻譯。米田嵌入是該做者範疇論的第二部分的最後一篇，我尚不知道下一步是先翻譯第三部分仍是翻譯一些這樣的零散文章。在我翻譯這一篇以後，我會把翻譯以後的連接補過來。譯者注。

預序的例子

這是Robert Harper所建議的一個例子。它是米田嵌入在由一個預序定義的範疇上的應用。一個預序就是帶上一個順序關係的集合，這個元素間的順序關係一般寫做<=（小於等於）。預序裏之因此有個"預"字是由於咱們只須要這個關係的傳遞性和自反性而不須要反對稱性（因此它是可能成環的）。

一個帶有預序關係的集合導出了一個範疇。集合中的元素就是對象，若是對象a和b無法比較或者a <= b是錯的，那a到b的態射就沒有，或者a <= b，那這個態射就存在，它由a指向b。一個對象到另外一個的態射永遠不會多於一個。因該範疇上的hom集要麼就是空集，要麼就是單例集。這樣的範疇稱爲薄的。

你很容易就能夠看出這的確構造了一個範疇：箭頭是可複合的，由於若是a <= b而且b <= c那麼a <= c；並且這個複合是結合的。咱們還有恆等箭頭，由於每一個元素（小於或）等於本身（這個關係的自反性）。

如今咱們能夠把逆米田嵌入用到預序範疇上了。特別地，咱們感興趣的是它在態射上的行爲：

[C, Set](C(-, a), C(-, b)) ≅ C(a, b)

右邊的hom集是非空的，當且僅當a <= b——這時它是個單例集。所以，若是a <= b，就存在一個左邊的天然變換。不然就沒有這樣的天然變換。

那麼預序的hom函子間的天然變換到底是什麼？它應該是一個從集合C(-, a)到C(-, b)的函數族。在預序裏，這些集合中的每個要麼是空的要麼是單例集。讓咱們看看咱們如今所處理的函數都是些什麼傢伙。

這裏的表達略微混亂，不過不影響理解。「這些集合中的每個要麼是空的要麼是單例集」應指像 C(x, a)和 C(x, b)這樣的傢伙，而不是 C(-, a)和 C(-, b)。譯者注。

從空集到自身有一個函數（也就是空集上的恆等函數），從空集到單例集有個absurd函數(它什麼也不作，由於這須要定義一個空集中的元素，但空集裏什麼也沒有)，從單例集到本身也有個函數(單例集的恆等函數)。惟一不被容許的組合方式是把一個單例集映爲空集（這個函數把那單個的元素究竟映爲了什麼呢？）。

因此咱們的天然變換永遠不能把單例集和空集連起來。換句話說，若是x <= a(C(x, a)是個單例hom集)那麼C(x, b)就不能爲空。一個非空的C(x, b)意味着x小於等於b。因此這個問題裏天然變換的存在性就須要對於每一個x來講，若是x <= a那麼x <= b。

for all x, x ≤ a ⇒ x ≤ b

另外一邊，反米田嵌入告訴咱們天然變換的存在性等價於C(a, b)是非空的，或者說a <= b。把這二者放到一塊兒，就獲得了:

a ≤ b if and only if for all x, x ≤ a ⇒ x ≤ b

咱們能夠直接獲得這個結果。直觀上說，若是a <= b那麼全部比a小的元素都要比b小。反過來，把右邊的x替換成a，就獲得了a <= b。但你必須認可經過米田嵌入獲得這個結果遠讓人更爲興奮。

天然性

米田引理構造了一個天然變換的集合和一個Set中對象的同構。天然變換是函子範疇[C, Set]的態射。兩個函子間天然變換的集合是這個範疇的一個hom集。米田引理是下面這個同構：

[C, Set](C(a, -), F) ≅ F a

這個同構能夠證實對於F和a都是天然的。換句話說，它在積範疇[C, Set] × C的序對(F, a)上是天然的。注意如今咱們把F當作函子範疇的一個對象。

讓咱們考慮下這意味着什麼。天然同構是兩個函子間的可逆的天然變換。確實，咱們的同構的右邊是個函子。這是個從[C, Set] × C到Set的一個函子。它在序對(F, a)上做用的結果是個集合——就是給函子F帶入對象a的執行結果。這樣的函子叫執行函子。

左邊也是個把(F, a)變到天然變換集合[C, Set](C(a, -), F)的一個函子。

爲了證實它們是真正的函子，咱們還應該定義它們在態射上的行爲。但序對(F, a)和(G, b)之間的態射是什麼？這是一對態射,(Φ，f)；第一個是函子間的態射——一個天然變換——第二個是C上的常規態射。

執行函子取序對(Φ, f)並把它映爲一個集合F a到G b間的函數。咱們能夠輕易地經過Φ在a上的份量（它把F a映爲G a）和被G提高後的態射f，構造出這樣一個函數：

(G f) ∘ Φ_a

注意，因爲Φ有天然性，因此這等同於:

Φ_b ∘ (F f)

我不會證實整個同構的天然性——在構建了函子以後，證實是很是機械化的。它利用了咱們的同構是創建在函子和天然變換上的這樣一件事。這很簡單，沒可能搞錯。

挑戰

1. 在Haskell中表達逆米田嵌入
2. 證實咱們創建的fromY和btoa之間的雙射是個同構（這兩個映射是互逆的）。
3. 用米田嵌入處理幺半羣。幺半羣的那個單個對象對應的是什麼函子？幺半羣態射對應的是什麼天然變換？
4. 協變的米田嵌入在預序上的應用是什麼？（Gershom Bazerman所提出的問題）
5. 米田嵌入能夠用來把任意函子範疇[C, D]嵌入到函子範疇[[C, D], Set]。指出它在態射（這裏是天然變換）上的行爲。

致謝

感謝Gershom Bazerman檢查個人數學和邏輯。

下一篇：有關態射的一切