トップ «前の日記(2008-11-12) 最新 次の日記(2008-11-14)» 月表示 編集

日々の流転


2008-11-13 [長年日記]

λ. “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
  • ∧∘〈π2, π1〉 = ∧
  • ∨∘〈π2, π1〉 = ∨
  • ∧∘〈∧, id〉 = ∧∘〈id, ∧〉
  • ∨∘〈∨, id〉 = ∨∘〈id, ∨〉
  • ∧∘〈id, true∘!〉 = id
  • ∨∘〈id, false∘!〉 = id
  • ∧∘〈id, id〉 = id
  • ∨∘〈id, id〉 = id
  • ∧∘〈π1, ∨〉 = π1
  • ∨∘〈π1, ∧〉 = π1

そして、セオリー間の射を対象を保存する関手とし、これらのなす圏をJとする。 セオリーAのモデルとなる代数はAからSetへの直積を保存する関手と考えられるし、準同型は関手の間の自然変換と考えられるので、A代数の圏は一種の関手圏。Jの射 f : A→B に対して関手 Setf : SetB→SetA は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 ではこんなにシステマティックにやってはいないけど。

Tags: 論文 圏論

*1 終対象ではないので注意。