feat(RingTheory): regular local ring is domain

[Thmoas-Guan]

In this PR, we proved for a regular local ring R,
1 : for a finite set S in the maximal Ideal of R, it can be extended to a regular system of parameters iff they are linear independent in the cotangent space iff R/span S is regular local ring of dimesion dim R - |S|

2 : is domain
3 : regular system of parameter form regular sequence.

---

• depends on: [Merged by Bors] - feat(RingTheory): definition of regular local ring #28682
• depends on: feat(RingTheory/minimalPrimes): add some lemmas for minimalPrimes #37500

[github-actions]

PR summary 4ec5d95aa6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.RegularLocalRing.Basic (new file)	2162

---

Declarations diff

+ FiniteRingKrullDim.ringKrullDim_eq_nat
+ Ideal.height_eq_zero_iff
+ Ideal.span_singleton_mul_eq_self_of_isPrime
+ IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ IsLocalRing.maximalIdeal_sq_lt_maximalIdeal
+ IsLocalRing.spanFinrank_maximalIdeal_quotient
+ instance [IsRegularLocalRing R] : IsDomain R := isDomain_of_isRegularLocalRing R
+ isDomain_of_isRegularLocalRing
+ isRegular_of_span_eq_maximalIdeal
+ minimalPrimes_isPrime
+ quotient_isRegularLocalRing_tfae
+ quotient_span_singleton
+ spanFinrank_eq_one_iff

You can run this locally as follows

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

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

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

---

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

Current number	Change	Type
6899	4	backward.isDefEq.respectTransparency

Current commit fa61664280
Reference commit 4ec5d95aa6

You can run this locally as

./scripts/reporting/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).

[Thmoas-Guan]

This PR is depending some lemma developed from Krull heights theorem.

[erdOne]

Maybe we should have

lemma Ideal.IsMaximal.le_iff_eq
    {α : Type*} [Semiring α] {I J : Ideal α} (hI : I.IsMaximal) (hJ : J ≠ ⊤) : I ≤ J ↔ I = J :=
  ⟨Ideal.IsMaximal.eq_of_le hI hJ, le_of_eq⟩

lemma Ideal.subset_iUnion_iff_mem_of_isMaximal_of_finite
    {R : Type*} [CommRing R] {M : Ideal R} [M.IsMaximal] {S : Set (Ideal R)}
    (hs : S.Finite) (a b : Ideal R) (hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime)
    (ha : a ≠ ⊤) (hb : b ≠ ⊤) : ((M : Set R) ⊆ ⋃ I ∈ S, I) ↔ M ∈ S := by
  rw [Ideal.subset_union_prime_finite hs a b (by simpa)]
  trans ∃ i ∈ S, M = i
  · refine exists_congr fun I ↦ and_congr_right fun hI ↦ ‹M.IsMaximal›.le_iff_eq ?_
    by_cases I = a; · aesop
    by_cases I = b; · aesop
    exact (hp _ hI ‹_› ‹_›).ne_top
  · simp

as its own lemma as well?

So that this obtain would become

    have : ¬ (maximalIdeal R : Set R) ⊆ ⋃ I ∈ insert (maximalIdeal R ^ 2) (minimalPrimes R), I := by
      suffices maximalIdeal R ∉ insert (maximalIdeal R ^ 2) (minimalPrimes R) by
        rwa [Ideal.subset_iUnion_iff_mem_of_isMaximal_of_finite _ (maximalIdeal R ^ 2) ⊥]
        all_goals simp +contextual [Ideal.isPrime_of_mem_minimalPrimes,
            Ideal.IsMaximal.ne_top, minimalPrimes.finite_of_isNoetherianRing]
      have h₀ : 1 ≤ (maximalIdeal R).height :=
        WithBot.coe_le_coe.mp (le_trans (b := ↑(n + 1)) (by norm_cast; simp) (by simp [*]))
      have h₁ : maximalIdeal R ^ 2 < maximalIdeal R := by
        simp [IsLocalRing.maximalIdeal_sq_lt_maximalIdeal, isField_iff_maximalIdeal_eq]; aesop
      simp [← Ideal.height_eq_zero_iff_mem_minimalPrimes, h₁.ne']
      aesop
    obtain ⟨x, xmem, xnmem⟩ := Set.not_subset_iff_exists_mem_notMem.mp this

if you add the missing lemmas

lemma Ideal.isPrime_of_mem_minimalPrimes {R : Type*} [CommRing R] {I : Ideal R}
    (hI : I ∈ minimalPrimes R) : I.IsPrime := Ideal.minimalPrimes_isPrime hI

lemma Ideal.height_eq_zero_iff_mem_minimalPrimes
    {R : Type*} [CommRing R] {I : Ideal R} [I.IsPrime] :
    I.height = 0 ↔ I ∈ minimalPrimes R := by
  simp [Ideal.height_eq_primeHeight, Ideal.primeHeight_eq_zero_iff]

lemma IsLocalRing.maximalIdeal_sq_lt_maximalIdeal
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] :
    maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬ IsField R := by
  trans ¬ IsIdempotentElem (maximalIdeal R)
  · simp [IsIdempotentElem, ← pow_two, lt_iff_le_and_ne, Ideal.pow_le_self]
  · simp [Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing, Ideal.IsPrime.ne_top,
      isField_iff_maximalIdeal_eq]

instance {α : Type*} [AddCommMonoid α] [Subsingleton (AddUnits α)] :
    Subsingleton (AddUnits (WithBot α)) where
  allEq := by
    rintro ⟨a, b, hab, hba⟩ ⟨c, d, hcd, hdc⟩; revert a b c d
    simp [WithBot.forall, ← WithBot.coe_add]

[Thmoas-Guan]

@erdOne Do you have idea where should the third lemma go? find_home didn't give reasonable suggestions.

[erdOne]

I would suppose somewhere near Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing?

[Thmoas-Guan]

The first lemma is hI.1.1, the second have no trouble rewriting both sides, even easier from right side, do you think they are needed?

[erdOne]

I don't think we should be abusing the underlying defeq for minimalPrimes so I would say yes. I would even try to remove all the hI.1.1's currently in mathlib but of course this shouldn't be done in this PR.

[erdOne]

Maybe we should even make Ideal.primeHeight private...
Not entirely sure about this.

[Thmoas-Guan]

Fine, maybe I should do some of these in a separate PR, I agree on your first two comments, for making Ideal.primeHeight private I have no idea.

[Thmoas-Guan]

I've opened #37500

[Thmoas-Guan]

Now back to the main part, do we really need a prime avoidance for maximal ideal? I think it is not really useful, in contrast the application to maximalIdeal R with (maximalIdeal R)^2 and a set of primes (associated primes/minimal primes) are used in other places, what do you think?

[erdOne]

I do tend to believe that the Ideal.subset_iUnion_iff_mem_of_isMaximal_of_finite I provided is enough steps away from the prime avoidance for primes that it would be useful to have.