Help with formalisation of a reasoning about simplicial sets

61 Views Asked by At

We briefly mention during lectures that the homotopy relation between two maps of simplicial sets is not necessarily symmetric. So I thought for a counterexample but I don't know how to formalise it because I started only yesterday studying them.

After digging in the literature, I found that good candidates for my non-reflexive homotopy should be the maps $$ \Delta[0] \to \Delta[1]$$ defined as $i_0 \colon x\mapsto \text{const.} 0$ and $i_1 \colon x\mapsto \text{const.} 1$. Now an homotopy between the two I thought it is the map $$\Delta[0] \times \Delta[1] \to \Delta[1]$$ defined as the projection to the second coordinate. In fact if I compute the n-th level of the composition with the inclusions I get $$(\pi_2)_n\circ (i_0)_n \colon x_n \mapsto (x_n , \text{const.}0)\mapsto \text{const.}0$$ and the same with the other composition. So $i_0\sim i_1$. But now to prove that $i_1\not\sim i_0$ I think the idea should be that the maps has to be monotone, hence "morally" $H\circ i_0 =i_1$ implies that cannot be true that $H\circ i_1 =i_0$. BUT I'm unable to formalise it properly. I don't know how to use this property of being monotone because maps between simplicial sets are natural transformations.

So can someone explain me in detail what's going on here? Maybe with some example I can grasp the main idea behind this kind of reasonings.