Smooth schemes over regular schemes are regular #
If f : X ⟶ Y is a smooth morphism and Y is a locally Noetherian scheme all of whose local
rings are regular, then every local ring of X is regular. On affine opens U ⊆ f⁻¹ V this is
TauCeti.IsRegularRing.of_smooth, since the ring of sections of Y over an affine open is a
regular ring exactly when the local rings at its points are regular. In particular every local
ring of a scheme smooth over a field is regular.
Main declarations #
TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_of_smooth: a scheme smooth over a locally Noetherian scheme with regular local rings has regular local rings.
theorem
TauCeti.AlgebraicGeometry.isRegularLocalRing_stalk_of_smooth
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.Smooth f]
[AlgebraicGeometry.IsLocallyNoetherian Y]
[∀ (y : ↥Y), IsRegularLocalRing ↑(Y.presheaf.stalk y)]
(x : ↥X)
:
IsRegularLocalRing ↑(X.presheaf.stalk x)
If f : X ⟶ Y is smooth and Y is locally Noetherian with regular local rings, then the
local rings of X are regular.