[Merged by Bors] - refactor(RingTheory/Ideal/Height): make `Ideal.primeHeight` private by Thmoas-Guan · Pull Request #37627 · leanprover-community/mathlib4

Thmoas-Guan · 2026-04-04T07:07:32Z

We mark Ideal.primeHeight as private, making Ideal.height the only public definition for heights of (prime) ideals. This makes the API more consistent and stops contributors from adding more declarations involving Ideal.primeHeight, which should instead be formulated in terms of Ideal.height.

To relate Ideal.height to the order theoretic Order.height in the lattice of prime ideals PrimeSpectrum we add a lemma PrimeSpectrum.height_eq_orderHeight.

depends on: [Merged by Bors] - refactor(RingTheory): refactor APIs for minimal primes to lessen defeq abuse #38029

github-actions · 2026-04-04T07:08:34Z

PR summary 45b8864a30

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Ideal.height_add_one_le_of_lt_of_isPrime
+ Ideal.height_eq_inf_minimalPrimes
+ Ideal.height_eq_ringKrullDim_iff
+ Ideal.height_eq_zero_iff
+ Ideal.height_le_ringKrullDim_of_isPrime
+ Ideal.height_lt_top_of_isPrime
+ Ideal.height_mono_of_isPrime
+ Ideal.height_ne_top_of_isPrime
+ Ideal.height_strict_mono_of_isPrime
+ Ideal.height_strict_mono_of_isPrime_of_isPrime
+ Ideal.height_strict_mono_of_isPrime_of_is_prime
+ Ideal.isMaximal_of_height_eq_ringKrullDim
+ Ideal.sup_isMaximal_height_eq_ringKrullDim
+ Ideal.sup_isPrime_height_eq_ringKrullDim
+ IsLocalization.height_under_eq_of_isPrime
+ PrimeSpectrum.height_eq_orderHeight
- Ideal.height_strict_mono_of_is_prime
- IsLocalization.primeHeight_under

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

chrisflav

Thanks a lot!
maintainer merge

github-actions · 2026-05-21T14:18:56Z

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

faenuccio · 2026-05-21T22:05:49Z

Can you explain why you want to make this private and update both the PR title (add a verb) and the description with this explanation?

Thmoas-Guan · 2026-05-22T05:41:17Z

Can you explain why you want to make this private and update both the PR title (add a verb) and the description with this explanation?

The motivation is sort of vague, this part is from Andrew's old lean3 repo, but when migrating many things wasn't thought carefully enough.
The current motivation is simple, to unify exposed API thus reduce confusion. If anyone have better description about this please pin me and I'll add it in description.
The original motivation for this is suggested by @erdOne.

chrisflav · 2026-05-22T16:08:58Z

Ideal.primeHeight is an implementation detail that is an auxiliary declaration to define Ideal.height. By making it private, the only public API we have is in terms of Ideal.height which makes the API more consistent. It also prevents contributors from adding new lemmas about Ideal.primeHeight that should instead be formulated in terms of Ideal.height.

faenuccio · 2026-05-22T16:13:00Z

Ideal.primeHeight is an implementation detail that is an auxiliary declaration to define Ideal.height. By making it private, the only public API we have is in terms of Ideal.height which makes the API more consistent. It also prevents contributors from adding new lemmas about Ideal.primeHeight that should instead be formulated in terms of Ideal.height.

Yes, I imagined that this was the rationale. But given that the proof translating from the general height to prime height is easy but non-trivial (see

mathlib4/Mathlib/RingTheory/Ideal/Height.lean

Lines 44 to 48 in a0d161d

    
           /-- For a prime ideal, its height equals its prime height. -/ 
        
           lemma Ideal.height_eq_primeHeight [I.IsPrime] : I.height = I.primeHeight := by 
        
             unfold height primeHeight 
        
             simp_rw [Ideal.minimalPrimes_eq_subsingleton_self] 
        
             simp

), I wonder why you say that primeHeight is only an implementation detail. I would argue that there might be cases where people are really only working with prime ideals and don't want to go through this each time.

chrisflav · 2026-05-22T16:16:05Z

If you want to use the order theoretic height, which only makes sense for prime ideals, you can use PrimeSpectrum.height_eq_orderHeight. All downstream users of Ideal.height should not need this though, as the file Ideal.Height should already provide all required API in the general case (and if that API does not exist, we can always still add it in that file).

faenuccio · 2026-05-22T16:24:02Z

If you want to use the order theoretic height, which only makes sense for prime ideals, you can use PrimeSpectrum.height_eq_orderHeight. All downstream users of Ideal.height should not need this though, as the file Ideal.Height should already provide all required API in the general case (and if that API does not exist, we can always still add it in that file).

OK, perfect, thanks, now I understand and I've reviewed the whole PR with a different eye.

faenuccio · 2026-05-22T16:24:07Z

bors r+

…37627) We mark `Ideal.primeHeight` as `private`, making `Ideal.height` the only public definition for heights of (prime) ideals. This makes the API more consistent and stops contributors from adding more declarations involving `Ideal.primeHeight`, which should instead be formulated in terms of `Ideal.height`. To relate `Ideal.height` to the order theoretic `Order.height` in the lattice of prime ideals `PrimeSpectrum` we add a lemma `PrimeSpectrum.height_eq_orderHeight`.

mathlib-bors · 2026-05-22T17:40:40Z

Build failed (retrying...):

ci (staging) / Build

…37627) We mark `Ideal.primeHeight` as `private`, making `Ideal.height` the only public definition for heights of (prime) ideals. This makes the API more consistent and stops contributors from adding more declarations involving `Ideal.primeHeight`, which should instead be formulated in terms of `Ideal.height`. To relate `Ideal.height` to the order theoretic `Order.height` in the lattice of prime ideals `PrimeSpectrum` we add a lemma `PrimeSpectrum.height_eq_orderHeight`.

mathlib-bors · 2026-05-22T18:07:37Z

Pull request successfully merged into master.

Build succeeded:

…eanprover-community#37627) We mark `Ideal.primeHeight` as `private`, making `Ideal.height` the only public definition for heights of (prime) ideals. This makes the API more consistent and stops contributors from adding more declarations involving `Ideal.primeHeight`, which should instead be formulated in terms of `Ideal.height`. To relate `Ideal.height` to the order theoretic `Order.height` in the lattice of prime ideals `PrimeSpectrum` we add a lemma `PrimeSpectrum.height_eq_orderHeight`.

Thmoas-Guan added 23 commits April 1, 2026 22:22

add two lemmas

ff03d3b

reduce .1.1

1f74255

add more heoght analogus

348b715

add le lemma

c24b383

reduce more .1.1 and .1.2

a12d523

add private and deprecation

e7fd6ee

golf Ideal.sup_primeHeight_eq_ringKrullDim

43fc664

fix

a580c9e

Merge branch 'master' into minimalPrimes-API

74377c6

make strict mono private

b5387ef

fix

732ccc0

deprecate strict mono

ae7cff9

golf

facecae

deprecate primeHeight_eq_zero

bc6aba4

fix

c043789

add height version of definition

a35ed7f

deprecate more lemmas

2eef181

deprecate more

e09911d

deprecate even more

55ca9bf

deprecate even more

618cfa2

deprecate a prime height usage

ab901db

Merge branch 'minimalPrimes-API' into refactor-primeHeight

4643655

deprecate further more

cd6b68c

github-actions Bot added the t-ring-theory Ring theory label Apr 4, 2026

Thmoas-Guan added the WIP Work in progress label Apr 4, 2026

golf

375cdb8

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 4, 2026

Thmoas-Guan added 2 commits April 6, 2026 11:11

Merge branch 'master' into minimalPrimes-API

c27d5f9

Merge branch 'minimalPrimes-API' into refactor-primeHeight

57a4272

Thmoas-Guan added 3 commits May 21, 2026 21:45

fix doc for primeHeight

825663a

fix naming

8cae927

temp fix

a4420aa

chrisflav reviewed May 21, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Ideal/Height.lean Outdated

chrisflav reviewed May 21, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Ideal/Height.lean Outdated

chrisflav reviewed May 21, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Ideal/Height.lean Outdated

fix naming

45b8864

chrisflav approved these changes May 21, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 21, 2026

faenuccio removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 21, 2026

faenuccio self-assigned this May 21, 2026

Thmoas-Guan changed the title ~~refactor(RingTheory/Ideal/Height): private Ideal.primeHeight~~ refactor(RingTheory/Ideal/Height): make Ideal.primeHeight private May 22, 2026

mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 22, 2026

mathlib-bors Bot changed the title ~~refactor(RingTheory/Ideal/Height): make Ideal.primeHeight private~~ [Merged by Bors] - refactor(RingTheory/Ideal/Height): make Ideal.primeHeight private May 22, 2026

mathlib-bors Bot closed this May 22, 2026

Conversation

Thmoas-Guan commented Apr 4, 2026 • edited by chrisflav Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Apr 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 45b8864a30

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented May 21, 2026

Uh oh!

faenuccio commented May 21, 2026

Uh oh!

Thmoas-Guan commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chrisflav commented May 22, 2026

Uh oh!

faenuccio commented May 22, 2026

Uh oh!

chrisflav commented May 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

faenuccio commented May 22, 2026

Uh oh!

faenuccio commented May 22, 2026

Uh oh!

mathlib-bors Bot commented May 22, 2026

Uh oh!

mathlib-bors Bot commented May 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Thmoas-Guan commented Apr 4, 2026 •

edited by chrisflav

Loading

github-actions Bot commented Apr 4, 2026 •

edited

Loading

Thmoas-Guan commented May 22, 2026 •

edited

Loading

chrisflav commented May 22, 2026 •

edited

Loading