このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

[参照用 記事]

リントンの定理

「ローヴェア・セオリーのモデルの圏と、ローヴェア・セオリーに対応するモナドのアイレンベルク/ムーア圏が圏同値である」という結果は、リントン〈Fred Linton〉が示したのだと僕は思っていました。しかし、リントンのオリジナルの論文 "Some aspects of equational categories" (1966) を読んだわけではないので、間接伝聞で知った、ということです。

では、その間接伝聞のソースは何だったのでしょう? 思い出せないので検索で探してみたら、ハイランド/パワーの次の論文のようです。

この論文内に次の記述があります。[29] はリントンの1966年論文のことです。

Linton [29] made the general connection between monads and Lawvere theories (universal algebra): every Lawvere theory gives rise to a monad on Set whose category of algebras is equivalent to the category of models of the Lawvere theory, and, subject to a generalisation in the definition of Lawvere theory, every monad arises thus, uniquely up to coherent isomorphism.


リントン [29] は、モナドとローヴェア・セオリー(普遍代数)とのあいだの一般的な関係を確立した: すべてのローヴェア・セオリーは、集合圏上のモナドを生成する。そのモナドのアイレンベルク/ムーア代数の圏は、ローヴェア・セオリーのモデルの圏と圏同値となる。ローヴェア・セオリーの定義を一般化すれば、すべてのモナドはこの方法で生成できて、一貫性同型を除いて一意的である。

リントンが厳密な証明をしたかどうかは定かではありませんが、ハイランド/パワーの文言によれば、リントンは「モナドのアイレンベルク/ムーア圏とモデルの圏は圏同値である」ことを認識していたようです。なので、当該の定理は「リントンの定理〈Linton's theorem〉」と呼んでもよさそうです。ただし、「リントンの定理」として、"Linton’s monadicity theorem" というのがあるらしく*1、そっちのほうが有名なのかも知れません。事情を明確にしたいのなら、今話題にしている定理は「リントンの代数-モデル対応定理〈Linton's algebra-model correspondence theorem〉」と呼べば紛れがありません。

ローヴェア・セオリーに関して、「モナド-セオリー対応〈monad-theory correspondence〉」という言葉はよく使われます。リントンの定理もモナド-セオリー対応ですが、代数〈アイレンベルク/ムーア代数〉とモデルの対応のほうに注目したいと思います。

さてところで、「リントンの代数-モデル対応定理」はスケマティック(「スケマティック」参照)な状況でも成立するだろうと僕は信じています。これはどういうことかと言うと、「ストリング図、ストリング図動画が“使える”とは?」で述べたツールバッグ(指標と事実上同じ)にモデルの概念を定義し、ツールバッグからモナドを作る手順を確立すれば、「モナドのアイレンベルク/ムーア圏とモデルの圏は圏同値」だろう、ということです。

ツールバッグからモナドを作る手順では、ストリング図をヘビーに使うという意味で、極めてスケマティックです。具体例や状況証拠から、このスケマティックなモナドが存在することはまず間違いないのですが、具体的かつ詳細にモナドを構成しようとすると、だいーぶ大変、めんどくさい。

スケマティックなリントンの代数-モデル対応定理を完全に記述したいと、以前から思ってはいるのですが、そのめんどくささに気力が萎えてしまうのですよ。しかしまー、ちょびちょびと準備を重ねて、いつか完全な記述を完成させたいですね。


以下は、関連する記事へのリンク集となります。

*1:これも、1966年論文に記述されているそうです。