feat(RingTheory/Ideal): more lemmas about the height of an ideal

[xyzw12345]

In this PR, we continue to port a part of Andrew Yang's lean3 repository at this repository, which is appoved by @erdOne after his discussion with @chrisflav . This PR follows #20741 (merged by Bors) and #20744.

We ported Andrew's definition of Ideal.height and Ideal.primeHeight with some small changes in #20741, and in this PR, we ported some more lemmas about these definitions, finishing the porting work of dimension_theory/height.lean in that repository.

• depends on: feat(Algebra/Module): the minimum cardinality of generating set #20744 [some of the lemmas used spanRank]
  Co-authored-by:
  @erdOne
  @Xuchun-Li [email protected]
  @jjdishere [email protected]
  @Blackfeather007 [email protected]
  @ShouxinZhang [email protected]

---

[github-actions]

PR summary 8415ff9a8d

Import changes exceeding 2%

%	File
+32.69%	Mathlib.RingTheory.Ideal.Height
+4.00%	Mathlib.RingTheory.Ideal.MinimalPrime.Localization
+4.10%	Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Ideal.Height	1147	1522	+375 (+32.69%)
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic	1121	1167	+46 (+4.10%)
Mathlib.RingTheory.Ideal.MinimalPrime.Localization	1126	1171	+45 (+4.00%)

Import changes for all files

Files	Import difference
18 files Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Order.KrullDimension Mathlib.RingTheory.Spectrum.Prime.Jacobson Mathlib.RingTheory.Spectrum.Prime.Noetherian	1
71 files Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Module.Presentation.Differentials Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.NumberField.Basic Mathlib.NumberTheory.NumberField.Completion Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.NumberField.Embeddings Mathlib.NumberTheory.NumberField.Norm Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.ZetaValues Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.RingTheory.Discriminant Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Extension Mathlib.RingTheory.Filtration Mathlib.RingTheory.Generators Mathlib.RingTheory.Ideal.Cotangent Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.Invariant Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Kaehler.Basic Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.RingTheory.Kaehler.Polynomial Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Localization.NormTrace Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.Presentation Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.RingTheory.Smooth.Basic Mathlib.RingTheory.Smooth.Kaehler Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Pi Mathlib.RingTheory.Smooth.StandardSmoothCotangent Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.RingTheory.Trace.Basic Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Basic Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.Pi Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.RingTheory.WittVector.Isocrystal	3
4 files Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.RingHom.Flat	8
Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField	9
Mathlib.RingTheory.Henselian	14
Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.RingTheory.LocalRing.ResidueField.Ideal	18
7 files Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.Surjective	23
5 files Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.Padics.Hensel Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Inverse	27
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization	28
5 files Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.DualNumber	30
5 files Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Topology.Sheaves.CommRingCat	35
Mathlib.RingTheory.Ideal.MinimalPrime.Localization	45
18 files Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.CharP.MixedCharZero Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.LocalSubring Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.Valuation.ExtendToLocalization	46
Mathlib.RingTheory.Ideal.Height	375
Mathlib.Algebra.Module.SpanRank (new file)	914

---

Declarations diff

+ FG.exists_fun_spanRankNat_span_range_eq
+ FG.spanBasis
+ FG.spanBasis_mem
+ FG.spanRank_le_iff_exists_span_range_eq
+ FG.span_range_spanBasis
+ FiniteRingKrullDim
+ Ideal.finiteHeight_of_le
+ Ideal.height_le_ringKrullDim_of_ne_top
+ Ideal.isMaximal_of_primeHeight_eq_ringKrullDim
+ Ideal.mem_minimalPrimes_of_height_eq
+ Ideal.minimalPrimes_comap_subset
+ Ideal.primeHeight_eq_ringKrullDim_iff
+ Ideal.primeHeight_eq_zero_iff
+ Ideal.primeHeight_le_ringKrullDim
+ IsLocalRing.maximalIdeal_height_eq_ringKrullDim
+ IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim
+ IsLocalization.AtPrime.ringKrullDim_eq_height
+ IsLocalization.height_comap
+ IsLocalization.minimalPrimes_comap
+ IsLocalization.minimalPrimes_map
+ IsLocalization.primeHeight_comap
+ _root_.Ideal.minimalPrimes_finite_of_isNoetherianRing
+ add_inj_of_ne_top
+ disjoint_comap_iff
+ exists_spanRank_le_and_le_height_of_le_height
+ fg_iff_spanRank_eq_spanRankNat
+ finiteDimensionalOrder_iff_krullDim_ne_bot_and_top
+ finiteRingKrullDim_iff_ne_bot_and_top
+ height_eq_krullDim_Iic
+ instance (priority := 900) Ideal.finiteHeightOfFiniteRingKrullDim {I : Ideal R}
+ instance : OrderTop (PrimeSpectrum R)
+ krullDim_eq_bot_iff_isEmpty
+ krullDim_eq_top_iff_infiniteDimensional
+ mem_minimalPrimes_of_primeHeight_eq_height
+ nonempty_of_finiteDimensional
+ nonempty_of_finiteDimensionalType
+ ringKrullDim_lt_top
+ ringKrullDim_ne_top
+ spanRank
+ spanRankNat
+ spanRank_bot
+ spanRank_eq_zero_iff_eq_bot
+ spanRank_ne_top_iff_fg
+ spanRank_span_set_finite
+ spanRank_sup_le_sum_spanRank

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.

---

No changes to technical debt.

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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Algebra/Module): the minimum cardinality of generating set #20744
  By Dependent Issues (🤖). Happy coding!