「量子と古典の物理と幾何＠名古屋」まで1月を切ってしまったので、話題について考えて、このブログに記録することにします。実際にこう話すとか事前に読んで欲しいとかいうものではなくて、自分の考えをまとめるために書くものです。
全体のストーリーは置いといて（まだ確定してない）、道具として（たぶん）PROを使います。なので、PROの話をします。とはいえ、PROを前面に出したりはしないでしょう。あくまで背景にPROがあるだけです。
内容：
PRO
PROは、prodocut（積）の最初の3文字を取った名前らしいです。酷いネーミングだな、と思いますが、既に使われている名前なので、そのまま使います。PROは特殊なモノイド圏のことです。モノイド圏PがPROだとは：
より正確には、|P| がNと同型というべきでしょうが、気にしないことにして、|P| = N と考えます。定義から、PRO Pは厳密モノイド圏で、単位対象は自然数0となります。PROの例をいくつか挙げます。
- Nから作った離散圏（射は恒等射だけ）に、足し算でモノイド積を入れたモノイド圏。
- Nに大小関係の順序を考え、順序から作ったやせた圏に、足し算でモノイド積を入れたモノイド圏。
- 適当な係数（成分）半環Kに対する行列圏に対角ブロック和でモノイド積を入れたモノイド圏
- 組み紐の圏、モノイド積は組み紐の併置。「はじめての圏論 中間付録B：アミダとブレイド」参照
- テンパリー／リーブ圏、「テンパリー／リーブ圏とカウフマンのスケイン関係式」参照
PROは単なるモノイド圏ですが、対称モノイド圏とした場合がPROPです。nLabによると、"product category"と"products and permutations category"の略称がPROとPROPとのことです。permutationは対称（symmetry）と同じ意味なので、PROPは対称PRO（symmetric PRO）と呼んだほうが辻褄が合うと思います。
PRO, PROP（対称PRO）と同様に、自然数の足し算の上に載ったデカルト・モノイド圏はローヴェル・セオリー（Lawvere theory）とか代数的セオリー（algebraic theory）とか呼びます。「セオリー（理論）」とは言っても単に圏のことです。これも、デカルトPRO（cartesian PRO）と呼べば辻褄が合うんですが、そう呼ぶことはないですね。
| 一般の場合 | 対象が自然数 |
|---|---|
| モノイド圏 | PRO |
| 対称モノイド圏 | PROP |
| デカルト・モノイド圏 | ローヴェル・セオリー |
PがPROのとき、Pからモノイド圏Cへのタイト・モノイド関手を、CにおけるPのモデルとか代数と呼びます。Pは1つの台対象（underlying object）を持つ代数系の定義とみなせます（後述）。プログラミング言語っぽい言い方をするなら、Pのモデルは「型クラスPのインスタンス」と言ってもいいでしょう。
指標と等式的公理系によるPROの構成
指標と等式的公理系を使ってPROを構成しましょう。指標（signature）とは、Nを頂点集合とする箙（「形容詞「複」「多」と箙〈えびら〉」参照）のことです。指標Σは Σ = (N, A, src, trg) と書けます。ここで：
Nはずっと固定するので省略して、記号の乱用で Σ = (Σ, src, trg) と書きます。また、n, m∈N に対して、Σ(n, m) := {a∈Σ | src(a) = n, trg(a) = m} とします。
箙としての指標のアローをオペレーション記号（演算記号、演算子）または単にオペレーション（演算）と呼びます。オペレーション記号aに対して src(a)をaのアリティ、trg(a)をaのコアリティと呼びます。この事情から、srcをarity、trgをcoariとも書きます。
指標Σに対して、Σを含む最小のPRO（Nを対象集合とする厳密モノイド圏）が同型を除いて一意的に決まります。このPROをFreePRO(Σ)と書き、指標Σで生成された自由PROと呼びます。アミダ図、ブレイド図（「はじめての圏論 中間付録B：アミダとブレイド」参照）、カウフマン図（「テンパリー／リーブ圏とカウフマンのスケイン関係式」参照）などの図からなる圏は、自由PROです。
アミダ図、ブレイド図、カウフマン図などでは、図を同値な図で置き換えることを許してました。これは、図のあいだに同値関係があり、商集合を考えていることを意味します。自由PROに等式の集まりによる同値関係を入れ、商を取る構成は頻繁に使われます。
PがPROのとき、P上の等式とは、Pの射のペア(f, g)のことです。ただし、arity(f) = arity(g), coari(f) = coari(g) という条件が付きます。いま、Eを、P上の等式の集合としましょう。Eが与えられると、厳密モノイド圏P上の合同関係が定まります。
P上の合同関係（coguruence）とは、射の集合Mor(P)上の二項関係〜で次を満たすものです。
- f〜g ならば、dom(f) = dom(f) かつ cod(f) = cod(g) 。
- 各ホムセットP(n, m)上で〜は同値関係である。
- f〜f' かつ g〜g' ならば、f;g 〜 f';g'
- f〜f' かつ g〜g' ならば、f
g 〜 f'
P上の等式の集合Eが与えられると、「(f, g)∈E ならば f〜g」を満たすような合同関係のなかで最小なものが決まります。この合同関係を〜Eとして、Mor(P) を合同関係で割ります（商集合を作る）。割った結果は再びPROになることが示せるので、それをP/E と書くことにします。(P/E)(n, m) = P(n, m)/〜E です。
指標ΣとFreePRO(Σ)上の等式の集合Eのペア(Σ, E)を等式的仕様（equational specification）と呼びます。このとき、Eを等式的公理系（equational (system of) axioms）といいます。等式的仕様(Σ, E)に対して、PRO(Σ, E) := FreePRO(Σ)/E と定義します。
等式的仕様の例
等式的仕様として、一番よく引き合いに出される例はモノイド仕様でしょう。指標Σを次のように定義します。
- Σ(2, 1) = {μ}
- Σ(0, 1) = {ε}
- その他のΣ(n, m) = {}
FreePRO(Σ)の結合（の記号）を「;」、モノイド積を「」とします。対象に関しては、n
m = n + m です。E = {assoc, lunit, runit} として、それぞれの等式は次のようにします。
- assoc = ((μ
- lunit = ((ε
- runit = ((id1
もう少し普通の書き方をすると：
- μ:2→1
- ε:0→1
- assoc:: (μ
- lunit:: (ε
- runit:: (id1
以上で決まる等式的仕様が「モノイドの仕様」です。
(Σ, E)がモノイドの仕様のとき、厳密モノイド圏PRO(Σ, E)から（厳密とは限らない）モノイド圏Cへのタイト・モノイド関手FがPRO(Σ, E)のモデルまたは代数です。今の場合は、モデルはモノイド圏C内のモノイドになります。F(1)∈|C| がモノイドの台対象となります。F(n) = F(1)n と、自然数nに対する値はF(1)のモノイド積累乗になります。
モノイド圏Cを変えると、色々なモノイド概念が得られます。通常のモノイド（集合圏のモノイド）以外に、結合的多元環（ベクトル空間の圏のモノイド）やモナド（自己関手圏のモノイド）などがあります。
可換モノイドを定義するには、変数を入れ替える σ:2→2 を指標に入れて、入れ替え（置換、対称）の等式的公理系を追加しておく必要があります。このような手間を省くには、最初から対称が入ったPROP（対称PRO）を使えば楽です。同様に、変数のコピーと破棄も必要なら、ローヴェル・セオリー（代数的セオリー、デカルトPRO）を使えばいいでしょう。
PROと代数系の圏
2つのモノイド圏C, Dに対して、TightMon(C, D)はタイト・モノイド関手の全体とします。モノイド自然変換も一緒に考えることにして、TightMon(C, D)は圏として扱います。
(Σ, E)を前節で定義したモノイドの仕様として、タイト・モノイド関手 PRO(Σ, E)→C はC内のモノイドを決めます。つまり、C内のモノイドの全体をMon(C)とすると：
- Mon(C) = TightMon(PRO(Σ, E), C)
モノイドという代数系とその準同型射からなる圏は、モノイド仕様(Σ, E)に対するPROからの関手圏として定義できるわけです。
これはモノイドに限らず、単一の台対象（underlying object）を持つ代数系（単ソート代数という）は、適当なPRO（あるいはPROP、ローヴェル・セオリー）からの関手とみなせます。当該の代数系と準同型射のなす圏は、関手圏として構成できます。
以上のことは、「代数系を関手で表現できる」ことを意味します。逆に考えると、「関手を代数系で表現できる」可能性も示唆します。実際、タチの良い関手は代数系でエンコードできることがあります。
「量子と古典の物理と幾何＠名古屋」では、とある現象を定式化する関手を、代数系にエンコードする事例を示すつもりです（予定）。
