Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Presentation of finite Reedy categories as localizations of finite direct categories

Genki Sato

TL;DR

This work constructs a finite direct category $ ext{Down}(C)$ from any finite Reedy category $C$ and a functor $ ext{Down}(C) o C$ that exhibits $C$ as an $( orall ext{(∞,1)}})$-localization of $ ext{Down}(C)$, strengthening previous results by guaranteeing finiteness. The approach combines Grothendieck constructions, detailed analysis of hom-posets via skew ladders, and a suite of endofunctors on simplicial sets to model $( orall ext{(∞,1)}})$-diagrams; key localization steps are encoded as universal localizations and inner anodyne maps. A central contribution is the constructive, finiteness-preserving 1-localization and the subsequent $( orall ext{(∞,1)}})$-localization proof, together with a counterexample showing limits of the method in generality. The results facilitate embedding the construction into non-infinitary logical syntax and hint at a meta-theory for finitely truncated simplicial types in HoTT, enabling robust finite diagrammatic reasoning in type-theoretic settings.

Abstract

In this paper, we present a construction from a Reedy category $C$ of a direct category $\operatorname{Down}(C)$ and a functor $\operatorname{Down}(C) \to C$, which exhibits $C$ as an $(\infty,1)$-categorical localization of $\operatorname{Down}(C)$. This result refines previous constructions in the literature by ensuring finiteness of the direct category $\operatorname{Down}(C)$ whenever $C$ is finite, which is not guaranteed by existing approaches. The finiteness property is useful when we want to embed the construction into the syntax of a (non-infinitary) logic: the author expects the construction may be used to develop a meta-theory of finitely truncated simplicial types for homotopy type theory.

Presentation of finite Reedy categories as localizations of finite direct categories

TL;DR

This work constructs a finite direct category from any finite Reedy category and a functor that exhibits as an -localization of , strengthening previous results by guaranteeing finiteness. The approach combines Grothendieck constructions, detailed analysis of hom-posets via skew ladders, and a suite of endofunctors on simplicial sets to model -diagrams; key localization steps are encoded as universal localizations and inner anodyne maps. A central contribution is the constructive, finiteness-preserving 1-localization and the subsequent -localization proof, together with a counterexample showing limits of the method in generality. The results facilitate embedding the construction into non-infinitary logical syntax and hint at a meta-theory for finitely truncated simplicial types in HoTT, enabling robust finite diagrammatic reasoning in type-theoretic settings.

Abstract

In this paper, we present a construction from a Reedy category of a direct category and a functor , which exhibits as an -categorical localization of . This result refines previous constructions in the literature by ensuring finiteness of the direct category whenever is finite, which is not guaranteed by existing approaches. The finiteness property is useful when we want to embed the construction into the syntax of a (non-infinitary) logic: the author expects the construction may be used to develop a meta-theory of finitely truncated simplicial types for homotopy type theory.

Paper Structure

This paper contains 21 sections, 76 theorems, 166 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Grossaries
  4. Remarks on foundations
  5. Direct and Reedy categories
  6. The simplex category
  7. Simplicial sets, quasicategories and (∞,1)-categories
  8. Several categories related to a Reedy category
  9. The hom-posets of the categories of skew ladders
  10. Reedy structure, directness and finiteness
  11. Functors between the constructed categories
  12. The proof of 1-localization
  13. Shapes of (∞,1)-diagrams used in the proof of (∞,1)-localization
  14. Some endofunctors on Set_Δ
  15. Some natural transformations between the endofunctors
  16. ...and 6 more sections

Key Result

Theorem 1.1

Let $C$ be a Reedy category. Then there is a concrete construction (to be seen in def:down-cdef:down-fctr-last) of a direct category $\mathop{\mathrm{Down}}\nolimits(C)$ and a functor $\mathop{\mathrm{Down}}\nolimits(C) \to C$ which exhibits $C$ as an $(\infty, 1)$-categorical localization of $\math

Theorems & Definitions (190)

  • Theorem 1.1
  • Theorem 1.2: Preceding result
  • Corollary 1.3
  • Definition 2.1: Category-theoretic glossary
  • Definition 2.2
  • Remark 2.3
  • Definition 2.4: Well-foundedness
  • Definition 2.5
  • Lemma 2.6
  • proof
  • ...and 180 more