Walk-through to Morel-Voevodsky A¹-homotopy theory part II (page 48, Lemma 1.1)

Here is the second part of my walk-through to Voevodskys A¹-homotopy theory:
On page 48, the first Lemma is shown. Without proof - so I will try to illuminate things a little bit by giving the proof. This lemma isn't used until section 3, so you can skip it, if you want to. I suggest not to do so, if you are intimidated by the diagram, because it isn't that hard, and it's a nice exercise to get the concepts in your head right.

A detailed explanation

The lemma states, that a monomorphism $f : X \rightarrow Y$ between simplicial sheaves induces maps $sk_{n-1}(f) \rightarrow sk_n(f)$ and $Y_n \times \Delta^n \rightarrow sk_n(f)$ whose fiber coproduct ist the space
$! ((X_n \coprod_{X_n^{deg}} Y_n^{deg}) \times \Delta^n) \coprod_{(X_n \coprod_{X_n^{deg}} Y_n^{deg})} (Y_n \times \partial\Delta^n)$

Preliminaries

What is $\Delta^n$?
First, there is a category $\Delta$, whose objects are just finite integer sequences $\Delta_n := (0,1,...,n)$. One considers the opposed category $\Delta^{op}$ (May writes $\Delta^\ast$ instead), whose morphisms are defined to be the monotonic maps. Then $\Delta := \Delta^{op\ op}$. It is important to understand the nature of these monotonic maps - read at least the first chapter in Mays "Simplicial Objects in Algebraic Topology". You will then see, that a simplicial set ist just a functor $\Delta^{op} \rightarrow Sets$, just as any simplicial object ist a functor from $\Delta^{op}$.
For each object $\Delta_n \in \Delta$, define $\Delta^n := Hom(-,\Delta_n)$, a functor $\Delta^{op} \rightarrow Sets$, thus a simplicial set. Together with the embedding of sets as constant sheafs, this gives us a simplicial sheaf $\Delta^n$, which is what is meant here. Observe that we have a functor $\Delta \rightarrow \Delta^{op}Sh(T)$ by sending a map $\alpha : \Delta_n \rightarrow \Delta_m$ to the morphism $\alpha \circ : \Delta^n \rightarrow \Delta^m$. This functor $\Delta^\bullet$ is a cosimplicial object and turns the category of simplicial sheaves on the site T into a simplicial model category (that is, a model category which is compatibly enriched over simplicial sets, so the Hom-Sets are simplicial sets) with the simplicial function object $! S(X,Y) = Hom_{\Delta^{op}Sh(T)}(X \times \Delta^\bullet, Y)$
We will talk in detail about the simplicial model category structure later.

So what is $sk_n(f)$?
It's defined to be $sk_n(f) := f(X) \cup sk_n(Y)$ where $sk_{-1}(Y)=\emptyset$ and for $n \geq 0$ is $sk_n(Y)$ the $n$-skeleton of $Y$, that is the image of the "obvious" functor $X_n \times \Delta^n \to X$, which may not be so obvious at first sight. Remember that $X$ and $\Delta^n$ are both contravariant functors into the category of simplicial sets, so by Yoneda lemma we have $Trans(\Delta^n, X) = X(\Delta^n) = X_n$. This gives us an interpretation of $X_n \times \Delta^n$ as $Hom(\Delta^n, X) \times \Delta^n$, where the $Hom$ is taken in the category of functors. The "obvious" functor $X_n \times \Delta^n \to X$ is the evaluation map. Observe that (by Yoneda Lemma) for $x \in X_n$ we have $\overline{x}(\Delta_n) = x$, where $\overline{x} \in Trans(\Delta^n, X)$ corresponds to $x$.
At the moment, we don't care about the right adjoint $cosk_n$ (coskeleton) of the skeleton functor.

What is $X_n^{deg}$?
It's defined to be $X_n^{deg} := \cup_{i=0}^{n-1} s_i^{n-1}(X_{n-1})$, the union of all degenerated $n$-simplices that come from $X_{n-1}$ (therefore the name deg). In Mays book "Simplicial Objects", this is written $\bar X_n$. Another equivalent definition would be $X_n^{deg} = (sk_{n-1}(X))_n$.

The statement of the lemma explained

What are these complicated looking objects in the diagram?
Let's look at the following pushout diagram:

Y_n^deg and X_n^deg -> X_n, denoted by Z_n." width="250" height="250" />$$$$
Where I have given the name $Z_n := X_n \coprod_{X_n^{deg}} Y_n$ to make it look less scary. The letter $\iota$ denotes inclusion. There is clearly an inclusion $Y_n^{deg} \rightarrow Y_n$ and the restriction of $f$ gives an arrow $X_n \rightarrow Y_n$ and by pushout property we get a unique arrow $\phi : Z_n \to Y_n$ that makes the diagram commutative:

Y_n" width="450" height="400" />$$$$
The next step is again a pushout diagram:

Y_n x del Delta^n and id x iota : Z_n x del Delta^n --> Z_n x Delta^n, denoted by W_n" width="350" height="250" />$$$$
Where I have given the name $W_n := (Z_n \times \Delta^n) \coprod_{(Z_n \times \partial \Delta^n)} (Y_n \times \partial \Delta^n)$. We have morphisms $id \times \iota : Y_n \times \partial \Delta^n \rightarrow Y_n \times \Delta^n$ and $\phi \times id : Z_n \times \Delta^n \to Y_n \times \Delta^n$ that give us by the pushout property a unique arrow $\psi : W_n \rightarrow Y_n \times \Delta^n$.

Y_n x Delta^n" width="500" height="300" />$$$$

What are the maps in the cocartesian diagram?
The arrow $\psi$ constructed above is the left arrow of the diagram. The right arrow can only be an inclusion $sk_{n-1}(f) \rightarrow sk_n(f)$. The bottom arrow is just the evaluation morphism explained above $ev : Y_n \times \Delta^n \rightarrow sk_n(Y) \subseteq sk_n(f)$.
To construct the top arrow, look at the pushout defining $W_n$ above. The composition of $\phi \times id : Z_n \times \Delta^n \rightarrow (f(X_n) \cup Y_n^{deg}) \times \Delta^n$ with the evaluation morphism $Y_n \times \Delta^n \rightarrow sk_n(Y)$ and the evaluation morphism $Y_n \times \partial \Delta^n \rightarrow sk_{n-1}(Y)$ give us, by pushout property, a unique morphism $\alpha : W_n \rightarrow sk_{n-1}(f)$.

Proof

To check that the diagram is cocartesian means to check that $sk_{n}(f)$ has the pushout property in the diagram

sk_{n-1}(f) and psi : W_n -> Y_n x \Delta^n" width="300" height="200" />$$$$
Take a test object $V$ together with morphisms $s : sk_{n-1}(f) \rightarrow V$ and $t : Y_n \times \Delta^n \rightarrow V$ such that $s\circ \alpha = t \circ \psi$. We have to find a unique morphism $\beta : sk_n(f)\rightarrow V$ that makes the whole diagram commutative.

For a moment, think about the sheaves as sheaves on $T = pt$, so our category is just the category of simplicial sets. We can prove the theorem in this case:

Remember $sk_n(f) = f(X) \cup sk_n(Y)$. For each $\sigma \in sk_{n-1}(Y)$ we can define $\beta(\sigma) := s(\sigma)$. For $\sigma \in sk_n(Y)$ we see that $\sigma$ lies in the image of the (monic) evaluation map from $Y_n \times \Delta^n$, so we can define $\beta(\sigma) := t(ev^{-1}(\sigma))$. Is $\beta$ well-defined? If $\sigma \in sk_n(f)$ has a preimage under the evaluation map, it lies in $sk_n(Y)$; if it has at the same time a preimage of $sk_{n-1}(f)$, it lies in $sk_{n-1}(Y)$, which lies in the image of the map $\alpha$, therefore we seee that $\beta$ is well-defined.

Uniqueness? If we'd have a second map $\beta' : sk_n(f) \to V$, but $\beta \neq \beta'$, then we would have a $\sigma \in sk_n(f)$ such that $\beta(\sigma) \neq \beta'(\sigma)$. Such a $\sigma$ can't have a preimage under the inclusion of $s_{n-1}(f)$ or the evaluation on $Y_n \times \Delta^n$. So $\sigma \notin f(X)$ and $\sigma \notin sk_n(Y)$. Nothing remains, so $\sigma$ doesn't exist.

The general case is done by applying all points $x^\ast : Sh(T) \rightarrow Sets$ respectively all points $x^\ast : \Delta^{op}Sh(T) \rightarrow \Delta^{op}Sets$, which are finite limit- and finite colimit-preserving functors. We can apply the lemma for the point case (which we have proved just before) and deduce from its validity for all points its validity in general (since our site $T$ has enough points - we took only $T$ like that in the beginning).