Principal bundles on formal disc and lifting problem

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.

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.

• Thank you very much for you answer @KReiser, now it is crystal clear. Can you give some references for your claim that if $G$ is smooth and locally of finite presentation then any principal bundle will be it too? Commented Jun 23, 2021 at 9:14
• Combine the following facts: these properties are local, your torsor is locally trivial (i.e. locally isomorphic to a product), the properties are preserved under base extension, and the properties hold for $G\to \operatorname{Spec} \Bbb C$. Commented Jun 23, 2021 at 9:34
• But in this case, $G$ is also of finite type, wouldn't it imply that the principal bundle is also of finite type over $\text{Spf}(\mathbb{C}[[t]])$? Commented Jun 23, 2021 at 10:01
• Sure. This shouldn't be too surprising - locally of finite type and locally of finite presentation are equivalent over locally noetherian bases; the difference between the two terms shows up elsewhere. Commented Jun 23, 2021 at 17:59