refactor: generalize IsIntegrallyClosed away from fraction fields #7116

Vierkantor · 2023-09-12T11:46:41Z

Instead of saying IsIntegrallyClosed R means the ring R contains all integral elements of the ring of fractions, we follow, as suggested by @alreadydone in the review for #6126, the convention by the Stacks project and paramerize over an arbitrary algebra A: IsIntegrallyClosed R A means R contains all integral elements of A.

Most results generalize straightforwardly. The general algorithm: if the fraction field is already there, use that. Otherwise use FractionRing R.

TODO: generalize away from IsFractionRing if they are not needed.

depends on: [Merged by Bors] - refactor: remove IsDomain hypothesis from IsIntegrallyClosed #6126

ericrbg · 2023-09-12T12:05:19Z

Mathlib/RingTheory/IntegrallyClosed.lean


-variable {R : Type*} [CommRing R]
+-- TODO: this section can be generalized from `IsFractionRing` to any `Algebra` that is injective,
+-- but there is no way to hook that assumption up to the typeclass system.


iirc, it's NoZeroSmulDivisors

The identity homomorphism from R to itself is injective but wouldn't satisfy NoZeroSmulDivisors if R has zero divisors.

ah, indeed, I just remember using it in flt-reg for that purpose but that's just because we were dealing with domains at all times

Mathlib/Algebra/GCDMonoid/IntegrallyClosed.lean

Mathlib/RingTheory/IntegrallyClosed.lean

alreadydone · 2023-09-13T02:08:20Z

Mathlib/RingTheory/IntegrallyClosed.lean


-variable {R : Type*} [CommRing R]
+-- TODO: this section can be generalized from `IsFractionRing` to any `Algebra` that is injective,
+-- but there is no way to hook that assumption up to the typeclass system.


The identity homomorphism from R to itself is injective but wouldn't satisfy NoZeroSmulDivisors if R has zero divisors.

Mathlib/RingTheory/IntegrallyClosed.lean

leanprover-community-mathlib4-bot · 2023-09-14T11:47:01Z

This PR/issue depends on:

~~[Merged by Bors] - refactor: remove IsDomain hypothesis from IsIntegrallyClosed #6126~~
By Dependent Issues (🤖). Happy coding!

Mathlib/RingTheory/IsAdjoinRoot.lean

Instead of saying `IsIntegrallyClosed R` means the ring `R` contains all integral elements of the ring of fractions, we follow the convention by the Stacks project and paramerize over an arbitrary algebra `A`: `IsIntegrallyClosed R A` means `R` contains all integral elements of `A`. Most results generalize straightforwardly.

The general algorithm: if the fraction field is already there, use that. Otherwise use `FractionRing R`. TODO: generalize away from `IsFractionRing` if they are not needed.

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

jcommelin · 2023-09-14T17:08:30Z

Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

@@ -71,7 +71,7 @@ end

 variable [IsDomain S] [NoZeroSMulDivisors R S]

-variable [IsIntegrallyClosed R]
+variable [IsIntegrallyClosed R (FractionRing R)]


Shouldn't we introduce a name for this? Can we call these rings "normal"?
@alreadydone do you have opinions on this?

Normal implies not only IsIntegrallyClosed R (FractionRing R) but also IsReduced according to Stacks' definition.
Maybe we could call this generalized version IsIntegrallyClosedIn and let IsIntegrallyClosed R := IsIntegrallyClosedIn R (FractionRing R), so the definition of IsIntegrallyClosed remains unchanged. To be honest I don't see much use of IsIntegrallyClosedIn yet ...

Vierkantor · 2023-09-27T09:30:00Z

Coming back to this, I indeed don't see a direct application for the changes. However, the integral closure machinery in Mathlib still feels somewhat messy at the moment so I'd like to spend some time figuring out how to make it better.

Continuing along Junyan's suggestion, can't we define IsIntegrallyClosedIn R A := IsIntegralClosure R R A and then IsIntegrallyClosed R := IsIntegrallyClosedIn R (FractionRing R)? I expect that would integrate the different classes in a neater way. I don't know if aliases or defs would be the best mechanisms.

alreadydone · 2023-09-27T15:53:23Z

Continuing along Junyan's suggestion, can't we define IsIntegrallyClosedIn R A := IsIntegralClosure R R A and then IsIntegrallyClosed R := IsIntegrallyClosedIn R (FractionRing R)? I expect that would integrate the different classes in a neater way. I don't know if aliases or defs would be the best mechanisms.

Indeed, there's IsIntegralClosure too. Sounds like a good idea!

…sedIn` This refactor adds a new definition `IsIntegrallyClosedIn R A` equal to `IsIntegralClosure R A A`, and redefines `IsIntegrallyClosed R` to equal `IsIntegrallyClosed R (FractionRing A)`. This should make it possible and convenient to generalize away from the fraction fields. This also more closely approximates the conventions of the Stacks project. This is a second attempt at the refactor, after #7116 which was much more messy.

Vierkantor · 2023-10-23T10:53:47Z

Closing in favour of #7857.

…sedIn` This refactor adds a new definition `IsIntegrallyClosedIn R A` equal to `IsIntegralClosure R A A`, and redefines `IsIntegrallyClosed R` to equal `IsIntegrallyClosed R (FractionRing A)`. This should make it possible and convenient to generalize away from the fraction fields. This also more closely approximates the conventions of the Stacks project. This is a second attempt at the refactor, after #7116 which was much more messy.

…sedIn` (#7857) This refactor adds a new definition `IsIntegrallyClosedIn R A` equal to `IsIntegralClosure R A A`, and redefines `IsIntegrallyClosed R` to equal `IsIntegrallyClosed R (FractionRing A)`. This should make it possible and convenient to generalize away from the fraction fields. This also more closely approximates the conventions of the Stacks project. This is a second attempt at the refactor, after #7116 which was much more messy.

Vierkantor mentioned this pull request Sep 12, 2023

[Merged by Bors] - refactor: remove IsDomain hypothesis from IsIntegrallyClosed #6126

Closed

1 task

Vierkantor added RFC Request for comment t-algebra Algebra (groups, rings, fields etc) labels Sep 12, 2023

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Sep 12, 2023

ericrbg reviewed Sep 12, 2023

View reviewed changes

alreadydone approved these changes Sep 13, 2023

View reviewed changes

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes label Sep 14, 2023

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Sep 14, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 14, 2023

Vierkantor commented Sep 14, 2023

View reviewed changes

Mathlib/RingTheory/IsAdjoinRoot.lean Outdated Show resolved Hide resolved

Vierkantor and others added 4 commits September 14, 2023 13:25

Add Junyan's notes on normal rings/domains

90e3679

Fixes

db4b2ac

The general algorithm: if the fraction field is already there, use that. Otherwise use `FractionRing R`. TODO: generalize away from `IsFractionRing` if they are not needed.

Review / lint suggestions

db78430

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Vierkantor force-pushed the integrallyClosed-plus-algebra branch from 1761fe8 to db78430 Compare September 14, 2023 13:25

Generalize from free: Field → CommRing

bbfe4cf

Vierkantor added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes RFC Request for comment merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Sep 14, 2023

Remove unused hypothesis

d0e3dad

jcommelin reviewed Sep 14, 2023

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 14, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 19, 2023

Vierkantor mentioned this pull request Oct 23, 2023

[Merged by Bors] - refactor(RingTheory/IntegrallyClosed): generalize to IsIntegrallyClosedIn #7857

Closed

Vierkantor closed this Oct 23, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor: generalize IsIntegrallyClosed away from fraction fields #7116

refactor: generalize IsIntegrallyClosed away from fraction fields #7116

Vierkantor commented Sep 12, 2023 •

edited by github-actions bot

ericrbg Sep 12, 2023

alreadydone Sep 13, 2023

ericrbg Sep 13, 2023

alreadydone Sep 13, 2023

leanprover-community-mathlib4-bot commented Sep 14, 2023

jcommelin Sep 14, 2023 •

edited

alreadydone Sep 14, 2023 •

edited

Vierkantor commented Sep 27, 2023

alreadydone commented Sep 27, 2023

Vierkantor commented Oct 23, 2023

refactor: generalize IsIntegrallyClosed away from fraction fields #7116

refactor: generalize IsIntegrallyClosed away from fraction fields #7116

Conversation

Vierkantor commented Sep 12, 2023 • edited by github-actions bot

ericrbg Sep 12, 2023

Choose a reason for hiding this comment

alreadydone Sep 13, 2023

Choose a reason for hiding this comment

ericrbg Sep 13, 2023

Choose a reason for hiding this comment

alreadydone Sep 13, 2023

Choose a reason for hiding this comment

leanprover-community-mathlib4-bot commented Sep 14, 2023

jcommelin Sep 14, 2023 • edited

Choose a reason for hiding this comment

alreadydone Sep 14, 2023 • edited

Choose a reason for hiding this comment

Vierkantor commented Sep 27, 2023

alreadydone commented Sep 27, 2023

Vierkantor commented Oct 23, 2023

Vierkantor commented Sep 12, 2023 •

edited by github-actions bot

jcommelin Sep 14, 2023 •

edited

alreadydone Sep 14, 2023 •

edited