Catの性質と計算

どうでもいいようなことではあるが； 2圏Catのハナシ。

F:A→Bによる引き戻しF^★:Cat(B, C)→Cat(A, C) を次のように定義する。

• G:B→C に対して、F^★(G) = F;G :A→C
• β::G→G':B→C に対して、(F^★(β))_a = β_Fa::F;G→F;G':A→C

G∈|Cat(B, C)|に対してF^★G∈|Cat(A, C)|、β∈Cat(B, C)に対してF^★β∈Cat(A, C)、F^★が反変関手になっていることは確かめられる。よって、F|→F^★ は、Cat(A, B)→Cat(Cat(B, C), Cat(A, C)) になっている。

Cat(-, -)を[-, -]と書くと、(-)^★:[A, B]→[[B, C], [A, C]]。ここで、Cは本質ではないから、(-)^★:[A, B]→[[B, -], [A, -]] とかける。[[B, -], [A, -]]をキチンと定式化すると、米田埋め込みに似てるような？

G:B→Cに対しては、G_★(F) = F;G, (G_★(α))_a = G(α_a) として共変の(-)_★も定義できる。

ところで、自然変換ι::F→F:A→Bをι_a = id_Fa :Fa→Fa で定義する。ιはFごとに決まるから、ιFと書く。すると、(ιF)*β = F^★β、α*(ιG) = G_★α が成立する。

(-)^★、(-)_★、ι(-)などで計算が簡単になるか？