[Merged by Bors] - feat: Chevalley's theorem

[YaelDillies]

This is https://stacks.math.columbia.edu/tag/00FE.

From GrowthInGroups (LeanCamCombi)

Co-authored-by: Andrew Yang

---

• depends on: [Merged by Bors] - feat: the prime spectrum is quasi-separated #21362

[github-actions]

PR summary 2df7b1e4c8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (new file)	1648

---

Declarations diff

+ BasicConstructibleSetData
+ chevalley_mvPolynomialC
+ chevalley_mvPolynomial_mvPolynomial
+ chevalley_polynomialC
+ degBound_casesOn_succ
+ degBound_le_degBound
+ degBound_pos
+ degBound_succ
+ degBound_zero
+ instance : DecidableEq (BasicConstructibleSetData R) := Classical.decEq _
+ map_comp'
+ map_id'
+ numBound_casesOn_succ
+ numBound_mono
+ numBound_succ
+ numBound_zero
++ numBound
++- map
++- map_comp
++- map_id
++- toSet
++- toSet_map
+-++ degBound

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
1166	1	erw

Current commit 2df7b1e4c8
Reference commit 8deb89281c

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[AntoineChambert-Loir]

Would it be worthy to try to track degree and number of open sets separately?
(I'd say yes: in some parts of AG, it's useful to know that some varieties are defined by equations of degree 2.)

[YaelDillies]

Do you mean "number of polynomials" rather than "number of open sets"? We're tracking the former, not the latter.

Given the shape of the bound (a tower of size depending on both the degree and number of polynomials used to describe the original variety), I doubt it is possible to track both variables independently.

[chrisflav]

Maybe what Antoine is asking, is to have separate bounds on the degree and the number of polynomials, not necessarily independent of each other? In this case, it seems that this is what actually happens in chevalley_mvPolynomial_mvPolynomial, but this doc string does suggest something else, namely that there is only one M bounding both the number of polynomials and degrees. Could you clarify this in this docstring?

[YaelDillies]

Yes, I wrote the docstring informally because the fact that there is a bound is all that matters, really. chevalley_mvPolynomial_mvPolynomial features two bounds solely because we can't (usefully) make those bounds into one due to mutual recursion.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: the prime spectrum is quasi-separated #21362
  By Dependent Issues (🤖). Happy coding!

[chrisflav]

I went through most of the overall strategy and docstrings, but I yet have to have a closer look at the proofs, which I'll hopefully find time to do before the end of the week.

[jcommelin]

bors d+

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

Thank you everyone for the reviews! This is a great milestone.

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Canceled.

[YaelDillies]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style