Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 5 of 5
The statement of HTT Lemma 3.2.2.9 refers to “the map Δn×An→M(Φ)”, but unfortunately, it does not actually define what this map is or what properties we expect it to have (and it is not defined anywhere earlier in the book). Is there some canonical choice of such a map that I’m somehow missing?
Got it, An×Δn is the constant mapping simplex of length n at the simplicial set An. The map is induced by the functoriality of the mapping simplex.
Is there some canonical choice of such a map
Yes. Maybe you want to explicitly write
Δn×An≃∐σ∈AnΔnwhich in turn you should think of as
⋯=∐σ:Δn→AΔn.Then go back to the definition of M(ϕ) on the top of p. 151: a morphism Δn→M(ϕ) is a pair consisting of a morphism f:Δn→Δn and a morphism σ:Δn→Amaxf.
The first has a canonical choice: the identity. The second choice is parameterized by the index set An of the above coproducts.
Wait a sec, I didn’t use the indices as in the book. Just a sec
Urs, it’s even easier than that.
Given a simplicial set A, let cA:[n]→sSet be the constant functor at A.
Claim: M(cA)≅A×Δn.
Giving a simplex of Δj→M(cA) gives a map Δj→Δn and another map Δj→A (since cA is constant). That is the same thing as giving a simplex of the product, by definition, so we’re done.
Then we obtain the required map (the one I originally wanted) by the functoriality of the mapping simplex functor, since we have an obvious natural transformation cAn→Φ defined component-wise as follows:
αi:An→Ai is given by the composite An→An−1→…→Ai. We immediately verify that the transformation is natural (by construction).
Hmm, a more pressing concern:
How can we show that M(Φ)≅M(Φ′)∐An×Δn−1An×Δn?
It’s a pain in the neck because that pushout is defined by a mapping property in, while the pushout has a mapping property in the opposite direction.
Here’s a link to the mathoverflow question.
1 to 5 of 5