反ラックス・モノイド余モナドの計算(ストライプ図絵算)をゴニョゴニョしているときに気付いた等式があります。とりあえずその等式を、余モナドのパンツマジック等式〈pants magic equation〉と呼んでおきます。ストライプ図を眺めると、下着〈パンツ〉の上にズボン〈パンツ〉を履いていたのに下着だけになってしまうマジックに見えるからです。
ある観点から見ると、パンツマジック等式は自明な等式でした -- 「なーんだ」という気分になりました。なので、この記事はボツにしようかとも思ったのですが、ゴニョゴニョの過程がまったく無意味というわけでもなさそうです。余クライスリ圏 の計算をもとの圏 で行うとき、パンツマジックに関連する技法や概念が使えます。計算練習/計算事例として多少の意味はあるでしょう。
内容:
- 最初の記事(シリーズ目次あり): 準マルコフ圏からなる2-圏
- 次の記事: ??
- 前の記事: モノイド圏: 評価写像の双関手性
後知恵から言うと
この記事のパンツマジック等式は、モノイド圏上の反ラックス・モノイド余モナド の余クライスリ圏 のなかで考えると次の等式に相当します。
これは当たり前。
この記事のシングレットという概念は、 とした恒等射 の における表示です。また、シングレット=クライスリ恒等射は、次の可換図式の縦方向の辺で与えられます。
と、このような事情を前もって知っていれば、この記事の書きっぷりはだいぶ変わっていたでしょう。もっとスッキリした展開になっていたはずです。が、発見的なガチャガチャした計算をそのまま残すのも一興かと思い、最初書いたストーリーを修正せずに記します。後知恵に基づく整理は別記事にします。
セットアップと記法
「反ラックス・モノイド余モナド: 記号の使用・乱用 再考」で述べた記法を使います。
はモノイド圏で、 は反ラックス・モノイド自己関手とします。そして、 を、 を台とする 上の余モナドとします。余モナドの余乗法・余単位は反ラックス・モノイド自然変換です。それは以下が成立することです。
- ( は単位対象)
余モナド と、その台である反ラックス・モノイド関手 をオーバーロード(意図的に混同)はしません。が、反ラックス・モノイド関手 と台関手 はオーバーロードします。つまり、反ラックス・モノイド関手の台関手を と書くことがあります。
に対して、「モノイド圏: 評価写像の双関手性」で導入した評価写像〈evaluation map〉の略記を使います。
モノイド圏とは限らない圏の一般的な話として、 が関手(単なる関手)で、 のとき、次の記法を使います。
'' は、関手版fmapの中置演算子記号です。「反ラックス・モノイド関手の一般余結合律」で既に使っています。
同様な記法を自然変換に対しても使います。 が自然変換、 のとき:
対象/射、関手/自然変換の記述のために、「準マルコフ余モナドの計算と記述の方法」で紹介した行列形式記法を使います。ただし、対象と射が区別しやすいように、射には矢印を添える記法を使います。例えば、 の書き方ならば:
以前の記法
新しい記法
余モナドのパンツマジック等式の記述
前節のセットアップと記法に従い、余モナドのパンツマジック等式を記述します。次は前もって決まって固定されているとします。
- : モノイド圏 上の反ラックス・モノイド余モナド
- : 台関手(記号の乱用)
は、「反ラックス・モノイド関手の一般余結合律」で定義した一般余乗法〈generic comulitplication〉です。これは、反ラックス・モノイド関手 から決まるので のように書くべきですが、反ラックス・モノイド関手は事前に決まっているので省略します。
余モナドのパンツマジック等式〈pants magic equation〉は次の主張です。
BUNツリー を変えると、見た目は違った様々な等式が得られます。
なぜパンツマジックなのか
余モナドのパンツマジック等式を、 の場合に考えてみます。記述は次のようになります。
等式の左辺のレイアウトを変えてみます(内容・意味は変わりません)。赤字の番号を追加しています。
これをストライプ図に描けば次のようになります。
これが、下着の上にズボンを履いている姿に見えるだろう、ということです。ただし、下着は、レスリングのウェアのように上半身から繋がっていると考えてください(下の写真)。レスリングウェアはシングレット〈singlet〉と呼ぶんだそうです。ズボンも、股上が長いサルエルパンツ〈saruel pants〉を想定してください(その下の写真)。
赤で描いてあるのは、いずれも自然変換の成分である射です。これらはストリング図のノードですが横線で描いています。2番、5番は視認性の都合で“代表点”を描いていますが、これも自然変換の成分です。シングレット&ズボンの比喩から次のように呼ぶことにします。
- ベルト: 余モナドの余乗法
- シングレットの股: 反ラックス・モノイド関手の余乗法
- シングレットの左裾: 余モナドの余単位
- シングレットの右裾: 余モナドの余単位
- ズボンの股: 反ラックス・モノイド関手の余乗法
- ズボンの左裾: 余モナドの余単位
- ズボンの右裾: 余モナドの余単位
さて、等式の右辺をストライプ図で描くと次のようです。
シングレットだけが残りベルトやズボンが消えています。マジックです。もちろんこの言い回しは比喩的なコジツケなので、あまり真に受けないでくださいね。
[/補足]
典型的パンツマジック等式の証明
前節で出した に対するパンツマジック等式を証明しましょう。
余モナド の余乗法や余単位は、反ラックス・モノイド自然変換なので、反ラックス・モノイド関手の余乗法と協調します。これは、余モナドの余乗法・余単位の位置と反ラックス・モノイド関手の余乗法の位置を入れ替え可能なことを意味します(「セットアップと記法」の冒頭参照)。このことを利用してパンツマジック等式を示します。
やり方は2通りあります。ひとつは、1番のベルトと3番・4番のシングレットの裾を、5番のズボンの股より下まで下げてしまうやり方。もうひとつは、3番・4番のシングレットの裾を2番のシングレットの股より上に上げるやり方です。
ここでは後者の方法で計算します。等式の左辺を再掲すると:
まずは3番・4番の移動。中段のブロックに次の等式を適用します。
次のように変化します。
上2つのブロックをまとめて簡略化します。
上段のブロックは、余モナドの余単位律から になるので、残るのは下段のブロックだけです。
これで、目的の右辺が得られました。
赤字の番号を見ると、もともとあったズボンが残って、ベルトとシングレットのトランクス部分が消えたことになります。これは、マジックとしてはインパクトに欠けますね。別なやり方のほうでは、ベルトとズボンを膝下まで下げた後で、ベルトとズボンが消えます。この方法も確認してみてください。
単純さと汎用性からは、今述べた内側のシングレットの裾を上げる方法のほうが有利です。
特殊な場合のパンツマジック等式
前節で の場合のパンツマジック等式を示しました。BUNツリーごとにパンツマジック等式の具体形があります。 と のときのパンツマジック等式もみておきましょう。BUNツリーを生成する基本記号とモノイド圏の単位対象がどちらも なので注意してください。
まず、パンツマジック等式に出てくる反ラックス・モノイド関手の一般余乗法 の特殊ケースを確認しておくと:
ここで次のような等式を使っています。
一般余乗法の特殊ケースとして恒等射や余単位も含まれていたわけです。
の特殊ケースも確認しておくと:
これらの値(対象や射)を、一般的パンツマジック等式に代入すると目的の具体形が得られます。
の場合:
恒等射を取り除くと:
これは確かに成立しています。
の場合:
恒等射を取り除くと:
これも成立しています。
シングレット
例え話として「シングレット」(レスリングウェア)という言葉を出しました。「シングレット」を、反ラックス・モノイド余モナドに関連するテクニカルタームとして定義しましょう。
今まで同様、 は、モノイド圏 上の反ラックス・モノイド余モナドとします。シングレットは、BUNツリーと対象のリストに対して定義されます。次の記号でシングレットを表します。
反ラックス・モノイド余モナドは前もって決まっているので省略してかまいません。
シングレット〈singlet〉の定義は以下のようです。
シングレットを構成するために必要な素材は、余モナドから得られるので、余モナド が決まっている状況ではシングレットを定義できます。
シングレットを使えば、パンツマジック等式は簡略に書けます。
おわりに
前節で定義したシングレット は、余クライスリ圏 の恒等射 (の表示)のことです。「反ラックス・モノイド余モナドの余クライスリ圏 その1」の記号の約束に従うと、余クライスリ圏の恒等射にはハットを付けるので、次のように書けるでしょう。
最初の節で述べたように、余クライスリ圏 では自明な等式を、もとのモノイド圏 のなかでガチャガチャ計算していたわけです。 のなかでのガチャガチャした計算が必要になることもあります。今回の話は、そんなときに参考になるかも知れません。