コゥゼン代数再び

http://d.hatena.ne.jp/m-hiyama-memo/20100109/1263025526 で「Σコゥゼン σ-順序代数」てのを導入したが、あれは大事だ。すごく役に立つ。

公理が：

1. [ジョイン演算の保存]f(..., x∪y, ...) = f(..., x, ...)∪f(..., y, ...)
2. [全射性（生成性）] ∪f(1, ...,1) = 1、ただしすべてのf∈Σに関して合併をとる。fには定数記号も含まれる。
3. [分離性（排他性）] f≠g ならば、f(1, ..., 1)∩g(1, ..., 1) = 0。f, gには定数記号も含まれる。
4. [非退化性] 有限個のx_iに関して ∧(x_i ≠ 0) ならば、f(x, ..., x) ≠ 0

となっているが、∪や1という定数をやめて、別な定式化をしたほうが良さそうだ。

1. [単調性]すべてのfに対して、x≦y ならば f(..., x, ...) ≦ f(..., y, ...)
2. [全射性（生成性）] これは生成系の定義とする。最初からは仮定しない。
3. [分離性] f(x1, ..., xn) = g(y1, ..., ym) ならば、f=g （したがって、n = m）。かつ、xi = yi。
4. [非退化性] f(x, ..., x) = 0 ならば、どれかのiでx_i = 0。

≦ は台となる順序集合の順序で、0は最小元。つまり、台は最小元を持つことは仮定する。fの全体は集合Σだが、これは擬積指標と呼ぶことにする。擬積（pseudo product）とは、積に似た演算だが、ほんとに積である必要はないような演算記号。上の公理は、擬積が単調非退化な演算であり、分離性を満たすことを言っている。分離性はエルブラン性と言ってもいいだろう。

Σが無限集合、つまり無限個の擬積を持つ場合が重要だ。

[追記]

Σはユーザーが指定可能（プラッガブル）な指標だが、小文字のσのほうは構文フレームワークに作り付け。σには普遍的に使う定数と演算が含まれる。

σとΣが決まると指標が固定されるので、これで代数（指標のモデル）を考えることができるようになる。固定されたσ-Σに対するモデルの圏 Mod[σ-Σ] が出来る。Mod[σ-Σ] の対象であるσ-Σ代数Aに対して、その生成系を定義できる。Bが生成系のとき、σ-Σ, B, Var（変数集合）を使って、項（あるいは多項式）の集合 Term(σ, Σ, B, Var) を定義できる。Termにイッパイ引数があるから、これを色々と変えたり固定したりすると、面白いことができる、ってわけだ。

ここらへんはまさに、エルブランやコゥゼンがやったことだよね。

[/追記]