Geometric integrality of smooth, geometrically connected morphisms #
After base change to a field, a smooth scheme is locally Noetherian with regular local rings.
Its local rings are therefore domains, and connectedness implies integrality via
TauCeti.AlgebraicGeometry.isIntegral_of_connected_of_isRegularLocalRing_stalk.
Main declaration #
TauCeti.AlgebraicGeometry.Smooth.geometricallyIntegral: a smooth, geometrically connected morphism is geometrically integral.
@[instance 100]
instance
TauCeti.AlgebraicGeometry.Smooth.geometricallyIntegral
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.Smooth f]
[AlgebraicGeometry.GeometricallyConnected f]
:
A smooth, geometrically connected morphism of schemes is geometrically integral.