generated at
集合指標実例の圏
集合ベースの指標実例の圏
WIP
definition
一般の場合と対比するため、明示的に「1-」と書く
1-圏\mathbf{Set}_×におけるΣモデルの圏\mathbf{Model}(Σ) \: \mathrm{in} \: \mathbf{Set}_× = [Σ.\mathbf{F},\mathbf{Set}_×]_{\mathbf{CCC}_×}
インデックス付き圏
where
\mathbf{SIGN}
1-指標圏
Σ \colon \mathbf{SIGN}
1-指標
\mathbf{CCC}_× = \left\lang \mathbf{CCC};×,\mathbf{I},[]_{\mathbf{CCC}_×};\dots \right\rang
「（小さいとは限らない）1-デカルト閉圏」のデカルト閉圏
\mathbf{Set}_× \colon \mathbf{CCC}_×
\mathbf{Set}_× = \left\lang\mathrm{ CCC }\colon\mathbf{Set};×,I,[,];\dots\right\rang
集合と写像の圏を1-デカルト閉圏にしたもの
\mathbf{F} \colon \mathbf{SIGN}→ \mathbf{CCC}_×
自由函手
\left\lang \mathbf{F} ⊣ \mathbf{U} \colon \mathbf{SIGN}→ \mathbf{CCC}_×, \boldsymbol{η}, \boldsymbol{ε} \right\rang
自由-忘却随伴系
モデル函手
\mathbf{Model}= [\_.\mathbf{F},\mathbf{Set}]_{\mathbf{CCC}_×}
\colon \mathbf{SIGN}^\mathrm{op}→\mathbf{CCC}_×
対象
指標の実例
M : \mathbf{Model}(Σ)=[Σ.\mathbf{F},\mathbf{Set}_×]_{\mathbf{CCC}_×}
M \colon Σ.\mathbf{F}→\mathbf{Set}_× \colon \mathbf{CCC}_×
自由-忘却随伴系\mathbf{F} ⊣ \mathbf{U}より転置として指標の準同型が対応
指標の割り当て
M^∩ \colon Σ → \mathbf{Set}_×.\mathbf{U} \colon \mathbf{SIGN}
M^∩=Σ.\boldsymbol η * M.\mathbf U
where
\boldsymbol η \colon \mathbf{SIGN}^\wedge ⇒ \mathbf{F} \# \mathbf{U}
\boldsymbol ε \colon \mathbf{U} \# \mathbf{F} ⇒ \mathbf{CCC}_×^\wedge
演算子
SetSIGNCCC?
1;**#
2;;*
射
指標の準同型
P\colon M→N : \mathbf{Model}(Σ)
P\colon M ⇒N\colon Σ.\mathbf{F}→\mathbf{Set}_× \colon \mathbf{CCC}_×
転置
P^∩\colon M^∩ ⇒ N^∩ \colon Σ → \mathbf{Set}_×.\mathbf{U}
P^∩=Σ.\boldsymbol η * P.\mathbf U