Tracking issue: dimension theory of (commutative) rings

[chrisflav]

The state of dimension theory in mathlib is very immature, but many things have been proven in various public or private repositories. This issue is meant to track the state of dimension theory and the road to mathlib.

Feel free to edit this issue to add projects you are aware of.

Completed or ongoing projects

• Krull's height theorem: done by @erdOne in this lean3 repository. A group of PKU students is working on porting it (see open PRs)
• Dimension of polynomial rings (also includes going-down and similar results): done by a group of PKU students here. This partly depends on Krull's height theorem.
• $$dim R/(x) + 1 \le dim R$$ for a non-zero divisor $$x$$: done by @erdOne (link?)
• Hilbert polynomials, Hilbert-Serre theorem: done by @jjaassoonn in fg graded ring #9819
• more on dimension theory done by @jjaassoonn in Dimension theory #6277

PRs

Port of Krull's height theorem

• feat(Algebra/Module): the minimum cardinality of generating set #20744
• [Merged by Bors] - feat(RingTheory/Ideal): the height of an ideal  #20741

General purpose preparations

• [Merged by Bors] - feat(RingTheory): minimal primes are contained in zero divisors #20306
• feat(RingTheory/FaithfullyFlat): equivalent characterizations for algebras #20725