…色々 ストリング図とストライプ図 演繹系とオペラッド 呼び名の約束内容的な説明をする前に、「セオリー」で混乱してしまうことを回避するために、次の約束をします。 ローヴェア・セオリーはある種の圏なので、ローヴェア圏〈Lawvere category〉とも呼びます。「ローヴェア圏〈ローヴェア・セオリー〉」とか「ローヴェア・セオリー〈ローヴェア圏〉」とかの書き方も使います。 ローヴェア圏は、それ以前から論理や普遍代数で使われていた等式的代数指標〈equational algebra…

…だけ解説しています。ストライプ図を潰して（幅や広がりをゼロにして）ストリング図にする技法も紹介しています。昨日の記事とこの記事では、描き方が多少違うところもあります。以下はその例です。波線＋ノードも二重線＋ノードも、どちらも生の2-自然変換です。この記事は最初に書いた時点からほとんど変更していません。そのため、後から追加した「生の2-関手と生の2-自然変換」との連携があまりとれてません。あしからず。射と変換手通常の圏〈1-圏〉は対象と射を持ちます。圏のあいだに関手があり、関手…

… 生の2-自然変換 ストライプ図とストリング図 生の◯◯◯ → ？ 2-圏$`\cat{K}, \cat{L}`$ などは（必ずしも厳密とは限らない）小さい2-圏だとします*1。次の約束をします。 2-圏 $`\cat{K}`$ の対象〈0-射〉の集合を $`|\cat{K}|`$ と書く。$`|\cat{K}|`$ の要素〈対象 | 0-射〉は、ラテン文字小文字 $`a, b`$ などで表す。 2-圏 $`\cat{K}`$ の射〈1-射〉の集合を $`|\cat{K}|_…

…グ図、関手ボックス、ストライプ図などに関しては、このブログ内に山のように関連記事があります。 「ストリング図」の検索結果 「ボックス」の検索結果 「ストライプ」の検索結果 入門的記事をひとつだけ挙げれば： ストリング図の基本概念と描き方 さて、関手ボックスは、関手 $`F:\cat{C} \to \cat{D}`$ に対してボックス〈箱〉を描きます。 ボックスの内部には圏 $`\cat{C}`$ のストリング図を描く。 ボックスの外部（キャンバスの地）は圏 $`\cat{D}…

…ctor box〉、ストライプ図〈stripe diagram〉があります。$`F(f:A \to B)\In \cat{D}`$ を次のように描きます。関手の値を、左端は単にワイヤー＆ノードとして描いています。左から二番目は関手ボックスによる絵です。三番目は射の部分を膨らましたストライプ図、右端はストレートなストライプ図です。$`\cat{C}`$ の対象・射を普通のストリング図として描いて、関手 $`F`$ を表すボックスまたはストライプ〈シース | sheath〉で包む…

…手の記述と計算には、ストライプ図が便利に使えます。これについても「モノイド圏と加群圏に関するフォークロアとマックレーン五角形・三角形」に書いてあります。ストライプ図とストリング図を組み合わせる話は次の過去記事などを見てください。 新しい絵算手法：ストリング＋ストライプ図 ストリング図とストライプ図 定数関手記述を簡潔にするために、 $`\quad \cat{D} := \cat{C}\times \cat{C}^\op`$ と置きます。$`\cat{D}`$ は、$`\cat…

…れたものになります。ストライプ図をゴニョゴニョ描いてみた感じでは、追加の構造・条件は次のようにすると良さげです。 ラックス・モノイド関手のラックス乗法／ラックス単位は可逆である。つまり、タイト・モノイド関手になる。[追記]この条件は強すぎるようです。たぶん、続きを書きます。→続き[/追記] タイト・モノイド関手の反ラックス構造（コモノイド様構造）は、デカルト・モノイド圏のDC構造と協調する。 二番目の条件は、大雑把な等式で書くと次のようです。[追記]以下の一番目は間違いです。…

…いかも知れないので、ストライプ図を描くことをオススメします*3。 が同型射ならタイト左強度〈tight left strength〉、同型射とは限らないときはラックス左強度〈lax left strength〉と呼びます。反ラックス左強度〈oplax left strength〉は次のプロファイルを持ちます。“左”を“右”に置き換えることにより次の概念が定義できます。 右テンソル強度〈right tensor strength〉 右強度〈right strength〉 タイト…

…描画に関手ボックス／ストライプ図を使っています。しかし、コエンド計算では関手ボックス／ストライプ図を使っていません。米田埋め込みは関手ボックスで描くのがわかりやすいのに…。コエンドの具体的構成で使われるコエンド同値関係も、関手ボックスを使って次のように描けます。説明： この図は集合圏におけるストリング図で、描画方向は「↓→」。つまり、射の順行方向は上から下。 ピンクはプロ関手 の関手ボックス。 左辺関手ボックス内の左側は逆行する 、あるいは 。 左辺関手ボックス内の右側は順行…

…イド余モナドの計算（ストライプ図絵算）をゴニョゴニョしているときに気付いた等式があります。とりあえずその等式を、余モナドのパンツマジック等式〈pants magic equation〉と呼んでおきます。ストライプ図を眺めると、下着〈パンツ〉の上にズボン〈パンツ〉を履いていたのに下着だけになってしまうマジックに見えるからです。ある観点から見ると、パンツマジック等式は自明な等式でした -- 「なーんだ」という気分になりました。なので、この記事はボツにしようかとも思ったのですが、ゴ…

…うに、ストリング図／ストライプ図のよる計算を、2次元的テキスト表示で（かなり苦しいのだけど）なんとか伝えようと思います。計算はモノイド圏 のなかで行います。等式の左辺 は、 のなかで次のように表示できます。これは、 の定義を使って展開しています。縦方向の繋ぎ目部分を短縮します。書き方を短くしているだけ。ひとつの行列にまとめます。ここまでは、テキスト表示の書き方・レイアウトを変えているだけで何も行ってません。 の自然性から、 を“上に移動”します。 が“下に移動”したとも言えま…

…は と“同じ形状”のストライプ図で定義されます。次の絵をみてください。左上が を表す二分木です。右側が“同じ形状”のストライプ図です。「同じ形状」とは何かを具体的に言えば： の （または の ）の位置に余乗法 が置かれたツリーが、 のストライプ図の形状となる。 上の絵の下側のツリーは、形状だけを取り出したツリーです。二分木としての の形状、そして のストライプ図の形状と同じです。念のため、 を行列形式記法で書くと次のようになります。以上は、絵図を利用した直感的な説明でしたが、…

…す。これは、なんとかストライプ図をイメージできるかな。 反ラックス・モノイド関手の余乗法の余結合律 余結合律（に類似の法則）は次のようです。もとのストライプ図を知っていれば思い出すキッカケにはなるでしょう。 反ラックス・モノイド関手の余乗法と対称との強調 が特定の対象 を左から掛ける関手のときは、この等式は次のストリング図で描けます（「準マルコフ圏の掛け算関手」参照）。比較的素直なストライプ図なら、ギリ再現できる感じですね。 *1:homotopy.io（globularの後…

…書くと以下の形です。ストライプ図のあいだの等式で描くと分かりやすいでしょう。余結合律：左余単位律：右余単位律： の場合は次のようになります。余結合律：左余単位律：右余単位律：先に具体的に定義した に関する を使って、これらの等式を示すことになります。テキストの式や可換図式ではさすがに辛いかも知れません。ストリング図のあいだの等式として確認すると楽でしょう。当然ながら、 に関する性質は使うことになります。反ラックス対称モノイド関手としての掛け算関手反ラックス・モノイド関手が対称…

…の話はストリング図／ストライプ図で記述し考えるのが便利です。つうか、ストリング図／ストライプ図なしで理解するのはすごく辛いと思います。だがしかし、僕がストリング図／ストライプ図を描く気力がないので、MathJax で容易に書けるテキスト数式で記述します。毎度愚痴っていることですが、ストリング図／ストライプ図を手軽に描けるツール／環境がないのがホーントに困ってる。ハァー（ため息）。ストリング図／ストライプ図を含む絵図の描き方については、以下の過去記事を参照してください。これらの…

…います。この描画法はストライプ図*9です。最初に挙げたロマン〈Mario Roman〉の図（下に再掲）は、すぐ上の図と同じです。ワイヤーやエリア（平面内の領域）のラベルは省略されています。圏 C 内で描画しているわけではなくて、圏の圏 CAT 内で描画しています。絵図を見るときは、「どこで、何を、どのように描いているのか？」を最初に確認しないとワケワカランことになります。注意しましょう。 *1:実は絵しか見てません。 *2:絵の読み書きに関する一般的注意は「絵算をはじめた人へ…

…// マッカーディのストライプ図 ストリング図とストライプ図 関手に限らず、圏論的コンストラクタ／オペレーターをボックスで表すことができます。モナドを拡張スタイルで定義するときの拡張オペレーター〈クライスリ・オペレーター〉をボックスで描いた例は次の記事にあります。 絵算で見る、拡張スタイルのモナドとモノイド・スタイルのモナド そもそも、コンストラクタやオペレーター（コンビネータとも呼ぶ）が何であるかは次の記事を見てください。 圏論的コンストラクタと圏論的オペレータ： 関手性・…

…触れてるだけだな）。ストライプ図は関手ボックスの変種です -- 「モノイド関手／ラックス・モノイド関手とその実例 // マッカーディのストライプ図」に説明があります。射のプロファイルとin記法もよく使うので、必要があれば次も参照してください。 前層の圏における記法と計算 // プロファイリングとin記法 モノイド・スタイルのモナドの定義テキスト記法は図式順記法を使うので、必要があれば演算子記号の一覧表を確認してください。 関手と自然変換の計算に出てくる演算子記号とか // 今…

…// ストリング図とストライプ図 テキストへの翻訳コミュニケーションの都合で、絵図をテキストに翻訳する必要が生じます。一例をやってみましょう。上の図で、目ぼしいノードはαとηなので、これらのノードを横に切る補助線（赤い点線）を引いて、ラベルの2次元的配置を取り出します。この2次元配置〈行列〉に演算子記号を入れて1次元に押し込めて、左右の順番も入れ替えましょう。[補足][追記] 最後の結果 がコンパクトなのは、絵が持っていた情報の相当部分を落としてしまっているからです。試しに、…

…tは、ストリング図やストライプ図のような絵図と、従来のテキスト記法を橋渡しするフォーマットになるだろうと期待できます。以下は、CatPictの試案〈プロトタイプ〉で、幾つかの等式や定義を書いてみた例です。なんか、上記の2008年当時の記法とあんまり変わってませんが、同じ人（檜山）が考えてるもんで、まーしょうがない。 *1:新しいかどうかは疑問。以前から使っていた記法を整理拡充する感じです。 *2:使える回転機能がないので僕は、例えば文字'Y'の+90度回転を'>-'、-90度…

…// ストリング図とストライプ図」の続きです。内容： 自然変換ストリング図と関手ストリング図 ストリング図書き換え ストライプ図 自然変換ストリング図と関手ストリング図単に「ストリング図」と言ってきましたが、二種類のストリング図が登場してましたね。「自然変換、関手、圏」を表すストリング図を自然変換ストリング図〈natural transformation string diagram〉、「関手、圏」を表すストリング図を関手ストリング図〈functor string diagr…

…して、ストリング図とストライプ図の関係を説明します。内容： ラックス・モノイド関手 ストリング図書き換え ラックス・モノイド関手の素材 ラックス・モノイド関手の結合律と単位律 ストリング図とストライプ図 関連する記事： 図式思考の例として、コモノイドについて考えてみる ラックス・モノイド関手モノイド圏、各種モノイド関手、モノイド自然変換については、以下の記事を参照してください。だいたいの雰囲気を知っていればいいです、完全な理解は要求してません。 モノイド関手／ラックス・モノイ…

…容でもストリング図／ストライプ図で描くとずっと分かりやすく感じます。ストライプ図については、 モノイド関手／ラックス・モノイド関手とその実例 // マッカーディのストライプ図 ストライプ図を使っている記事は： モノイド圏と加群圏に関するフォークロアとマックレーン五角形・三角形 モノイド自然変換とモノイド同値関手 リストモナドとテンソル空間モナドのあいだの準同型射 インデックス付き圏を拡張してファイバー付き圏へ ストリング図／ストライプ図を使うと、次の類似性が目視で確認できると…

…える ストリング図とストライプ図 タイト2-関手 ファイバー付き圏の構成 ファイバー付き圏とインデックス付き圏ファイバー付き圏の定義の方法が二通りあります。 射影関手 P:E→B を使う方法。 Bを添字圏〈indexing category〉とする圏の添字族〈indexed family of categories〉を使う方法 二番目の添字族〈インデックス族〉を使う方法として、インデックス付き圏があります。しかし、インデックス付き圏の定義が強すぎる（きつすぎる）ので、射影関手…

…がモナド本来の生態が観察できる気がします。関連する記事： ラックス・モノイド関手について、もうちょっと モナド論をヒントに圏論をする（弱2-圏の割と詳しい説明付き） 弱2-圏内のモナドに関する補足：モナドが作る2-圏の多様性 高次圏： 用語法と文脈（主に2次元） 新しい絵算手法：ストリング＋ストライプ図 *1:[追記]「ラックス2-」という形容詞にそれほど意味がわるわけではない（語呂を揃えるため）ので、「0-変換手」と「1-変換手」のほうが良い呼び名かも知れません。[/追記]

…算手法：ストリング＋ストライプ図 絵算のテキスト表現（結論：疲れる） 絵算のテキスト化を完全にやってみた（超・疲れた） もとの定理（結合律 (mN);m = αN,N,N;(Nm);m）の内容はあんまり気にしなくていいです。同じ定理の記述と証明を、いろんな手法でやってみようというノリです。結合律の絵による証明とテキスト（項と等式）による証明は既に述べたので、可換図式〈commutative diagram〉による証明を挙げましょう。以下の図がソレです。GraphVizで描いた…

…算手法：ストリング＋ストライプ図」を書いた時点で、例題である“結合律”を証明する絵〈pictorial proof〉は描いていました。翌日の「絵算のテキスト表現（結論：疲れる）」において、行列レイアウトを使って絵の一部をテキストに写し取ってみたのですが、疲れて途中でやめてしまいました。4月30日の夜と5月1日の朝を使って、残りの写し取り作業を完成させたので、その結果をお見せしましょう。面倒だったよー。たぶん、こんな事はもうやらないと思います。内容： はじめに 書き方のお約束 …

…は持ってない*1し、ストライプ図をまったくサポートしていません。次のような絵（マースデンとマッカーディ）は、通常の（汎用の）お描きツールで描いていると思われます。 僕は手描きの絵をスキャンしてますが、汚いし、編集して再利用が出来ないのが難点です。テキスト表現では記述や計算が困難なので絵図を使っているわけで、それをテキストにしても嬉しいことはないのですが、編集と交換の容易性を重視するなら、「なにかしらのテキストで」となるでしょう。また、「どうしても絵図には馴染めない」という人と…

…です。ストリング図とストライプ図のハイブリッドなので、ベタにストリング＋ストライプ図〈string+stripe diagram〉と呼んでます。メインはストライプ図なので、ストリング図機能を取り込んだストライプ図とも言えます。内容： “モノイド圏の圏”における3つの方向 3次元見取り図 正面図：ストライプ図 側面図：ストリング図 例題のサワリ おわりに “モノイド圏の圏”における3つの方向2つのモノイド圏とそのあいだの関手を扱うと、射の結合の方向、モノイド積の方向、関手の結合…

…示にはマッカーディのストライプ図を使うのが便利です。ストライプ図については、次の記事を参照してください。 モノイド関手／ラックス・モノイド関手とその実例 モノイド圏と加群圏に関するフォークロアとマックレーン五角形・三角形 モノイド自然変換とモノイド同値関手 次は多色のストライプ図の例です（"Frobenius Morphisms of Bicategories"より）。ストライプ図は、モノイド圏を含む2次元の圏とそのあいだの関手の計算に大変便利な道具です。スパンの弱2-圏 ＝…