Smooth morphisms are stable under retracts

If a morphism of schemes f : X ⟶ S is a retract of a smooth morphism g : Y ⟶ T in the arrow category, then f is smooth (AlgebraicGeometry.Smooth.of_retract, packaged as the instance MorphismProperty.IsStableUnderRetracts @Smooth).

The main case is a retract over a fixed base: morphisms i : X ⟶ Y and r : Y ⟶ X with i ≫ r = 𝟙 X and r ≫ f = g. Then f = i ≫ g is locally of finite presentation by cancellation, and at each point x the stalk of X at r (i x) = x is a retract of the stalk of Y at i x as an algebra over the stalk of S, so it is formally smooth over it. The general case reduces to this one after base change of g to S.

A typical use: a scheme over S which admits a section into a smooth S-scheme, retracted by a morphism over S, is smooth over S. This is how a fine moduli scheme is shown to be smooth when it is a retract of a finite étale cover of a smooth parameter space.

Main results

• AlgebraicGeometry.Smooth.of_retract_of_comp_eq: a retract of a smooth morphism over the same base is smooth.
• AlgebraicGeometry.Smooth.of_retract: a retract of a smooth morphism in the arrow category is smooth.

theorem AlgebraicGeometry.Smooth.of_retract_of_comp_eq {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) (i : X ⟶ Y) (r : Y ⟶ X) (hir : CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id X) (hrf : CategoryTheory.CategoryStruct.comp r f = g) [Smooth g] : Smooth f

A retract of a smooth morphism over the same base is smooth. Let g : Y ⟶ S be smooth and let i : X ⟶ Y and r : Y ⟶ X satisfy i ≫ r = 𝟙 X. Then r ≫ f = g forces f to be smooth.

theorem AlgebraicGeometry.Smooth.of_retract {X S Y T : Scheme} {f : X ⟶ S} {g : Y ⟶ T} (h : CategoryTheory.RetractArrow f g) [Smooth g] : Smooth f

Smooth morphisms are stable under retracts. If f is a retract of a smooth morphism g in the arrow category, then f is smooth.

instance AlgebraicGeometry.instIsStableUnderRetractsSchemeSmooth_tauCeti : CategoryTheory.MorphismProperty.IsStableUnderRetracts @Smooth