トレース付きモノイド圏における結合

檜山正幸 (HIYAMA Masayuki)
Tue Mar 01 2005:start
Wed Mar 02 2005:prefinal

トレース付きモノイド圏(C, ×, 1, σ, Tr)において、 f;g≒TrYX,Z((f×g);σY,Z) を示す。

目次

1. はじめに

(C, ×, 1)がモノイド圏(monoidal category)で、対称(交差)σとトレー スTrを加えた(C, ×, 1, σ, Tr)がトレース付きモノイド圏(traced monoidal category)だとする。このとき、f:X→Y, g:Y→Z in Cに対して、次 が成立する(≒はisomorphic)。

これは、トレース付きモノイド圏で一般的に成立する事実として言及はされ るが、一般的には、特別に重大なことではないのかもしれない。しかし、僕に とっては非常に印象深い公式である。

というのも、この等式(同型)が成立することは、特別な状況における現象 としては1995年くらいから知っていたのである。僕が知っていた例では、対称 σの存在が分かりにくく(僕のイイカゲンな定式化のなかでは分かりにくかっ たということだが)、f;g=Tr(f×g) のように見えていた。つまり、圏の基本 演算である結合(composition)が、テンソル積(モノイド積)とトレースで 書けてしまうような形をしていた。

f;g=Tr(f×g) は、僕にとっては不可解であったし、気持ちの悪い現象だと感 じていた。なにか根本的に間違いを犯しているような不安もあった。だが、こ れはトレース付きモノイド圏が背後に存在する状況証拠だとわかって、やっと 気分が落ち着いた。

f;g≒Tr((f×g);σ)は、トレース付きモノイド圏の公理から簡単に示せるが、 簡単すぎるせいか、ハッキリとした証明が見あたらない。簡単とはいっても、 トレース付きモノイド圏に慣れてないと自明とは言えないだろう。そこで、 f;g≒Tr((f×g);σ) を具体的に示す。

2. 前提となる知識

左右のタイトニング(left/right tightening)、対称(交差)σの基本性質、 「ずらし」に関しては、記事「スーパーポージング公理 からスーパーポージング定理へ」のなかに図がある。ヤンキング(yanking) の絵は、記事「お絵描き圏論」内にあ る。

念のために、図を以下に再掲しておく。

トレース付きモノイド圏の完全な定義は、Masahito Hasegawa "Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi" 1997(CiteSeer.IST を探してみよ)にある。

FIG: 左タイトニングと右タイトニング

/* tightening */

FIG: クロス(対称)の基本性質

/* cross-axioms */

FIG: ずらし

/* shift */

FIG: ヤンキング

/* yanking */

3. f;g≒Tr((f×g);σ)の証明

TrYX,Z((f×g);σY,Z)からはじめて、 f;gへと変形する。図式の 変形を下に描いておいた。説明は下にある。

FIG: f;g≒Tr((f×g);σ)の証明

/* composition-in-tmc */

  1. f×gの部分を「ずらし」を使って、 (f×Y);(Y×g)にしておく。
  2. σの交差と(Y×g)を交換する。ここでは、 (Y×g);σY,ZY,Y;(g×Y)を使った。
  3. Trの被作用部は、(f×Y);σY,Y;(g×Y)となった。左タイトニングと 右タイトニングを使って、Trの被作用部をσY,Yに狭める。全体は、 f;TrYY,Y);g となる。
  4. ヤンキングを使うと、TrYY,Y)はY(恒等射)になる。 トレース作用素は消えて、f;Y;g となる。
  5. これはf;gに他ならない。