Commit 2025-11-13 13:13 d43fad94

View on Github →

feat: define geometrically reduced algebras (#27400) Define geometrically reduced algebras, and prove that if all finitely generated subalgebras of an algebra A are geometrically reduced, then A is geometrically reduced.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Adjoin/FGBaseChange.lean

added theorem exists_fg_and_mem_baseChange

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem IsReduced.tensorProduct_of_flat_of_forall_fg

Modified Mathlib/RingTheory/Nilpotent/Defs.lean

added theorem exists_isNilpotent_of_not_isReduced

Created Mathlib/RingTheory/Nilpotent/GeometricallyReduced.lean

added theorem Algebra.IsGeometricallyReduced.of_forall_fg

added theorem Algebra.IsGeometricallyReduced.of_injective

added theorem Algebra.isReduced_of_isGeometricallyReduced

Modified Mathlib/RingTheory/TensorProduct/Maps.lean

added def Subalgebra.baseChange

added theorem Subalgebra.tmul_mem_baseChange