[Merged by Bors] - feat(RingTheory): definition of regular local ring by Thmoas-Guan · Pull Request #28682 · leanprover-community/mathlib4

Thmoas-Guan · 2025-08-20T08:36:02Z

In this PR, we give the definition of regular local ring.
The class IsRegularLocalRing is defined as (maximalIdeal R).spanFinrank = ringKrullDim R
We also established the lemma IsRegularLocalRing.iff_finrank_cotangentSpace proving this definition is equivalent to the cotangent space version.

depends on: [Merged by Bors] - feat(RingTheory): some lemma about span rank #35337

github-actions · 2025-08-20T08:37:07Z

PR summary 56e100aabd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.RegularLocalRing.Defs` (new file)	2148

Declarations diff

+ IsRegularLocalRing
+ iff_finrank_cotangentSpace
+ instance [IsLocalRing R] [IsDomain R] [IsPrincipalIdealRing R] : IsRegularLocalRing R := by
+ isRegularLocalRing_iff
+ of_ringEquiv
+ of_spanFinrank_maximalIdeal_le
+ ringKrullDim_le_spanFinrank_maximalIdeal

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) = (1.00, 0.00)

Current number	Change	Type
8728	1	backward.isDefEq

Current commit 24105372eb
Reference commit 56e100aabd

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

chrisflav

I am happy to see that someone finally went forward and pinned down a definition.

chrisflav · 2025-08-20T09:08:18Z

Please also extend the PR description by which definition you choose and that you show it is equivalent to the Cotangent space one.

Thmoas-Guan · 2025-08-20T09:09:56Z

I am happy to see that someone finally went forward and pinned down a definition.

I choose this definition only because it depends the least to state, maybe there are other opinions I haven't heard of, but at least it can be easily changed to the cotangent space definition. And thanks for the help, these PR are currently a bit messy.

chrisflav · 2025-08-20T09:15:03Z

I am happy to see that someone finally went forward and pinned down a definition.

I choose this definition only because it depends the least to state, maybe there are other opinions I haven't heard of, but at least it can be easily changed to the cotangent space definition. And thanks for the help, these PR are currently a bit messy.

I personally would have chosen the cotangent space definition, but it really does not matter, so please stick to your definition. Other people wanted to go via regular sequences, but as far as I can tell, this is also on your roadmap?

Thmoas-Guan · 2025-08-20T09:40:31Z

What on my roadmap? Regular system of parameters is regular seqence? If this then it is in #28683

chrisflav · 2025-08-20T09:44:58Z

What on my roadmap? Regular system of parameters is regular seqence? If this then it is in #28683

~~Do you also have the converse? If the maximal ideal is generated by a regular sequence of length dim R, then R is regular?~~ (this is trivial and already contained in this PR)
Yes, wonderful. Then I am very happy with your definition in this PR.

and add docstring

This reverts commit 78b6206.

Thmoas-Guan · 2025-08-26T07:04:38Z

Sorry that I just move the file, I'll try to address the comments

mathlib-dependent-issues · 2026-03-20T19:20:31Z

This PR/issue depends on:

~~[Merged by Bors] - feat(RingTheory): some lemma about span rank #35337~~
By Dependent Issues (🤖). Happy coding!

chrisflav · 2026-03-20T23:26:51Z

Could you please merge master?

chrisflav

Thanks!

maintainer merge

github-actions · 2026-03-27T15:48:18Z

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

pull_request_review, wf_run

riccardobrasca

Thanks!

bors d+

mathlib-bors · 2026-03-30T08:15:33Z

✌️ Thmoas-Guan can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Thmoas-Guan · 2026-03-30T17:01:40Z

bors r+

In this PR, we give the definition of regular local ring. The class `IsRegularLocalRing` is defined as `(maximalIdeal R).spanFinrank = ringKrullDim R` We also established the lemma `IsRegularLocalRing.iff_finrank_cotangentSpace` proving this definition is equivalent to the cotangent space version.

mathlib-bors · 2026-03-30T17:18:28Z

Pull request successfully merged into master.

Build succeeded:

…ity#28682) In this PR, we give the definition of regular local ring. The class `IsRegularLocalRing` is defined as `(maximalIdeal R).spanFinrank = ringKrullDim R` We also established the lemma `IsRegularLocalRing.iff_finrank_cotangentSpace` proving this definition is equivalent to the cotangent space version.

Thmoas-Guan added 6 commits August 18, 2025 10:52

Update Basic.lean

78b6206

Merge branch 'master' into WithBot-ENat-lemmas

74b6e46

define regular local ring

0d9df37

regular local ring is domain

58bfa3c

Update RegularLocalRing.lean

dbbc1d0

Update RegularLocalRing.lean

cb08e01

Thmoas-Guan added the t-ring-theory Ring theory label Aug 20, 2025

chrisflav reviewed Aug 20, 2025

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 20, 2025

chrisflav self-assigned this Aug 20, 2025

Thmoas-Guan mentioned this pull request Aug 20, 2025

feat(RingTheory): regular local ring is domain #28683

Open

3 tasks

Thmoas-Guan added 3 commits August 20, 2025 19:51

rearrange lemmas

1409e55

and add docstring

fix lemma name

f0eee47

Revert "Update Basic.lean"

df1e3df

This reverts commit 78b6206.

Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 20, 2025

chrisflav reviewed Aug 22, 2025

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 22, 2025

Thmoas-Guan added 2 commits August 26, 2025 10:59

Merge branch 'master' into Regular-Local-Ring-Def

b63f40c

Move Regular Local ring into folder

f525679

Thmoas-Guan mentioned this pull request Aug 26, 2025

[Merged by Bors] - feat(RingTheory): definition of regular ring #28684

Closed

1 task

Thmoas-Guan added 3 commits August 26, 2025 15:57

fix lemma name

5bce000

Merge branch 'master' into Regular-Local-Ring-Def

64a6daf

Merge branch 'master' into Regular-Local-Ring-Def

240a55d

Merge branch 'spanRank-lemma' into Regular-Local-Ring-Def

19c1337

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 20, 2026

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 20, 2026

Merge branch 'master' into Regular-Local-Ring-Def

29fec98

Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2026

chrisflav reviewed Mar 21, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/RegularLocalRing/Defs.lean Outdated

Comment thread Mathlib/RingTheory/RegularLocalRing/Defs.lean Outdated

Comment thread Mathlib/RingTheory/RegularLocalRing/Defs.lean Outdated

Comment thread Mathlib/RingTheory/RegularLocalRing/Defs.lean Outdated

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2026

Thmoas-Guan added 3 commits March 21, 2026 22:59

fix naming

3ddb6f3

refine def

a979108

fix doc

a5f4135

Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2026

chrisflav reviewed Mar 27, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/RegularLocalRing/Defs.lean Outdated

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026

combine instances

2410537

Thmoas-Guan removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026

chrisflav approved these changes Mar 27, 2026

View reviewed changes

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

riccardobrasca reviewed Mar 30, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/RegularLocalRing/Defs.lean

mathlib-triage Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 30, 2026

mathlib-bors Bot changed the title ~~feat(RingTheory): definition of regular local ring~~ [Merged by Bors] - feat(RingTheory): definition of regular local ring Mar 30, 2026

mathlib-bors Bot closed this Mar 30, 2026

Conversation

Thmoas-Guan commented Aug 20, 2025 • edited by alreadydone Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Aug 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 56e100aabd

Import changes for modified files

Declarations diff

Uh oh!

chrisflav left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

chrisflav commented Aug 20, 2025

Uh oh!

Thmoas-Guan commented Aug 20, 2025

Uh oh!

chrisflav commented Aug 20, 2025

Uh oh!

Thmoas-Guan commented Aug 20, 2025

Uh oh!

chrisflav commented Aug 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Thmoas-Guan commented Aug 26, 2025

Uh oh!

mathlib-dependent-issues Bot commented Mar 20, 2026

Uh oh!

chrisflav commented Mar 20, 2026

Uh oh!

Uh oh!

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 Mar 27, 2026

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors Bot commented Mar 30, 2026

Uh oh!

Thmoas-Guan commented Mar 30, 2026

Uh oh!

mathlib-bors Bot commented Mar 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Thmoas-Guan commented Aug 20, 2025 •

edited by alreadydone

Loading

github-actions Bot commented Aug 20, 2025 •

edited

Loading

chrisflav commented Aug 20, 2025 •

edited

Loading