Skip to content

feat: localizations of primes in Dedekind domains are valuation subrings#33010

Open
xgenereux wants to merge 9 commits intoleanprover-community:masterfrom
xgenereux:IsDedekindDomain.ValuationSubring.ofPrime
Open

feat: localizations of primes in Dedekind domains are valuation subrings#33010
xgenereux wants to merge 9 commits intoleanprover-community:masterfrom
xgenereux:IsDedekindDomain.ValuationSubring.ofPrime

Conversation

@xgenereux
Copy link
Copy Markdown
Collaborator

@xgenereux xgenereux commented Dec 17, 2025 •
edited
Loading

The goal of this PR is the theorem valuationSubringAtPrime_eq_valuationSubring which states that the localization at a nonzero prime in a Dedekind domain is precisely the valuation subring of the valuation associated with that same prime.

Given a Dedekind domain R in its field of fractions K, we define IsDedekindDomain.valuationSubringAtPrime, which is the localization of R at a nonzero prime, viewed as valuation subring of K.

We show that valuationSubringAtPrime K v ≤ (valuation K v).valuationSubring and use maximality to show that they must be equal.

Other small note:

  • added a variant of intValuation_exists_uniformizer in terms of valuation (instead of intValuation).

Co-authored-by: María Inés de Frutos Fernández <[email protected]>

Open in Gitpod

@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 17, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 17, 2025 •
edited
Loading

PR summary 34f85c5f24

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsDedekindDomain.valuationSubringAtPrime
+ IsDedekindDomain.valuationSubringAtPrime.toSubring
+ instance : Algebra R (valuationSubringAtPrime K v)
+ instance : IsDedekindDomain (valuationSubringAtPrime K v)
+ instance : IsScalarTower R (valuationSubringAtPrime K v) K
+ instance : Ring.KrullDimLE 1 (valuationSubringAtPrime K v)
+ valuationSubringAtPrime_eq_valuationSubring
+ valuationSubringAtPrime_le_valuationValuationSubring
+ valuation_exists_uniformizer'

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.

No changes to technical debt.

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

@github-actions github-actions bot added the t-ring-theory Ring theory label Dec 17, 2025
@xgenereux
Copy link
Copy Markdown
Collaborator Author

xgenereux commented Dec 19, 2025

have now renamed to use IsDedekindDomain.valuationSubringAtPrime, do let me know if you think this is a bad name!

erdOne
erdOne reviewed Dec 20, 2025
View reviewed changes
erdOne
erdOne reviewed Dec 20, 2025
View reviewed changes
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

/-- Given `v : HeightOneSpectrum R`, the valuation associated to `v` has the localization of
`R` at `v` as valuation subring. -/
theorem valuationSubringAtPrime_eq_valuationSubring :
Copy link
Copy Markdown
Member

@erdOne erdOne Dec 20, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you mention this in the docstring of valuationSubringAtPrime_eq_valuationSubring? Thanks.

Copy link
Copy Markdown
Collaborator Author

@xgenereux xgenereux Mar 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's been a while, what do you remember what you meant?

@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 20, 2025
@xgenereux xgenereux added the WIP Work in progress label Jan 3, 2026
@xgenereux
Copy link
Copy Markdown
Collaborator Author

xgenereux commented Jan 5, 2026

The code of this PR will get simplified if we have #33634, so I will wait for that.
(I will update this PR based on #33634 if I have time in the following week.)

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 5, 2026
@xgenereux xgenereux force-pushed the IsDedekindDomain.ValuationSubring.ofPrime branch from 647945d to 9b44589 Compare March 6, 2026 16:53
@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 6, 2026
@xgenereux xgenereux removed awaiting-author A reviewer has asked the author a question or requested changes. WIP Work in progress labels Mar 6, 2026
@xgenereux
Copy link
Copy Markdown
Collaborator Author

xgenereux commented Mar 6, 2026 •
edited
Loading

I'll wait for the dependent PRs to see if the error goes away.

@xgenereux xgenereux force-pushed the IsDedekindDomain.ValuationSubring.ofPrime branch from bc91bd8 to 19b3452 Compare March 17, 2026 17:40
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 17, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 27, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 27, 2026

This PR/issue depends on:

@xgenereux xgenereux force-pushed the IsDedekindDomain.ValuationSubring.ofPrime branch from 76a1551 to 76efd7d Compare March 27, 2026 19:27
@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

Assignees

No one assigned

Labels

t-ring-theory Ring theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@xgenereux @erdOne @mathlib4-dependent-issues-bot