日々の流転

λ. スライスのスライスはスライス

Γを圏Cの対象とすると、そのスライスである圏C/Γが定義できる。 さらに、σを圏C/Γの対象とすると、そのスライスである圏(C/Γ)/σが定義できる。

さらに、Cにプルバックが存在するとき、σ^* : C/Γ → C/dom(σ) を id_Γ ∈ |C/Γ| に適用すると、σ^* id_Γ ∈ |C/dom(σ)| と dom(σ^* id_Γ) ∈ |C| が得られる。 dom(σ^* id_Γ) を Γ・σ と書くことにすると、(C/Γ)/σ と C/(Γ・σ) は等しい。

LCCC(locally cartesian closed category, 局所デカルト閉圏)の名前は、全てのスライスがCCC(cartesian closed category, デカルト閉圏)であることからきているが、LCCCにはプルバックがあるので、LCCCのスライスはCCCであるだけでなく、それ自体LCCCになっている。

Categories for Everybody のLCCCの話に関係して小ネタ。