Principal bundles on formal disc and lifting problem

Question

I found the following post G-principal bundles on formal disc asking asking about the triviality of principal $G$-bundles on $\operatorname{Spf}(\mathbb{C}[[t]])$ being $G$ a linear algebraic group over $\mathbb{C}$. In the answers section, an user gives a the following answer:

Let $P\rightarrow\operatorname{Spf} \mathbb{C}[[t]]$ be a (Zariski-)locally trivial $G$-torsor for a linear algebraic group $G$ over $\mathbb{C}$. To show that $P$ is trivial, it suffices to exhibit a section $\operatorname{Spf}\mathbb{C}[[t]]\rightarrow P$. Since $\mathbb{C}$ is algebraically closed, there is a rational point $\operatorname{Spec}\mathbb{C}\rightarrow P$. It remains to extend this section over $\operatorname{Spec}\mathbb{C}$ to an infinitesimal neighborhood $\operatorname{Spf}\mathbb{C}[[t]]$. A map $\operatorname{Spf}\mathbb{C}[[t]]\rightarrow P$ is a compatible system of maps $\operatorname{Spec}\mathbb{C}[t]/t^n\rightarrow P$. Starting with $\operatorname{Spec}\mathbb{C}\rightarrow P$, this is the lifting problem posed by formal smoothness, which can be solved since G is smooth.

I don't fully understand the answer. Can you explain me with a little bit more of detail what is the lifting problem posed by formal smoothness and how can we solve it using the assumption that $G$ is smooth?

On the other hand, I would like to know it this remains true in the relative case, I mean, if any principal $G$-bundle on $\operatorname{Spf}(\mathbb{C}[[t]])\times_{\operatorname{Spec}\mathbb{C}} S$ is trivial, being $S$ a $\mathbb{C}$-scheme.

Thank you very much for your time and effort with this noobie.

Answer 1

One place to see some words about such things is the Stacks Project section on formally smooth morphisms. The definitions and lemma I use in this post are from there, for instance.

Definition. A closed immersion of schemes $X\hookrightarrow X'$ is called a first-order thickening if the ideal sheaf cutting out $X$ inside $X'$ has square zero.

Definition. A map of schemes $f:X\to S$ is called formally smooth if for any diagram

$$\require{AMScd} \begin{CD} T @>>> X\\ @VVV @VV{f}V \\ T' @>>> S \end{CD}$$

where $T\to T'$ is a first-order thickening, there exists a unique lifting $T'\to X$ making the diagram commute. (This is the lifting problem that formal smoothness is designed to solve.)

The situation we want to apply this to is when $f$ is the map $P\to \operatorname{Spf} \Bbb C[[t]]$. Taking a $\Bbb C$-point on $P$, we get a map $\operatorname{Spec} \Bbb C\to P$ which gives a map $\operatorname{Spec} \Bbb C\to \operatorname{Spf} \Bbb C[[t]]$ after composition with $f$. But this factors through $\operatorname{Spec} \Bbb C[t]/t^2$ because $\Bbb C[[t]]\to \Bbb C$ factors through $\Bbb C[t]/t^2$, so we get the diagram from the definition of formal smoothness. If we know $f$ is formally smooth, we obtain a map $\operatorname{Spec} \Bbb C[t]/t^2\to P$ making the diagram commute. As $\operatorname{Spec} \Bbb C[t]/t^n \to \operatorname{Spec} \Bbb C[t]/t^{n+1}$ is a first-order thickening for any $n$ and any map $\operatorname{Spec} \Bbb C[t]/t^n\to\operatorname{Spf}\Bbb C[[t]]$ factors through $\operatorname{Spec} \Bbb C[t]/t^{n+1}$, we can keep doing this and get a compatible system of maps $\operatorname{Spec} \Bbb C[t]/t^n \to P$ which assembles to a map $\operatorname{Spf} \Bbb C[[t]]\to P$ by the definition of $\operatorname{Spf}$.

All that's left is to verify that $P\to\operatorname{Spf} \Bbb C[[t]]$ is formally smooth. But it turns out that formally smooth morphisms coincide with smooth morphisms under a mild finiteness hypothesis:

Lemma (Stacks 02H6): Let $f:X\to S$ be a morphism of schemes. The following are equivalent:

1. The morphism $f$ is smooth, and
2. the morphism $f$ is locally of finite presentation and formally smooth.

As $G$ is smooth and locally of finite presentation over $\Bbb C$, we have that $P$ is smooth and locally of finite presentation over $\operatorname{Spf}\Bbb C[[t]]$ and we can run the argument above with no problem.

---

The generalization you ask for with torsors over $\operatorname{Spf} \Bbb C[[t]] \times S$ is more difficult. Notably, there's no reason we should have a section over this base, which is a problem: finding a section $S\to P$ where $P$ is your torsor is the first thing we have to do to run the above argument, and there's no reason we should be able to find that in general.