Geometrically reduced algebras

In this file we introduce geometrically reduced algebras. For a commutative ring R and an R-algebra A, we say that A is geometrically reduced (IsGeometricallyReduced) if for every prime ideal p of R, the base change of A to an algebraic closure of κ(p) is reduced. In the case of R = k a field, this is equivalent to AlgebraicClosure k ⊗[k] A being reduced.

Main results

• Algebra.isGeometricallyReduced_field_iff : for a field k and a commutative k-algebra A, A is geometrically reduced iff AlgebraicClosure k ⊗[k] A is reduced.

• 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 R-algebra, then for every R-algebra K that is a field, the tensor product K ⊗[R] A is reduced. (@Thmoas-Guan)

class Algebra.IsGeometricallyReduced (R : Type u_3) (A : Type u_4) [CommRing R] [Ring A] [Algebra R A] : Prop

An R-algebra A is geometrically reduced iff for every prime ideal p of Rthe base change toAlgebraicClosure p.ResidueField` is reduced.

• isReduced_algebraicClosure_tensorProduct (p : Ideal R) [p.IsPrime] : IsReduced (TensorProduct R (AlgebraicClosure p.ResidueField) A)

theorem Algebra.isGeometricallyReduced_iff (R : Type u_3) (A : Type u_4) [CommRing R] [Ring A] [Algebra R A] : IsGeometricallyReduced R A ↔ ∀ (p : Ideal R) [inst : p.IsPrime], IsReduced (TensorProduct R (AlgebraicClosure p.ResidueField) A)

theorem Algebra.isGeometricallyReduced_field_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.