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

ご連絡は上記 X アカウントに DM にてお願いします。

［参照用 記事］

有限集合達の圏とその骨格は圏同値

雑記／備忘

有限集合についてキチンと理解していることが必要となる場面は多いです。「キチンと理解している」とは、個々の有限集合だけではなくて、すべての有限集合達が形成する圏 $`\mathbf{FinSet}`$ の構造を理解していることです。

この記事では、有限集合達の圏 $`\mathbf{FinSet}`$ の骨格（と呼ばれる小さい圏）を定義して、骨格と有限集合達の圏が圏同値であることを示します。

理解を阻害する要因として、「記号の乱用と省略が諸悪の根源」と僕は思っているので、できるだけ記号の乱用（オーバーロード含む）と省略をしない記述をします。これは、名前の使用法の約束を明示化するということです。$`
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\mbf}[1]{ \mathbf{#1} }
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\u}[1]{ \underline{#1} }
\newcommand{\id}{ \mathrm{id}}
\newcommand{\In}{ \text{ in }}
\newcommand{\hyp}{\text{－} }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\o}[1]{ \overline{#1} }
\newcommand{\EQV}{\mathrel{\overset{\sim}{\equiv}} }
\newcommand{\Dashv}{ \style{display: inline-block; transform: rotate(180deg)}{\vDash} }
\newcommand{\ID}{\mathrm{ID}}
\newcommand{\Id}{\mathrm{Id}}
\newcommand{\T}[1]{\text{#1} }
\require{color}
\newcommand{\NX}[1]{ \textcolor{orange}{ {#1}} } % New Expression
\newcommand{\KX}[1]{ \textcolor{blue}{#1} } % Known EXpression
`$

内容：

有限集合達の圏

有限集合達の圏を $`\mbf{FinSet}`$ とします。$`\mbf{FinSet}`$ は集合圏〈集合達の圏〉 $`\mbf{Set}`$ の充満部分圏〈full subcategory〉なので、次が成立します。

$`\quad \mbf{FinSet}(X, Y) = \mbf{Set}(X, Y) \;\In \mbf{Set}`$

$`X\in |\mbf{FinSet}|`$ に対して、$`\mrm{card}(X)`$ は、有限集合 $`X`$ の基数〈cardinality〉だとします。ここでは、基数の値は自然数だとするので、$`\mrm{card}`$ は次のような関数〈写像〉です。

$`\quad \mrm{card} : |\mbf{FinSet}| \to \mbf{N} \In \mbf{SET}`$

自然数 $`n\in \mbf{N}`$ に対して、$`\bar{n}`$ は $`\{1, 2, \cdots, n\}`$ のことです。特に：

  • $`\bar{0} = \{\}`$
  • $`\bar{1} = \{1\}`$
  • $`\bar{2} = \{1, 2\}`$

$`n\mapsto \bar{n}`$ は次のような関数です。

$`\quad \o{(\hyp)}\: : \mbf{N} \to |\mbf{FinSet}| \In \mbf{SET}`$

僕は、自然数の上に線を引く記法をよく使ってますが、上線〈オーバーライン〉は他の用途でも使う記法なので注意してください。

  1. 「デカルト閉・型システム」では、外延化写像〈extensionalize map〉として上線を使っている。
  2. 「反対圏と反変関手はややこしい」では、“ほんとの反変関手”を含む圏達の2-圏を $`\o{\mbf{CAT}}`$ と書いている。
  3. 「複余有向コンテナ〈オペラッドコンテナ〉によるオペラッドの定義」では、複圏の複射達の集合に上線を使っている。アーマン／チャップマン／ウウスタル〈Danel Ahman, James Chapman, Tarmo Uustalu〉の書き方を踏襲。
  4. 「状態遷移系としての前層・余前層・プロ関手」では、反対圏の対象・射に上線を使っている。ボルトルッシ／モンベリ〈Noelia Bortolussi, Martín Mombelli〉の書き方を踏襲。

$`\o{(\hyp)}\:`$ に名前が必要なときは '$`\mrm{range}`$' という名前*1を使えばいいでしょう（使う機会はあまりないですけど）。

$`\quad \mrm{range} : \mbf{N} \to |\mbf{FinSet}| \In \mbf{SET}`$

有限集合達の圏の標準骨格

有限集合達の圏の標準骨格〈{standard | canonical} skeleton〉（と呼ばれる圏） $`\mbf{F}`$ を定義します。$`\mbf{F}`$ は $`\mathbb{F}`$ と書かれることが多いですが、黒板文字はサイズが大きい圏や二重圏に取っておきたいので、ボールド体とします。

  • 対象達の集合： $`|\mbf{F}| := \mbf{N}`$
  • ホムセット： $`\mbf{F}(n, m) := \mbf{Set}(\bar{n}, \bar{m}) \:\text{ for }n, m\in |\mbf{F}|`$
  • 恒等射： $`\id_n := \id_{\bar{n}}`$

射の結合は関数の結合です。関手 $`J: \mbf{F} \to \mbf{FinSet}`$ は次のように定義します。

  • $`J(n) := \bar{n} \:\text{ for }n \in |\mbf{F}|`$
  • $`J(f) := f \:\text{ for } f \in \mrm{Mor}(\mbf{F})`$

$`J`$ により、$`\mbf{F} \subset \mbf{FinSet}`$ あるいは $`\mbf{F} \subset \mbf{Set}`$ とみなすことがあります。$`\mbf{F} \subset \mbf{FinSet}`$ とみなした場合、部分圏 $`\mbf{F}`$ は次の特徴があります。

  1. $`\mbf{F}`$ は充満部分圏である。
  2. $`X, Y \in |\mbf{F}|`$ に対して、$`(X\cong Y\In \mbf{F}) \Imp X = Y`$ が成立する。
  3. 任意の $`S\in |\mbf{FinSet}|`$ に対して、$`S \cong X \In \mbf{FinSet}`$ となる $`X\in |\mbf{F}|`$ が存在する。

このような性質を持つ部分圏は $`\mbf{FinSet}`$ の骨格的部分圏〈skeletal subcategory〉、あるいは単に骨格〈skeleton〉と呼びます。$`\mbf{FinSet}`$ の骨格はたくさんありますが、$`\mbf{F}`$ は標準骨格〈{canonical | standard} skeleton〉と呼びます。

この記事で示したいことは、$`\mbf{FinSet}`$ と $`\mbf{F}`$ は圏同値であることです。次節で圏同値の定義を述べます。

圏同型、関手の自然同型、圏同値

2つの圏 $`\cat{C}, \cat{D}`$ が同型〈isomorphic〉であるとは； 関手のペア $`F, G`$ があって、以下の等式を満たすことです。'$`*`$' は、関手の結合〈合成 | composition〉の図式順演算子記号、'$`\Id`$' は恒等関手を表します。'$`\land`$' は論理ANDです。

$`\quad F* G = \Id_\cat{C} \;\land\; G*F = \Id_\cat{D}\\
\text{where }\\
\quad F : \cat{C} \to \cat{D} \In \mbf{CAT}\\
\quad G : \cat{D} \to \cat{C} \In \mbf{CAT}
`$

$`\cat{C}, \cat{D}`$ が同型〈圏同型〉であることは、$`\cat{C} \cong \cat{D}`$ と書きます。

2つの関手 $`F, G : \cat{C}\to \cat{D}`$ （上の $`F, G`$ とは無関係）が自然同型〈naturally isomorphic〉だとは、関手圏 $`[F, G]`$ のなかで同型なことです。もっと具体的に言うと、次のような自然変換のペア $`\alpha, \beta`$ が存在することです。'$`;`$' は、自然変換の縦結合〈vertical composition〉の図式順演算子記号、'$`\mrm{ID}`$' は恒等自然変換を表します。

$`\quad \alpha ; \beta = \mrm{ID}_F \;\land\; \beta ; \alpha = \mrm{ID}_G\\
\text{where }\\
\quad \alpha :: F \twoto G :\cat{C}\to \cat{D} \In \mbf{CAT}\\
\quad \beta :: G \twoto F :\cat{C}\to \cat{D} \In \mbf{CAT}
`$

$`F, G`$ が自然同型であることは、$`F \cong_{\mrm{nat}} G`$ と書きます。

2つの圏 $`\cat{C}, \cat{D}`$ が同値〈equivalent〉であるとは； 関手のペア $`F, G`$ があって、以下の自然同型関係が在ることです。

$`\quad F* G \cong_{\mrm{nat}} \mrm{Id}_\cat{C} \;\land\; G*F \cong_{\mrm{nat}} \mrm{Id}_\cat{D}`$

$`\cat{C}, \cat{D}`$ が同値〈圏同値〉であることは、$`\cat{C} \EQV \cat{D}`$ と書きます。

関手ペアの自然同型を与える自然変換を $`\alpha, \beta`$ とすると：

$`\quad \alpha ; \beta = \mrm{ID}_F \;\land\; \beta ; \alpha = \mrm{ID}_G\\
\text{where }\\
\quad \alpha :: F*G \twoto \mrm{Id}_\cat{C} :\cat{C}\to \cat{C} \In \mbf{CAT}\\
\quad \beta :: G*F \twoto \mrm{Id}_\cat{D} : \cat{D}\to \cat{D} \In \mbf{CAT}
`$

2つの圏 $`\cat{C}, \cat{D}`$ が圏同値でも、圏同型とは限りません。圏同型な2つの圏 $`\cat{C}, \cat{D}`$ は必ず圏同値です。したがって、$`\cat{C} \cong \cat{D}`$ であるときに $`\cat{C} \EQV \cat{D}`$ と書いても間違いにはなりません。このことから、圏同型と圏同値を区別しないで $`\cat{C} \cong \cat{D}`$ と書くような記述も一応は正当化されます。

具体例として、$`\mbf{R}`$ 上の有限次元ベクトル空間達の圏 $`\mbf{FdVect}_\mbf{R}`$ と実係数の行列達の圏 $`\mbf{Mat}_\mbf{R}`$ は、圏同値ですが圏同型ではありません。この記事内で述べる $`\mbf{FinSet}`$ と $`\mbf{F}`$ も、圏同値だが圏同型ではない事例を与えます。

随伴類似系としての圏同値

前節の $`\alpha`$ は（$`\beta`$ もだが）可逆自然変換なので、逆を $`\alpha'`$ とすると：

$`\quad \alpha' :: \mrm{Id}_{\cat{C}} \twoto F*G : \cat{C}\to \cat{C} \In \mbf{CAT}\\
\quad \beta :: G*F \twoto \mrm{Id}_{\cat{D}} : \cat{D}\to \cat{D} \In \mbf{CAT}
`$

上の形を見ると、$`\alpha', \beta`$ が随伴関手ペア $`F, G`$ の単位・余単位に似ていることがわかります。ただし、似ているだけで随伴系にはなりません。圏同値が随伴系にもなっているときは随伴同値〈adjoint equivalence〉と呼びます。随伴同値は単なる同値より強い〈きつい〉条件です。

圏同値はけっこう複雑な概念なので、随伴系に類似した系〈system〉として扱いましょう。系・構造なら指標で書くのがいいでしょう（以下に指標）。「構造記述のための指標と名前 1/n 基本」で約束したように、初出の名前はオレンジ色です。

$`\T{2-signature }\NX{\text{Equivalence}}\: \{ \\
\quad \T{sort }\NX{\cat{C}}, \NX{\cat{D}}\\
\quad \T{operation }\NX{F} : \cat{C} \to \cat{D}\\
\quad \T{operation }\NX{G} : \cat{D} \to \cat{D}\\
\quad \T{2-operation }\NX{\eta} :: \Id_\cat{C} \twoto F*G : \cat{C}\to \cat{C}\\
\quad \T{2-operation }\NX{\eta'} :: F*G \twoto \Id_\cat{C} : \cat{C}\to \cat{C}\\
\quad \T{2-operation }\NX{\varepsilon} :: G*F \twoto \Id_\cat{D} : \cat{D}\to \cat{D}\\
\quad \T{2-operation }\NX{\varepsilon'} :: \Id_\cat{D} \twoto G*F : \cat{D}\to \cat{D}\\
\quad \T{equation } \NX{\text{unit-inv-1}}::: \eta ; \eta' \Rrightarrow \ID_{\Id_\cat{C}}\\
\qquad :: \Id_\cat{C} \twoto \Id_\cat{C} : \cat{C} \to \cat{C}\\
\quad \T{equation } \NX{\text{unit-inv-2}}::: \eta' ; \eta \Rrightarrow \ID_{F*G}\\
\qquad :: F* G \twoto F*G : \cat{C} \to \cat{C}\\
\quad \T{equation } \NX{\text{counit-inv-1}}::: \varepsilon' ; \varepsilon \Rrightarrow \ID_{\Id_\cat{D}}\\
\qquad :: \Id_\cat{D} \twoto \Id_\cat{D} : \cat{D} \to \cat{D}\\
\quad \T{equation } \NX{\text{counit-inv-2}}::: \varepsilon ; \varepsilon' \Rrightarrow \ID_{G*F}\\
\qquad :: G* F \twoto G*F : \cat{D} \to \cat{D}\\
\}
`$

2-signature と書いているのは、2次元までの射を使うからです。sort, operation は指標で使う伝統的なキーワードですが、ここでは圏と関手を意味します。2-operation は自然変換です。equation は等式ですが、3-射と解釈しています。（なお、随伴系の2-指標〈2-signature〉をテキストとペースティング図とストリング図で書いた／描いた事例が「随伴系の2-指標」にあります。）

このようにちゃんと書き出してみれば、圏同値という概念がそこそこ複雑なことが分かるでしょう。なんとなく「2つの圏のあいだの関係」という程度の理解では役に立ちません。例えば、2つの圏が圏同値なことを示すには、$`F, G, \eta, \eta', \varepsilon,\varepsilon'`$ に相当する関手／自然変換を具体的に構成して、等式達 $`\text{unit-inv-1},\text{unit-inv-2},\text{counit-inv-1},\text{counit-inv-2}`$ をすべて証明する必要があります。

圏同値という系・構造の構成素に役割り名を与えましょう。随伴系における役割り名を借用します。随伴系の構成素役割り名については「随伴系はなぜ難しいか」に記述があります。

記号 構成素役割り名 種類
$`\cat{C}`$ (特に無い) 圏
$`\cat{D}`$ (特に無い) 圏
$`F`$ 左関手 関手
$`G`$ 右関手 関手
$`\eta`$ 単位 自然変換
$`\eta'`$ 単位の逆 自然変換
$`\varepsilon`$ 余単位 自然変換
$`\varepsilon'`$ 余単位の逆 自然変換

左関手と右関手のペアは随伴ペアならぬ同値ペアです。関手のペアが同値ペアであるためには、可逆な単位と余単位が要求されます。

法則〈自然変換のあいだの等式〉は次のように呼びましょう。

  1. $`\text{unit-inv-1}`$ ： 単位の可逆性その1
  2. $`\text{unit-inv-2}`$ ： 単位の可逆性その2
  3. $`\text{counit-inv-1}`$ ： 余単位の可逆性その1
  4. $`\text{counit-inv-2}`$ ： 余単位の可逆性その2

具体的な圏同値のセットアップ

具体的な圏同値とは、$`\mbf{F}`$ と $`\mbf{FinSet}`$ のあいだの圏同値です。前節で述べたように、圏同値は系・構造であり、12個の構成素〈constituent〉達から構成されます。具体的な圏同値を提示するとは、それら12個の構成素をすべて具体化することです。

法則〈等式〉以外の8個の構成素は次のように具体化します。'$`:=`$' の左側が一般的な構成素役割り名で、右側はこの個別特定の具体的事例に対して使う記号（固有名）です。一部、一般的な役割り名を流用しています。例えば、$`\eta`$ は、単位という役割りを表す一般的記号ですが、ここから先の具体的な圏同値を語る文脈では、個別特定の具体的な自然変換を表す固有名として使うことになります。

  1. $`\cat{C} := \mbf{F}`$
  2. $`\cat{D} := \mbf{FinSet}`$
  3. $`F := J`$ （左関手）
  4. $`G := K`$ （右関手）
  5. $`\eta := \eta`$ （単位）
  6. $`\eta' := \eta'`$ （単位の逆）
  7. $`\varepsilon := \varepsilon`$ （余単位）
  8. $`\varepsilon := \varepsilon'`$ （余単位の逆）

一般的記述で使った名前を、具体例の文脈で具体物の固有名に流用することはよく行われますが、文脈と名前使用法の切り替えについていけないと混乱します。

次節で具体的な構成素達を定義していきます。

具体的な圏同値の構成素達の定義

関手 $`J: \mbf{F} \to \mbf{FinSet}`$ は次のようです。

$`\text{For }n \in |\mbf{F}|\\
\quad J(n) := \bar{n}\\
\text{For }f: n\to m \In \mbf{F}\\
\quad J(f) := f
`$

関手 $`K`$ を作るために、以下のような同型射の族 $`\iota`$ （ギリシャ文字小文字イオタ）が必要です。

$`\text{For }X \in |\mbf{FinSet}|\\
\quad \iota_X : X \to \o{\mrm{card}(X)} \text{ isomorphism }\In \mbf{FinSet}
`$

$`\mrm{card}(X) = n`$ と置くと、$`\iota_X`$ は、有限集合 $`X`$ から $`\bar{n}`$ への同型写像〈isomorphism〉です。これは、$`X`$ の要素を数え上げていることになります。あるいは $`X`$ の要素に番号を付けていることです。$`\bar{n}`$ には全順序 $`1\lt 2\lt \cdots \lt n`$ があるので、要素達の順番を決めているともいえます。$`\iota_X`$ は、$`X`$ の番号付け〈numbering〉または順序付け〈ordering〉と呼びます。

有限集合 $`X`$ の番号付けはたくさんあるかも知れませんが、どれかひとつを選んで、それを $`\iota_X`$ としています*2。すべての有限集合達に対して、その番号付け〈順序付け〉を固定したものが $`\iota`$ です。

$`\iota`$ から決まる関手 $`K_\iota: \mbf{FinSet} \to \mbf{F}`$ は次のようです。

$`\text{For }X \in |\mbf{FinSet}|\\
\quad K_\iota(X) := \mrm{card}(X)\\
\text{For }f: X\to Y \In \mbf{FinSet}\\
\quad K_\iota(f) := {\iota_X}^{-1}; f ; \iota_Y
`$

$`K_\iota(f)`$ は、以下の図式が可換になるように決めています。

$`\quad \xymatrix{
X \ar[r]^f \ar[d]_{\iota_X}
&Y \ar[d]_{\iota_Y}
\\
\o{\mrm{card}(X)} \ar[r]_{K_\iota(f)}
&\o{\mrm{card}(Y)}
}\\
\quad \text{commutative }\In \mbf{FinSet}
`$

$`K_\iota`$ を単に $`K`$ とも略記します。ただし、$`K`$ を作るには $`\iota`$ が必要であり、$`K`$ は $`\iota`$ に依存して決まることは心に留めておいてください。

自然変換 $`\eta`$ は次のプロファイル（仕様）を持ちます。

$`\quad \eta :: \Id_\mbf{F} \twoto J*K : \mbf{F} \to \mbf{F}\In \mbf{CAT}`$

$`\eta`$ の成分は次のようになります。

$`\text{For }n \in |\mbf{F}|\\
\quad \eta_n : \Id_\mbf{F}(n) \to (J*K)(n) \In \mbf{F}
`$

成分は次のように簡略化されます。

$`\quad \eta_n : n \to n \In \mbf{F}
`$

成分の定義は：

$`\quad \eta_n := \id_n\; : n \to n \In \mbf{F}\\
\text{i.e.}\\
\quad \eta_n := \id_{\bar{n}} \; : \bar{n} \to \bar{n} \In \mbf{FinSet}
`$

自然変換 $`\eta'`$ は $`\eta`$ の逆ですが、恒等射の逆は恒等射なので：

$`\quad {\eta'}_n := \id_n\; : n \to n \In \mbf{F}`$

続いて自然変換 $`\varepsilon`$ ですが、これは次のプロファイルを持ちます。

$`\quad \varepsilon :: K*J \twoto \Id_\mbf{FinSet} : \mbf{FinSet} \to \mbf{FinSet}\In \mbf{CAT}`$

$`\varepsilon`$ の成分は次のようになります。

$`\text{For }X \in |\mbf{FinSet}|\\
\quad \varepsilon_X : (K*J)(X) \to \Id_\mbf{FinSet}(X) \In \mbf{FinSet}
`$

成分は次のように簡略化されます。

$`\quad \varepsilon_X : \o{\mrm{card}(X)} \to X \In \mbf{FinSet}
`$

成分の定義は：

$`\quad \varepsilon_X := {\iota_X}^{-1} \; : \o{\mrm{card}(X)} \to X \In \mbf{FinSet}
`$

$`\iota`$ は $`K_\iota`$ を定義するときに使った $`\iota`$ です。

自然変換 $`\varepsilon'`$ は：

$`\quad {\varepsilon'}_X := \iota_X\; : X \to \o{\mrm{card}(X)} \In \mbf{FinSet}
`$

上記の定義では、自然変換の成分だけを定義してますが、自然性の可換四角形も必要です。が、自然性は簡単に分かります。

圏同値の法則の確認

前節までに準備した $`\eta, \eta', \varepsilon, \varepsilon'`$ に関して次の法則を示す必要があります。

  1. 単位の可逆性その1 ： $`\eta ; \eta' \Rrightarrow \ID_{\Id_\mbf{F}}`$
  2. 単位の可逆性その2 ： $`\eta' ; \eta \Rrightarrow \ID_{J*K}`$
  3. 余単位の可逆性その1 ： $`\varepsilon' ; \varepsilon \Rrightarrow \ID_{\Id_\mbf{FinSet}}`$
  4. 余単位の可逆性その2 ： $`\varepsilon ; \varepsilon' \Rrightarrow \ID_{K*J}`$

見た目はいかついのですが、これらの法則はほとんど自明です。“最初の単位の可逆性その1”を見てみましょう。3-射の形で書いてありますが、'$`\Rrightarrow`$' は等号と同じです。

$`\quad \eta ; \eta' = \ID_{ \Id_{\mbf{F}} }`$

$`n\in |\mbf{F}|`$ における成分を書くと：

$`\quad \eta_n ; {\eta'}_n = \Id_{\mbf{F}}(n)`$

これは、$`\eta`$ の定義から成立します。

他の法則も成分に展開すれば明らかです

以上で、圏同値という系・構造の12個の構成素がすべて揃いました。これはつまり、$`\mbf{F}`$ と $`\mbf{FinSet}`$ が圏同値であることです。

一般論で片付けるなら

実は、関手 $`F:\cat{C}\to\cat{D}`$ が圏同値を与えるかどうかをチェックする方法があります。それは次の定理です。

  • 関手 $`F`$ が充満忠実〈fully faithful〉で本質的に全射的〈essentially surjective〉なら、$`\cat{C}`$ と $`\cat{D}`$ のあいだの圏同値を与える。

ひとつの関手の性質を見るだけで、2つの圏のあいだの圏同値が言えます。

今回話題にした関手 $`J:\mbf{F} \to \mbf{FinSet}`$ は、充満忠実かつ本質的に全射的であることは比較的簡単に分かります。上記の定理により、$`J:\mbf{F} \EQV \mbf{FinSet}`$ が言えます。

まとめと展望

今回の話は、圏同値を具体的に作る事例になっています。前節の一般的定理は圏同値の判定法を与えますが、白紙から圏同値（という構造）を作り上げる経験があったほうがいいかと思います。

2つの圏が圏同値なとき、圏論的議論はどっちでも同じように行えます。圏同値である2つの圏に対して違う結果が出てしまうような議論は“圏論的に邪悪〈evil〉”だと言われたりもします。

この記事で示したように、$`\mbf{F}`$ と $`\mbf{FinSet}`$ は圏同値なので、$`\mbf{FinSet}`$ の代わりに $`\mbf{F}`$ を使っても、たいていのことは大丈夫です。$`\mbf{F}`$ はサイズも小さく、とても扱いやすい圏です。議論が劇的に単純化されます。

$`\mbf{F}`$ は、ローヴェアの代数セオリーの理論〈theory of algebraic theories〉の基礎となる構造です。ヴォエヴォドスキーは、$`J:\mbf{F}\to\mbf{FinSet}`$ 上の相対モナドとしてローヴェア・セオリーを再定義しています（「リントンの定理と相対モナド」参照）。$`\mbf{F}`$ や $`J`$ は、単純だけど根源的な構造なのでしょう。

*1:ヴォエヴォドスキーは、https://arxiv.org/pdf/1601.02158 などで $`\bar{n}`$ を the standard set with n elements と呼び、$`\mrm{stn}(n)`$ と書いています。

*2:選択公理を仮定しています。