Reducedness of smooth algebras

A smooth algebra over a reduced commutative ring is reduced. The proof first treats integral domains: a standard-smooth algebra embeds into its étale generic fibre over a polynomial ring, and a standard-smooth localization cover gives the smooth case. For a reduced Noetherian base, embed the base into the finite product of its minimal-prime domain quotients and use flatness. Finally, Noetherian descent and passage through finitely generated subalgebras give the result over an arbitrary reduced base.

Over any commutative ring, a smooth algebra is geometrically reduced: its base changes to algebraic closures of residue fields are smooth over fields, hence reduced. This supplies the reducedness of geometric fibres used in the study of smooth affine group schemes.

Main declarations

• TauCeti.isReduced_of_smooth: a smooth algebra over a reduced commutative ring is reduced.
• TauCeti.isGeometricallyReduced_of_smooth: a smooth algebra over any commutative ring is geometrically reduced.

References

• The Stacks Project, Lemma 10.163.7.
• The Stacks Project, Section 10.140, Smooth algebras over fields.

theorem TauCeti.isReduced_of_smooth (R : Type u) (A : Type v) [CommRing R] [IsReduced R] [CommRing A] [Algebra R A] [Algebra.Smooth R A] : IsReduced A

A smooth algebra over a reduced commutative ring is reduced.

theorem TauCeti.isGeometricallyReduced_of_smooth (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] [Algebra.Smooth R A] : Algebra.IsGeometricallyReduced R A

A smooth algebra over a commutative ring is geometrically reduced.