Proposition: Let $A\to B$ be a local homomorphism of noetherian complete local rings. Assume $A$ is regular of dimension $d$, with residue field $k$. Assume $\dim B=d+r$ and $B\otimes_A k$ is formally smooth over $k$ and has dimension $r$. Then $B$ is formally smooth over $A$.
The proof:
(1) It is easy to reduce to $k=\bar k$.
(2) Then $B\otimes_Ak\cong k[[t_1,...,t_r]]$.
(3) We find by lifting $t_i$ to $B$ a surjection $A[[t_1,..,t_r]]\to B$.
(4) This cannot have a nontrival kernel, otherwise $\dim B<d+r$.
I am not clear about the proof:
(1) How does it related to algebraic closed field? How can we come back to the general case from the algebraically closed case? Can anyone help me with the details?
(2) Why does it hold? Does it because formally smooth implies $B\otimes_Ak$ regular and the ring contains the field $1\otimes_Ak$?
I had be confusing with the proposition. Maybe it is elementary. Thanks for explanations and comments!(It is 2.8 in de Jong's "smoothness, semi-stability and alternations")
The ring $B\otimes_A k$ is also a $k$-vector space and to say it is formally smooth of dimension $r$ over $k$ means the following. $B \otimes_A k$ is finite dimensional of dimension $r$, and the structure morphism $k \to B\otimes_A k $ is formally smooth.
And formal smoothness of a ring map $R \to S$ just means the following. Let $A$ be any $R$-algebra and $I$ a square zero ideal. Then formal smoothness just means $\hom_R(S,A) \twoheadrightarrow \hom_R(S,A/I)$ is surjective. Let me now answer the following questions of yours:
This follows from the fact that formal smoothness is stable under base change.
The result you want is the Cohen Structure Theorem.
The rest of your questions are confusing. I suggest you rephrase them.