Freydグルーイング

トポス理論における標準的な手法。トポス$\mathcal{E}$ を $\mathcal{E}\downarrow \Gamma$（$\mathcal{E}$ の箭圏、または$\mathcal{E}$と$\mathbf{Set}$の貼り合わせ）に埋め込むことで、$\mathcal{E}$の対象に「集合論的な情報」を付加する（[Forssell–Lumsdaine–Swan 2026, 命題1.24]）。

自由トポスにおける役割

• Freydグルーイングの古典的応用: 自由トポス$\mathcal{F}$の終対象 $1$が射影的であることの証明。これが存在性質 (EP) の証明となる（[Forssell–Lumsdaine–Swan 2026, 命題1.24]）。
• 内部Freydグルーイング（[Forssell–Lumsdaine–Swan 2026, 定理4.21]）: 任意のトポス$\mathcal{E}$において、内部自由$r$-トポス${\mathbb{F}}_r$の終対象は (indexed-) 射影的。
  • これを有限階数$r$ごとに適用し→ 標準解釈で外部化→$N$の射影性を得る、というのがMakkai証明の核心戦略。

関連ページ

• free-topos
• projectivity-of-N
• ranked-topos

出典

• Forssell, H., Lumsdaine, P. L., & Swan, A. W. (2026). Makkai’s Lost Proof of Projectivity of N in the Free Topos. arXiv:2604.01139v2 [math.LO]. https://arxiv.org/abs/2604.01139