I am a little bit confused about two lemmas regarding Grothendieck's algebraization. Assume all algebras are defined over some field. Here is the short version of my question: Does Tag 09ZT ("Lemma 1") plus Tag 0A42 ("Lemma 2") imply that colimit of $Y_i$'s in Lemma 1 exists in the category of schemes under mild assumptions? (this would mean the construction of $Y$ in the proof of Lemma 1 does not depend on $X$ and is the colimit) If so what is the minimal requirement for that to happen.

The longer version:

Let $A$ be complete with respect to $I$. Let $S=\text{Spec}(A)$ and $S_n=\text{Spec}(A/I^n)$ Let $Y_1\rightarrow Y_2 \rightarrow Y_3 \rightarrow \ldots$ be an infinite sequence of morphism of schemes. Assume $Y_i$ has a structure of a scheme over $S_i$. Let $X$ be a scheme which receives morphisms from $Y_i$'s in a compatible manner. Because of the condition on $Y_i$'s we can deduce that $X\times S$ also receives same type of compatible morphisms from $Y_i$'s. This specially induces a diagram of commutative morphisms in the following form:

Assuming $X_i:=X\times S_i$ let's denote the maps from $Y_i$ to $X_i$ by $f_i$. Furthermore all $f_i$ are finite morphism and $Y_1\rightarrow S_1$ is proper then by Tag 09ZT, there is some scheme $Y$ such all the maps from $Y_i$ to $X\times S$ factors through $Y$ and $Y_i=Y\times S_i$.

Now I want to deduce that the scheme $Y$ does not depend on $X$ and is the colimit of the diagram of $Y_i$'s. Now assume the same situation, we are going to replace $X$ with $X'$ with exactly the same role. Assume $X'$ is receiving compatible morphisms from $Y_i$'s. Then we can form a compatible commutative diagram between $Y_i$ and $X'_i:=X'\times S_i$.

Applying Tag 0A42 (for some reason $X$ and $Y$ is switched in this lemma), implies that the map from $Y_i$'s to $X'\times S$ factors uniquely through $Y$. Then we can project $X'\times S$ on the first factor to get the same conclusion for $X'$. This means $Y$ is the colimit of the diagram of $Y_i$'s.

formalscheme; the statement of the Grothendieck existence theorem is that a proper formal scheme with a finite morphism to a scheme is actually representable by a scheme. $\endgroup$