Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Question about generation of inner anodyne morphisms

Jack McKoen (Jan 22 2025 at 20:17):

I'm trying to formalize a proof that inner anodyne morphisms are generated (in the weakly saturated sense) by certain pushout-products--those of the form $(\Lambda^2_1 \hookrightarrow \Delta^2) \square (\partial \Delta^n \hookrightarrow \Delta^n)$. In particular I'm trying to understand Lemma 78.5 in https://rezk.web.illinois.edu/quasicats.pdf (or the second half of https://kerodon.net/tag/007F).

I'm stuck on explicitly showing that the pushout-products $(\Lambda^2_1 \hookrightarrow \Delta^2) \square (\partial \Delta^n \hookrightarrow \Delta^n)$ are generated by inner horn inclusions $\Lambda^n_i \hookrightarrow \Delta^n$. In Rezk's proof (screenshot attached), we take the pushout and attach simplices in a certain order until we present the pushout-product as a composition of inclusions, with each inclusion fitting into a pushout diagram with an inner horn inclusion. Rezk says that this process reduces to a list of elementary observations (I understand why the observations are true).

My problem is that I don't know how to explicitly construct the pushout diagrams from this information. For example, for the first inclusion where we attach $\sigma_{00}$ to the pushout $K = ( \Lambda^2_1 \times \Delta^n) \coprod (\Delta^2 \times \partial \Delta^n)$, we want to have a pushout diagram with $\Lambda^{n + 1}_{1} \hookrightarrow \sigma_{00}$ on the left and $K \hookrightarrow K \cup \sigma_{00}$ on the right. I'm not sure how the list of observations helps to construct the horizontal maps $\Lambda^{n + 1}_{1} \rightarrow K$ and $\sigma_{00} \rightarrow K \cup \sigma_{00}$.

I'd appreciate some help to understand this!

image.png