Colimit作為Coend [S2W7]

Coend是functor P:Cop×C→DP : C^{op} \times C \to D 上的一種construction,回憶一下Profunctor我們知道這種functor對左邊逆變、對右邊共變,因此對任意 f:x→yf : x \to y 有

figure tex10615

如果考慮對所有co-wedge P(−,−)→dP(-,-) \to d 有一個universal construction,換句話說以下交換圖成立

figure tex10616

∫x∈CP(x,x)\int^{x \in C} P(x,x) 這個universal construction被稱為coend。給定functor FF 我們能定義一個profunctor PP

P(x,y):=F(y)P(f,g):=F(g)P(x,y) := F(y) P(f,g) := F(g)

現在假設profunctor PP 有universal construction,然後我們把 PP 按照定義機械替換成 FF

figure tex10617

就可以看到如果 FF 有colimit這樣的universal construction,必定與 ∫x∈CF(x)\int^{x \in C} F(x) 重疊,所以colimit可以用coend表示

∫x∈CF(x)=lim→⁡F\int^{x \in C} F(x) = \varinjlim F