米田埋込みと関手のモデル圏

Cが圏で、Cからの集合圏への共変関手を単にC-関手と呼ぶことにする。C-関手の全体はSet^C だが、上付きが嫌なら [C, Set] を使う。Cを[C, Set]に米田埋め込みできるが、埋め込み自体は反変関手になる。A∈|C|として、Aの埋め込み像をA_ とすると、関手 A_ は共変関手である。

• A_(X) = C(A, X) or A_ = C(A, -)
• A^(X) = C(X, A) or A^ = C(-, A)

普通は、A|→A^ を使うことが多い。このとき、埋め込み自体は共変で、A^はCからSetへの反変歌手となる。

米田の補題は、

• Nat(F, C(-, A)) = F(A) or Nat(F, A^) = F(A)
• Nat(C(A, -), F) = F(A) or Nat(A_, F) = F(A)

F∈[C, Set]を固定して、Fのオーバー圏を考える。[C, Set]/F ね。特に、ρ:A_ → F という形のオーバー圏の対象は、A_ と ρ∈F(A) の組で与えられる。AとA_を同一視すれば、Aとρ∈F(A)の組。

すると、Cを米田埋め込みした先で、特定のC-関手をベースとしたオーバー相対対象を考えることは、Aとρの組を考えることに等しい。Cの米田埋め込みの像をC_ として、C_/F をFモデルの圏とコンヌは呼んでいる。