I do not understand the proof of Variant 4.2.3.16 of Higher Topos Theory by Jacob Lurie, and I need help.
Variant 4.2.3.16 asserts the following:
($\diamond$) Let $K$ be a finite simplicial set. There is a cofinal map $N(A)\to K$, where $A$ is a finite poset.
The proof proceeds as follows:
(1). Consider the following property for a simplicial set $K$:
($\ast$) Every nondegenerate simplex $\Delta^n\to K$ is a monomorphism.
If K satisfies ($\ast$), then $K$ satisfies the conclusion of ($\diamond$).
(2). We show that, for each finite simplicial set $K$, there is a cofinal map $\widetilde{K}\to K$, where $\widetilde{K}$ is finite and satisfies ($\ast$).
I am fine with step (1). But I don't understand the proof of (2).
Let me explain Lurie's proof of (2). He argues that we can prove (2) by induction on the number of nondegenerate simplices of $K$. According to him, this is because if $K$ can be written as $K=K_0\amalg _{\partial\Delta^n} \Delta^n$, where $K_0$ satisfies ($\ast$), then $K$ also satisfies ($\ast$). To prove this, he choose a cofinal map $\widetilde{K_0}\to K_0$, where $\widetilde{K}_0$ is a finite simplicial set satisfying ($\ast$), and claims that the map $$\widetilde{K}=(\widetilde{K}_0\times \Delta^n)\amalg _{\partial \Delta^n} \Delta^n\to K$$
witnesses property ($\ast$).
The problem is, I do not understand what the map $\partial \Delta^n\to \widetilde{K}_0$ used in the definition of $\widetilde{K}$ is. Can someone explain what this map is? (Or does anyone know how to prove (2) or ($\diamond$) in different ways?)
Thanks in advance.
Best Answer
[Rephrasing my comment as an answer]
While I cannot speak for the actual proof, two points are worth noting. First, a similar construction appears in Kerodon (https://kerodon.net/tag/02QA) but there (1) $\widetilde{K} \to K$ is required to be a trivial fibration but (2) it doesn't restrict correctly to when $K$ is finite.
The second point is that Kerodon also includes a stronger proof of this same fact (https://kerodon.net/tag/02MU). The construction is quite different but should suffice as a replacement.