[Merged by Bors] - feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings #18021

Paul-Lez · 2022-12-29T17:59:02Z

This PR generalizes some of the theory of minpoly to the setting of integrally closed rings. The main results proven here are:

minpoly.is_integrally_closed_eq_field_fractions and variants of it
minpoly.is_integrally_closed_dvd
monic.dvd_of_fraction_map_dvd_fraction_map

In a following PR, I will remove instances of gcd_domain_dvd (and the other results this PR generalises) from other files, and replace the file minpoly.gcd_domain by minpoly.is_integrally_closed

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

depends on: [Merged by Bors] - feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for integrally closed rings #18147

Paul-Lez · 2022-12-29T19:29:22Z

This PR is now ready for review. If someone has some advice on where the main results could be put, that would be super helpful.

ericrbg

some random stuff I saw - I'm too tired but I'll keep reviewing in the morning. it seems a lot of the results you have are strictly stronger than some already-existing ones so I'd just replace those in-place.

src/number_theory/temporary_file.lean

riccardobrasca

Can you please fix all the linter errors and change the name of temporary_file file?

We still don't know that a gcd_monoid is integrally closed, right?

ericrbg · 2022-12-30T11:30:46Z

@riccardobrasca, https://leanprover-community.github.io/mathlib_docs/algebra/gcd_monoid/integrally_closed.html

riccardobrasca · 2022-12-30T11:32:13Z

@riccardobrasca, leanprover-community.github.io/mathlib_docs/algebra/gcd_monoid/integrally_closed.html

Good! So there should be at least two or three results that can be generalized to integrally closed rings.

src/data/polynomial/algebra_map.lean

riccardobrasca · 2022-12-31T09:52:11Z

src/ring_theory/integral_closure.lean

@@ -125,6 +125,19 @@ begin
    aeval_alg_hom_apply, aeval_map_algebra_map, aeval_def, hP.2, _root_.map_zero]
 end

+lemma is_integral_of_commuting_diagram {R S T U : Type*} [nontrivial S] [nontrivial T]


Same comment as above about the name. This can maybe be golfed introducing some is_scalar_tower, but I am not sure.

I guess using is_scalar_tower is equivalent to this, since we have ring_hom.to_algebra. Which one would you think is most useful/practical to use?

src/ring_theory/integral_closure.lean

src/ring_theory/localization/fraction_ring.lean

src/ring_theory/polynomial/gauss_lemma.lean

src/number_theory/temporary_file.lean

…hree files (#18048) In this PR, we split the results contained in `minpoly.lean` into three separate files: `minpoly.basic.lean`, `minpoly.field.lean` and `minpoly.gcd_monoid.lean`. This is helpful for PR #18021.

…eory_PR

riccardobrasca · 2023-01-11T11:57:49Z

Actually I don't understand why you didn't generalize polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map to integrally closed domains (restricting to monic polynomials). Then gcd_domain_eq_field_fractions can be generalized to integrally closed domains, keeping essentially the same proof. In practice this gives is_integrally_closed_map_minpoly_eq_minpoly_fraction_ring with only is_domain S.
In any case note the inconsistency between the names of gcd_domain_eq_field_fractions and is_integrally_closed_map_minpoly_eq_minpoly_fraction_ring.

I hadn't really thought about that - I think what happened was I already had a proof of is_integrally_closed_map_minpoly_eq_minpoly_fraction_ring following the approach @alreadydone has suggested on Zulip, and realized I could generalize some of the results from gauss_lemma.lean to integrally closed domains only later. In any case I'll have a go at what you're suggesting!

I didn't check carefully, but it seems that the result about the minimal polynomial follow by the fact that irreducible over K is the same as irreducible over R. This is currently proved for primitive polynomials over gcd_monoid, but the minimal polynomial is always monic and for monic polynomials this is true over integrally closed domains (but we still want the version for primitive, that is more general, even if the assumption on R is stronger).

I think that the confusion is that there are two things people call "Gauss lemma":

the product of primitive polynomials is primitive: this is what we have for gcd_monoid, and I believe the strongest version is for UFD (it should be equivalent to being a UFD);
irreducibility/divisibility over R is the same as irreducibility/divisibility over K for monic polynomials. This follows from the first, but it is also true over integrally closed domains (it is equivalent to being integrally closed I believe).

The theory of minimal polynomial needed the second one.

…egrally closed rings (#18147) In this PR, we prove Gauss's lemma for integrally closed rings. See #18021 and #11523 for previous discussion on the topic. We also show that integrally closed domains are precisely the domains in which Gauss's lemma holds for monic polynomials. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2318021.20generalizing.20theory.20of.20minpoly) Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>

mathlib-dependent-issues-bot · 2023-01-14T17:46:04Z

This PR/issue depends on:

~~[Merged by Bors] - feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for integrally closed rings #18147~~
By Dependent Issues (🤖). Happy coding!

…eory_PR

riccardobrasca · 2023-01-15T19:52:10Z

Not that the other PR has been merged, can you summarize what is done in this one? For example, I guess the description needs to be updated.

Paul-Lez · 2023-01-15T20:46:06Z

Not that the other PR has been merged, can you summarize what is done in this one? For example, I guess the description needs to be updated.

Sure ! I'll first update the code - I think some of the lemmas I had written for the original proofs are no longer necessary for instance - and then update the summary.

src/data/polynomial/algebra_map.lean

riccardobrasca · 2023-01-17T16:28:58Z

src/data/polynomial/ring_division.lean

+  exact (lt_iff_not_ge _ _ ).mp h₂ (degree_le_of_dvd h₁ hc),
+end
+
+lemma eq_zero_of_nat_degree_lt {p q : R[X]} (h₁ : p ∣ q) (h₂ : nat_degree q < nat_degree p) :


If I am not confused by the implications, you can use this to generalize polynomial.monic.not_dvd_of_degree_lt removing the monic assumption. In doing so you should change the name of polynomial.monic.not_dvd_of_degree_lt, if this means modifying a lot of files where it is used can you please open another PR and asking for my review? It can be merged very quickly.

Sure, I'll try and have a go at that later on today!

Haha polynomial.monic.not_dvd_of_degree_lt was added by me days ago, so not many things depend on it. It holds for any semiring without need of no_zero_divisor though. Since this section has no_zero_divisors present, you can indeed prove a version without monic here.

Good point! Well I've just added the other version without monic - it's probably good to have both anyway

But I guess in that case no need to remove polynomial.monic.not_dvd_of_degree_lt from the files that use it :)

Yes, I didn't realize they had orthogonal assumptions.

src/field_theory/minpoly/gcd_monoid.lean

riccardobrasca · 2023-01-17T21:28:06Z

Thanks!

bors d+

bors · 2023-01-17T21:28:07Z

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

Paul-Lez · 2023-01-17T23:26:42Z

bors merge

…ngs (#18021) This PR generalizes some of the theory of `minpoly` to the setting of integrally closed rings. The main results proven here are: - `minpoly.is_integrally_closed_eq_field_fractions` and variants of it - `minpoly.is_integrally_closed_dvd` - `monic.dvd_of_fraction_map_dvd_fraction_map` In a following PR, I will remove instances of `gcd_domain_dvd` (and the other results this PR generalises) from other files, and replace the file `minpoly.gcd_domain` by `minpoly.is_integrally_closed` Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>

bors · 2023-01-18T01:35:28Z

Pull request successfully merged into master.

Build succeeded:

init

04a0277

Paul-Lez added WIP Work in progress t-algebra Algebra (groups, rings, fields etc) labels Dec 29, 2022

tidy

e325683

Paul-Lez added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Dec 29, 2022

Paul-Lez mentioned this pull request Dec 29, 2022

Develop basic theory of integrally closed domain #11523

Closed

ericrbg reviewed Dec 30, 2022

View reviewed changes

riccardobrasca requested changes Dec 30, 2022

View reviewed changes

riccardobrasca 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 Dec 30, 2022

Moved lemmas

a2a320c

Paul-Lez added awaiting-review The author would like community review of the PR WIP Work in progress and removed awaiting-author A reviewer has asked the author a question or requested changes awaiting-review The author would like community review of the PR labels Dec 30, 2022

riccardobrasca reviewed Dec 31, 2022

View reviewed changes

alreadydone reviewed Dec 31, 2022

View reviewed changes

Paul-Lez mentioned this pull request Jan 3, 2023

[Merged by Bors] - chore(field_theory/minpoly): Split results from minpoly.lean into three files #18048

Closed

WIP

1e65541

Paul-Lez added 5 commits January 4, 2023 09:59

Merge remote-tracking branch 'origin/master' into preliminary_ring_th…

f0cb426

…eory_PR

moved some lemmas and added import to gauss_lemma.lean

365d101

Fix cyclic import issue

52be975

More fixing of cyclic imports

19523e4

More lemmas moved, deleted temporary file

9f200d4

Paul-Lez added the WIP Work in progress label Jan 11, 2023

Paul-Lez mentioned this pull request Jan 12, 2023

[Merged by Bors] - feat(ring_theory/polynomial/gauss_lemma): Prove Gauss's Lemma for integrally closed rings #18147

Closed

mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 13, 2023

mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 14, 2023

Merge remote-tracking branch 'origin/master' into preliminary_ring_th…

49844f8

…eory_PR

Paul-Lez added 2 commits January 16, 2023 12:17

added key result

c94ebe4

Upadte results

f97552a

Paul-Lez added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. and removed WIP Work in progress labels Jan 17, 2023

riccardobrasca reviewed Jan 17, 2023

View reviewed changes

riccardobrasca approved these changes Jan 17, 2023

View reviewed changes

src/field_theory/minpoly/gcd_monoid.lean Outdated Show resolved Hide resolved

Paul-Lez added 2 commits January 17, 2023 18:01

Last few modifications

1a21901

Fixed lint error

f26f977

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jan 17, 2023

bors bot changed the title ~~feat(ring_theory/*): generalise minpoly.dvd to integrally closed rings~~ [Merged by Bors] - feat(ring_theory/*): generalise minpoly.dvd to integrally closed rings Jan 18, 2023

bors bot closed this Jan 18, 2023

bors bot deleted the preliminary_ring_theory_PR branch January 18, 2023 01:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings #18021

[Merged by Bors] - feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings #18021

Paul-Lez commented Dec 29, 2022 •

edited

Loading

Paul-Lez commented Dec 29, 2022

ericrbg left a comment

riccardobrasca left a comment

ericrbg commented Dec 30, 2022

riccardobrasca commented Dec 30, 2022

riccardobrasca Dec 31, 2022

Paul-Lez Jan 4, 2023 •

edited

Loading

riccardobrasca commented Jan 11, 2023

mathlib-dependent-issues-bot commented Jan 14, 2023

riccardobrasca commented Jan 15, 2023

Paul-Lez commented Jan 15, 2023

riccardobrasca Jan 17, 2023

Paul-Lez Jan 17, 2023

alreadydone Jan 17, 2023

Paul-Lez Jan 17, 2023

Paul-Lez Jan 17, 2023

riccardobrasca Jan 17, 2023

riccardobrasca commented Jan 17, 2023

bors bot commented Jan 17, 2023

Paul-Lez commented Jan 17, 2023

bors bot commented Jan 18, 2023

[Merged by Bors] - feat(ring_theory/*): generalise minpoly.dvd to integrally closed rings #18021

[Merged by Bors] - feat(ring_theory/*): generalise minpoly.dvd to integrally closed rings #18021

Conversation

Paul-Lez commented Dec 29, 2022 • edited Loading

Paul-Lez commented Dec 29, 2022

ericrbg left a comment

Choose a reason for hiding this comment

riccardobrasca left a comment

Choose a reason for hiding this comment

ericrbg commented Dec 30, 2022

riccardobrasca commented Dec 30, 2022

riccardobrasca Dec 31, 2022

Choose a reason for hiding this comment

Paul-Lez Jan 4, 2023 • edited Loading

Choose a reason for hiding this comment

riccardobrasca commented Jan 11, 2023

mathlib-dependent-issues-bot commented Jan 14, 2023

riccardobrasca commented Jan 15, 2023

Paul-Lez commented Jan 15, 2023

riccardobrasca Jan 17, 2023

Choose a reason for hiding this comment

Paul-Lez Jan 17, 2023

Choose a reason for hiding this comment

alreadydone Jan 17, 2023

Choose a reason for hiding this comment

Paul-Lez Jan 17, 2023

Choose a reason for hiding this comment

Paul-Lez Jan 17, 2023

Choose a reason for hiding this comment

riccardobrasca Jan 17, 2023

Choose a reason for hiding this comment

riccardobrasca commented Jan 17, 2023

bors bot commented Jan 17, 2023

Paul-Lez commented Jan 17, 2023

bors bot commented Jan 18, 2023

[Merged by Bors] - feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings #18021

[Merged by Bors] - feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings #18021

Paul-Lez commented Dec 29, 2022 •

edited

Loading

Paul-Lez Jan 4, 2023 •

edited

Loading