Geometrically reduced algebras

In this file we introduce geometrically reduced algebras. For a field k, we say that a k-algebra A is geometrically reduced (IsGeometricallyReduced) if the tensor product AlgebraicClosure k ⊗[k] A is reduced.

Main results

• IsGeometricallyReduced.of_forall_fg: for a field k and a commutative k-algebra A, if all finitely generated subalgebras B of A are geometrically reduced, then A is geometrically reduced.

References

• See [https://stacks.math.columbia.edu/tag/05DS] for some theory of geometrically reduced algebras. Note that their definition differs from the one here, we still need a proof that these are equivalent (see TODO).

TODO

• Prove that if A is a geometrically reduced k-algebra, then for every field extension K of k the K-algebra K ⊗[k] A is reduced.

class Algebra.IsGeometricallyReduced (k : Type u_3) (A : Type u_4) [Field k] [Ring A] [Algebra k A] : Prop

The k-algebra A is geometrically reduced iff its base change to AlgebraicClosure k is reduced.

• isReduced_algebraicClosure_tensorProduct : IsReduced (TensorProduct k (AlgebraicClosure k) A)

theorem Algebra.isGeometricallyReduced_iff (k : Type u_3) (A : Type u_4) [Field k] [Ring A] [Algebra k A] : IsGeometricallyReduced k A ↔ IsReduced (TensorProduct k (AlgebraicClosure k) A)

instance Algebra.instIsReducedTensorProductOfIsAlgebraicOfIsGeometricallyReduced (k : Type u_3) (A : Type u_4) (K : Type u_5) [Field k] [Ring A] [Algebra k A] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] [IsGeometricallyReduced k A] : IsReduced (TensorProduct k K A)

theorem Algebra.IsGeometricallyReduced.of_injective {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] {B : Type u_3} [Ring B] [Algebra k B] (f : A →ₐ[k] B) (hf : Function.Injective ⇑f) [IsGeometricallyReduced k B] : IsGeometricallyReduced k A

theorem Algebra.isReduced_of_isGeometricallyReduced (k : Type u_1) {A : Type u_2} [Field k] [Ring A] [Algebra k A] [IsGeometricallyReduced k A] : IsReduced A

theorem Algebra.IsGeometricallyReduced.of_forall_fg {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (h : ∀ (B : Subalgebra k A), B.FG → IsGeometricallyReduced k ↥B) : IsGeometricallyReduced k A

If all finitely generated subalgebras of A are geometrically reduced, then A is geometrically reduced.