Reduced tensor products over perfect fields

Every reduced algebra over a perfect field is geometrically reduced. The tensor product of two reduced algebras over a perfect field is therefore reduced, with no finite-generation hypothesis on either factor. This supplies the reduced tensor square needed to form reductions of affine groups.

References

• The Stacks Project, Tag 030U, reduced algebras after separable field extension.

instance TauCeti.instIsGeometricallyReducedOfPerfectField (k : Type u_1) [Field k] [PerfectField k] (A : Type u_2) [CommRing A] [Algebra k A] [IsReduced A] : Algebra.IsGeometricallyReduced k A

A reduced algebra over a perfect field is geometrically reduced, without a finite-generation hypothesis.

instance TauCeti.instIsReducedTensorProductOfPerfectField (k : Type u_1) [Field k] [PerfectField k] (A : Type u_2) (B : Type u_3) [CommRing A] [Algebra k A] [IsReduced A] [CommRing B] [Algebra k B] [IsReduced B] : IsReduced (TensorProduct k A B)

The tensor product of reduced algebras over a perfect field is reduced. Neither factor needs to be finitely generated.