Arity–coskeleton定理
## Trigger
[[zmpg4f]] が問う「公理に必要な変数数が coskeletal dimension を決める」という原理を，有限集合上の relational Horn structures について証明した．[[egzqw4]] の Arrow/Kori--Watanabe no-go 統一における低次元 rigidity の基礎定理にあたる．
## Result
**定理（Arity--coskeleton theorem）．** \(\sigma\) を有限 relational signature，\(T\) を universal Horn \(\sigma\)-theory とする．各 relation symbol の arity と，各公理に現れる distinct variables の数がともに高々 \(n\) であると仮定する．有限集合 \(A\) 上の \(T\)-models を割り当てる presheaf
\[
\operatorname{Mod}_T:\mathbf{FinInj}^{\mathrm{op}}\to\mathbf{Set}
\]
を考える．濃度高々 \(n\) の有限集合の full subcategory の包含を
\[
i_n:\mathbf{FinInj}_{\le n}\hookrightarrow\mathbf{FinInj}
\]
とすると，
\[
\operatorname{Mod}_T\cong\operatorname{Ran}_{i_n^{\mathrm{op}}}i_n^*\operatorname{Mod}_T.
\]
従って simplex dimension の規約では \(\operatorname{Mod}_T\) は \((n-1)\)-coskeletal である．
## Proof
有限集合 \(A\) を固定する．右 Kan extension の \(A\)-成分は，すべての \(B\subseteq A\), \(|B|\le n\) 上の \(T\)-structures \(M_B\) で，包含に沿う restriction と両立する族である．
arity \(r\le n\) の relation symbol \(R\) と tuple \(\bar a\in A^r\) に対し，\(\bar a\) の support を含む \(|B|\le n\) を選び，
\[
R^M(\bar a)\iff R^{M_B}(\bar a)
\]
と定める．二つの選択は tuple の support への restriction 上で一致するので well-defined である．
\(T\) の公理と \(A\) 上の valuation を取ると，公理に現れる変数の像は高々 \(n\) 点なので，ある \(|B|\le n\) に入る．\(M_B\) は \(T\)-model だから，公理は \(M\) でも成立する．逆に global model は restriction により compatible family を与え，relations の arity bound により一意に復元される．
## Corollary
\(Y\) が \((n-1)\)-coskeletal なら，任意の presheaf \(X\) に対して
\[
\operatorname{Nat}(X,Y)\cong\operatorname{Nat}(i_n^*X,i_n^*Y).
\]
従って \(Y\) への自然変換は濃度高々 \(n\) の有限集合上のデータだけで決まる．graphs は1-coskeletal，preorders・equivalence relations・partial orders・linear orders は2-coskeletalである．
## Interpretation
\[
\text{公理の essential variable arity}
\Longrightarrow
\text{自然変換の自由度の coskeletal dimension}
\]
という一般原理である．逆向き，最小 essential arity の不変化，既存文献との novelty 比較は未解決である．
## Status
上記の十分条件と証明は成立するが，priority は未監査である．