一般忘却関手 続き
忘却関手、具象圏、構成関手 - 檜山正幸のキマイラ飼育記 メモ編、一般忘却関手 - 檜山正幸のキマイラ飼育記 メモ編 の続き。
普遍的な忘却先(?)としてSetを考える（これも相対化できるが、キリがないから止める）。圏BとCは、標準的（canonical）な忘却関手UB:B→Set、UC:C→Setを持つ。この段階では、忘却関手の定義はなくて、単に、UB、UCが天下りに与えられているだけ。ただし、これらは忠実関手（それ以上の条件は仮定しない）。
さて、さらにBとC上には、充足構造が与えられているとする。これは本質的にはインスティチューション構造のこと。以下に充足構造を説明するが、Bが“（部分）順序集合の圏”PO、Cが“ベキ等半環の圏”ISRだとして読むとよい。
Σ、Γが指標（記号の集合）だとして、等号を前もって備えた一階述語論理に指標を加えて論理式を作り、閉じた論理式全体をSen(Σ)などとする。Σ上のセオリーとは、Sen(Σ)の演繹で閉じた部分集合のことである。SがΣ上のセオリー（例：ISRの等式的セオリー）、TがΓ上のセオリー（例：POのホーン式のセオリー）だとする。
圏C上の充足構造とは、|C|とSen(Σ)の関係|=のこと。A |= ψは、対象Aが文（命題）ψを満たす（充足する）と読む。Sが任意の文の集合のとき、A |= S は、∀ψ∈S.[A |= ψ]の略記だとする。圏Cの任意の対象Aが、A |= S なとき、圏CはSを満たすという。Sがセオリーなら、圏CはセオリーSを満たす圏、あるいは単にセオリーSの圏などと呼ぶ。セオリーと圏を関係付けるためには、充足構造が必須である。
(C, Σ, |=)、(B, Γ, |=)が充足構造のとき、写像t:Sen(Γ)→Sen(Σ)と関手R:C→Bの組が次を満たすとき、充足構造のあいだの射（準同型）と定義する。
- X |= t(ψ) ⇔ R(X) |= ψ
tを翻訳写像、Rを還元（reduct）関手と呼ぶ。（ここらへんは、そっくりインスティチューションの定義だけど、個人的にはなんかイマイチしっくりこない。いずれまた考えよう。）
SがΣ上のセオリーで、CはSの圏になっている、同様にBはセオリーTの圏になっているとする（例：SがISRセオリー、TがPOセオリー）。翻訳t:Sen(Γ)→Sen(Σ）が、t(T)⊆S の性質を持つとする。ψ∈T を |-Tψ と書けば：
- |-Tψ ⇒ |-St(ψ)
のこと。例えば、|-POψ ⇒ |-ISRt(ψ) のようなこと。このような翻訳は、セオリーTからセオリーSへの翻訳と呼ぶ。
やっと準備ができた。ΓセオリーT、ΣセオリーS、Tの圏B、Sの圏C、翻訳t:Sen(Γ)→Sen(Σ)、関手U:C→Bがあるとき、Uが忘却関手とは：
- tはセオリーTからセオリーSへの翻訳である。
- tとUの組は充足構造の射になっている。X |= t(ψ) ⇔ U(X) |= ψ
- U;UB = UC
この定義でいちおう、JSLat（ジョイン半束の圏）がIAbMon（ベキ等アーベルモノイド）への忘却関手を持ち、IAbMonがAbMonへの忘却関手を持ち、したがって、JSLatもAbMonに忘却関手を持つことが示せる。C→Bの（相対的）忘却関手を持つなら、CはB上の具象圏と呼ぶ。
以上の議論、使えなくはないが、かなり不満が残る。後でもう少し整理・一般化しよう。
