日々の流転

λ. “Functorial Semantics of Algebraic Theories” by F. William Lawvere

ちょっと前に読んだ論文。 代数セオリーやそのモデルの形式化を最初に見たときは「へぇー」と思った。 言われてみれば当たり前なんだけどね。 どう形式化するかというと、代数セオリーを自然数を対象とし対象nが対象1*1のn個の直積となっている小さな圏Aとして定義する。 例えば群であれば、この条件と以下から自由生成される圏がセオリーになる。

• e : 0→1
• inv : 1→1
• μ : 2→1
• μ∘〈e, id〉 = id
• μ∘〈inv, id〉 = id
• μ∘〈μ, id〉 = μ∘〈id, μ〉

同様に束を考えると、前述の条件と以下から自由生成される圏がセオリーになる。

• ∨, ∧ : 2→1
• true, false : 0→1
• ∧∘〈π₂, π₁〉 = ∧
• ∨∘〈π₂, π₁〉 = ∨
• ∧∘〈∧, id〉 = ∧∘〈id, ∧〉
• ∨∘〈∨, id〉 = ∨∘〈id, ∨〉
• ∧∘〈id, true∘!〉 = id
• ∨∘〈id, false∘!〉 = id
• ∧∘〈id, id〉 = id
• ∨∘〈id, id〉 = id
• ∧∘〈π₁, ∨〉 = π₁
• ∨∘〈π₁, ∧〉 = π₁

そして、セオリー間の射を対象を保存する関手とし、これらのなす圏をJとする。 セオリーAのモデルとなる代数はAからSetへの直積を保存する関手と考えられるし、準同型は関手の間の自然変換と考えられるので、A代数の圏は一種の関手圏。Jの射 f : A→B に対して関手 Set^f : Set^B→Set^A はB代数の圏からA代数の圏への忘却関手になり、この関手の左随伴が存在する。

さらに、ある圏があるセオリーの代数の圏になっているための条件、などなど。

【2008-11-19追記】 ところで、どっかで見たような話だなぁと思ったら、Conceptual Mathematics: A First Introduction to Categories(F. William Lawvere/Stephen Hoel Schanuel) の ARTICLE III: Examples of categories の 11. Types of structure あたりでこういう話は散々やったのだった。 もちろん、Conceptual Mathematics ではこんなにシステマティックにやってはいないけど。