Feat (RingTheory/Ideal/KrullDimension): defined the Krull dimension of a ring.

[FMLJohn]

The ring theoretic krull dimension is the order theoretic krull dimension applied to its prime spectrum. Unfolding this definition, it is the length of longest series of prime ideals ordered by inclusion.

@mariainesdff

---

• [x] depends on: #11147

[github-actions[bot]]

PR summary 11d3bac1b8

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic	1320	1325	+5 (+0.38%)

Import changes for all files

Files	Import difference
42 files Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed	5
Mathlib.RingTheory.KrullDimension.Basic	1055
Mathlib.RingTheory.KrullDimension.Field	1056

---

Declarations diff

+ LTSeries.length_le_krullDim + PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim + RingEquiv.ringKrullDim + krullDim_nonpos_of_subsingleton + ringKrullDim + ringKrullDim_eq_bot_of_subsingleton + ringKrullDim_eq_of_ringEquiv + ringKrullDim_eq_zero_of_field + ringKrullDim_eq_zero_of_isField + ringKrullDim_le_of_surjective + ringKrullDim_nonneg_of_nontrivial + ringKrullDim_quotient_le

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.

[jjaassoonn]

Note that the basic part of this PR is actually #11147

[mariainesdff]

Note that the basic part of this PR is actually #11147

Ah thanks, I didn't know about that one. I will list it as a dependency.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11147~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

What happened with the idea of having a predicate krullDimLT that asserted that the krullDim of a given ring/space/... was LT a given natural number? Is there a discussion recorded somewhere with the pros and cons and the reason for going with a function valued in WithTop (WithBot _)?

[FMLJohn]

What happened with the idea of having a predicate krullDimLT that asserted that the krullDim of a given ring/space/... was LT a given natural number? Is there a discussion recorded somewhere with the pros and cons and the reason for going with a function valued in WithTop (WithBot _)?

No I have checked the streams on Zulip and I don't think there is any recorded discussion on that. The reason why we use WithTop (WithBot _) is that we eventually want ⊥ + ⊺ = ⊥. It is true that for topological spaces X and Y, dim(X × Y) = dim(X) + dim(Y). Now if X is empty and Y is infinite-dimensional, then X × Y is also empty. So we have ⊥ + ⊺ = dim(X) + dim(Y) = dim(X × Y) = ⊥.

[jjaassoonn]

I think Johan is referring to @kbuzzard's idea that instead of defining krullDim, we can introduce a family of predicate krullDimLT, then the negative infinity case is krullDimLT 0, positive infinity case is \forall n, \not krullDimLT n and krull dimension equal to n is krullDimLT (n +1) and \not krullDimLT n

[FMLJohn]

Also please use variable {R S : Type*} [CommRing R] [CommRing S] at the top of the file.

Done!

[FMLJohn]

I think Johan is referring to @kbuzzard's idea that instead of defining krullDim, we can introduce a family of predicate krullDimLT, then the negative infinity case is krullDimLT 0, positive infinity case is \forall n, \not krullDimLT n and krull dimension equal to n is krullDimLT (n +1) and \not krullDimLT n

I have asked @kbuzzard recently and he said that both WithBot (WithTop Nat) and krullDimLT have advantages. We can define krullDimLT in another PR.

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[jcommelin]

@FMLJohn @erdOne @mattrobball what is the status here? I think this one fell through some cracks in the queue.

[mattrobball]

It looks like #14721 did not deprecate anything or provide an adaptation path here. @apnelson1 can you find this PR? Thanks.

[mattrobball]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style