科学・技術
ダブルカテゴリにおけるヨネダの補題
Yoneda Lemma in Double Categories (bartoszmilewski.com)
要約
この記事は、圏論におけるヨネダの補題を、より一般的な構造であるダブルカテゴリの文脈で再定式化する方法を探求しています。通常の圏論では、プレ関手(presheaf)の圏におけるヨネダ埋め込みは、対象のコリミットとしてのプレ関手の表現として理解されます。ダブルカテゴリでは、この概念はプロアロー装備(proarrow equipment)という枠組みを用いて、ホリゾンタルアローとバーティカルアローの概念を用いて表現されます。これにより、プレ関手という言葉を使わずにヨネダの補題を扱うことが可能になります。
全文翻訳
ホーム
Bartosz Milewski's Programming Cafeについて
カテゴリ理論、Haskell、並行性、C++
2026年9月13日
ダブルカテゴリにおけるヨネダの補題
Bartosz Milewski 著 カテゴリ理論、プロファクター装備 | タグ: カテゴリ理論、ダブルカテゴリ、プロアロー装備、プロファクター、ヨネダ構造 | [2] コメント
ダブルカテゴリを扱うことは、ミームで的確に要約できます。「セットについてセットに言及せずに話してください。」私たちはホムセットについては話しません、ホリゾンタルユニットについては話します。密かに、私たちはホリゾンタルアローをプロファクターとして視覚化しており、プロファクター合成の単位はホムファクターです。プレ関手は-値ファクターとして定義されるため、ダブルカテゴリでそれらを記述しようとするとすぐに問題に直面します。そしてプレ関手なしでは、圏論の作業馬であるヨネダの補題については話せません。確かに、多くの標準的な圏論的構成は、プレ関手の代わりにプロファクターを使用して一般化でき、ダブルカテゴリ設定にすぐに一般化できます。これは、(重み付き)極限、Kan拡張、要素の圏(タブレーション)などで実行できます。しかし、時にはプレ関手について言及せずにプレ関手について話す必要があるだけです。まず圏論での構成をスケッチし、次のパートでHaskellでのトイ実装を示します。
概要
ヨネダ構成をダブルカテゴリの言語に翻訳するために、プレ関手の対象(0-セル)とヨネダバーティカルアロー(1-セル)—ヨネダ埋め込み—を定義する必要があります。圏のプレ関手の圏からのガイダンスを得ます。ここで、ヨネダファクターは表現可能ファクターとして定義されます。
この図では、ダブルカテゴリの0-セルは圏を表し、その対象へのアクセスがないため、普遍的構成のみを使用してすべてを定義する必要があります。最も単純なこと、例えばプレ関手の対象への作用が集合になることさえ、まとめて、からへの特定のホリゾンタルアローとして定義する必要があります。また、ヨネダ埋め込みが密であること—「すべてのプレ関手は表現可能なもののコリミットである」というスローガンの一般化—も望みます。これは、ダブルカテゴリに一般化する方法を知っている左Kan拡張の観点から表現できます。最後に、ホムセットのマッピングについて話すことなく、ヨネダ埋め込みがフルで忠実であることを望みます。これらのことのほとんどは2-セルを使用して表現でき、文字列図を使用して視覚化できます。問題は、2-セルは片方向のマッピング、左から右へのマッピングに変換されることです。私たちがしばしば必要とするのは、いくつかの2-セルが可逆であることを要求する同型です。
分類アロー
ファクターをプロファクターに変換するのは簡単です。実際、表現可能プロファクターを定義する2つの標準的な方法があります。プロアロー装備では、それらはコンパニオンと共役に対応します。しかし、プロファクターからファクターを構築することも可能です。大まかな考えは、プロファクターが、カリー化されると、プレ関手圏へのファクターと見なせるということです。(Koudenburgはこのファクターを呼びます)。私はプレ関手圏の表記を使用します。これにより、次のように書くことができます。(以下では、添え字を省略することがあります。)成分で、この同値は可逆な自然変換として書くことができます。
もう1つの注意点があります。これは特別な注意が必要です。は圏の対象です。この対象をに適用することはどういう意味ですか?私たちは、でそれが何を意味するかを知っています。
はファクター圏です。ファクターを対象に適用することについて、私たちは二度考えません。しかし、それが実際に意味することは、カリー化のカウンニット、評価(プロ)ファクターを使用しているということです。
したがって、プロファクターのカリー化は、一般的に次のように書くことができます。
この恒等式の片方向、左から右は、ダブルカテゴリの2-セルとして図示できます。
反対方向は、この四角形がデカルト的である(付録1参照)ことを要求することによって得られます。ペアは、の分類子と呼ばれることがあります。それは、バーティカルアローを使用してホリゾンタルアローを分類することを可能にします。
ヨネダ埋め込み
ここで、次の質問をすることができます。最も単純なホリゾンタルアロー:単位アローの分類アローは何ですか?では、単位アローはホムプロファクターです。その分類アローはファクターです。この分類を定義する2-セルは次のように評価されます。
または、展開すると
ヨネダ埋め込みの定義と比較してください。
この2-セルは、コンパニオンの単位の定義としても認識できます。したがって、プロアロー装備では、評価プロファクターはヨネダファクターのコンパニオンと見なすことができます。
ファクターのコンパニオンの簡潔な表記はです。そのため、しばしば(添え字を省略して)と書きます。
この定義と矢印の曲げにより、カリー化を定義する元の図を再描画できます。
すべてのプレ関手が表現可能なもののコリミットであるという条件を一般化するために、が密であることを望みます。ファクターが密であるとは、それ自身に沿った左Kan拡張(密度コモナードと呼ばれる)が恒等に同型である場合です。
随伴
プロアロー装備では、コンパニオンのカウンニットは2-セルです。
オブジェクト(プレ関手)とで。
これは次のようになります。
これはヨネダの補題の半分にすぎません。一般に、反対側—右から左—は装備では自動的には成り立ちません。装備では、共役はコンパニオンの左随伴です。ヨネダアローの場合、随伴は次のように読みます。
ここで。
随伴は、次の2-セルを使用して図示できます。
と任意のホリゾンタル1-セル。
この随伴の単位は、を単位に置き換え、をに置き換えることによって生成されます。したがって、単位は片方向のマッピングを提供します。
または、展開した表記で
プロアロー装備では、2つのアローをまっすぐにすると、2-セルが得られます。
これは、単位アロー(ホリゾンタル、したがって省略)から単位アローへのマッピングとして解釈されます。では、これはホムセットからホムセットへの自然変換です。プレ関手圏で。
これは、ホムセットに対するヨネダファクターのアクションとして認識できます。実際、これは同型です。
これは、ヨネダ埋め込みが完全に忠実であるという通常の証明です。ただし、これは任意の装備では同型ではありません。したがって、随伴の単位が同型であるという条件を課します。これは、の密性と相まって、ヨネダ構造を持つ装備を特定します。そのような装備は、プレ関手オブジェクトとよく振る舞うヨネダ埋め込みを持ちます。
John Baezに建設的な批判に感謝します。
付録1
カリー化条件は、任意の0-セルに対して、ペアが存在し、任意のホリゾンタル1-セルに対して、バーティカル1-セルと2-セルが存在することを意味します。
一般に、これは十分な情報を与えません。与えられたに対して、候補が多数あり、'sも多数存在する可能性があります。私たちが望むのは、から再構築できることです。つまり、でそうであるように、カリー化が同型であることを望みます。
これは、上記の2-セルがデカルト四角形であることを要求することによって達成できます。デカルト四角形は、3つのプローブとの普遍的条件によって定義されます。
これは多くの処理が必要なように思えるかもしれませんが、コツがあります。では、とを、1つのオブジェクト/1つのアローを持つ終端カテゴリに置き換えることができます。
そのようなカテゴリからのファクターは、ターゲットカテゴリ内のオブジェクトを選択します。ここでは、オブジェクトとを選択する2つのファクターを選択します。
左辺はマッピングです。右辺はとホリゾンタル合成です。最初のものは、を完全に再構築することを可能にします。一般的なダブルカテゴリでは、グローバル要素を選択するための終端0-セルがない場合があるため、次に良いものを使用します。一般化された要素は、トリオによって与えられます。
共有する:
Redditで共有 (新規ウィンドウで開きます) Reddit
もっと
Xで共有 (新規ウィンドウで開きます) X
LinkedInで共有 (新規ウィンドウで開きます) LinkedIn
Facebookで共有 (新規ウィンドウで開きます) Facebook
友人へのリンクをメールで送信 (新規ウィンドウで開きます) Email
これのような:
いいね
読み込み中…
関連
「ダブルカテゴリにおけるヨネダの補題」への2件の返信
naso Says:
2026年9月13日午前11時19分
「すべてのプレ関手は表現可能なものの共同積であるというスローガン」あなたはコリミットを意味しましたか?