Smooth morphisms are geometrically reduced #
A smooth morphism of schemes has geometrically reduced fibres. After base change to a field,
smoothness is preserved, and an affine cover of the source has smooth coordinate algebras over
the ring of global functions of the target. That ring is isomorphic to the field, so the
coordinate algebras are reduced by TauCeti.isReduced_of_smooth.
The main result is the instance AlgebraicGeometry.Smooth.geometricallyReduced. Smooth,
geometrically connected morphisms are also shown to be geometrically integral in
TauCeti.AlgebraicGeometry.Morphisms.Smooth.GeometricallyIntegral.
No formalization is vendored. The commutative-algebra input is
TauCeti.isReduced_of_smooth; the passage from affine opens to the whole scheme uses
Mathlib's AlgebraicGeometry.IsReduced.of_openCover.
Every smooth morphism of schemes is geometrically reduced.