[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime #6924

atarnoam · 2021-03-28T17:02:38Z

ideal_inter_nonempty: the intersection of any two ideals is nonempty. A preorder with joins and this property satisfies that its ideal poset is a lattice.
An ideal is prime iff x \inf y \in I implies x \in I or y \in I.
A maximal ideal in a distributive lattice is prime.

depends on: [Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added is_ideal, is_pfilter, is_prime, is_maximal, prime_pair #6656

While proving that a maximal ideal in a distributive lattice is prime, I've noticed a problem.
I wanted to use the sup of two ideals, however in the current implementation this requires P to have a bottom element!
What is going on here is that to prove that the sup ideal is nonempty, it suffices to use only the fact that the intersection of any two ideals is nonempty. This is true for both the case where P has bot, and for when P has infs.
Thus we can define this property separately and show that it is true for these two cases.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

…rime_ideal

… into prime_ideal

…rime_ideal

… into prime_ideal

Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>

To show that `ideal P` is a lattice, it now suffices to check that `P` has joins and that the intersection of any two ideals is nonempty. Also added an equivalent characteristic of the join ideal when `P` is a lattice.

… into prime_ideal

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

jcommelin

This is not really my area of expertise. So I'm just commenting on style.

src/order/ideal.lean

src/order/pfilter.lean

src/order/ideal.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

mguaypaq

Sorry for the delay in reviewing, and thank you for this nice addition. I especially like your ideal_inter_nonempty, because I've wanted something like it before. As you noted, there are two natural and unrelated settings where this property holds (the two instances of it you define), and I don't think there's a better abstraction which covers both.

As always, I've tried to be somewhat thorough, so this review includes many comments, but most of them are minor changes due to the mathlib naming conventions and style guide.

src/order/ideal.lean

src/order/prime_ideal.lean

mguaypaq · 2021-04-09T18:33:53Z

src/order/prime_ideal.lean

+variables {I : ideal P}
+
+@[priority 100]
+instance is_maximal.is_prime [is_maximal I] : is_prime I :=


For such a nice theorem, and the main point of this PR, it's almost too bad that the statement is so unassuming!

mguaypaq

This PR seems fine to me, but a maintainer will have to poke bors so it can be merged.

awainverse · 2021-04-12T19:21:58Z

I think the ready-to-merge label indicates that a maintainer has already told bors to merge it, and that it's about to merge

bryangingechen · 2021-04-13T23:32:09Z

Looks like there's just one docstring suggestion left.

By the way, @atarnoam the way we've been doing reviews here, the author usually marks suggestions / conversations as "Resolved" if they've been addressed by commits or if the conversation has ended. This makes it easier for later reviewers to see at a glance what remains to be done.

@awainverse any final thoughts on this?

Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>

bryangingechen · 2021-04-14T18:56:47Z

Thanks!
bors r+

…er_nonempty`, proved that a maximal ideal is prime (#6924) - `ideal_inter_nonempty`: the intersection of any two ideals is nonempty. A preorder with joins and this property satisfies that its ideal poset is a lattice. - An ideal is prime iff `x \inf y \in I` implies `x \in I` or `y \in I`. - A maximal ideal in a distributive lattice is prime.

bors · 2021-04-15T03:49:03Z

Pull request successfully merged into master.

Build succeeded:

atarnoam and others added 30 commits March 12, 2021 16:42

feat(order/ideal) added is_prime and is_maximal ideals

367ba3a

Update src/order/ideal.lean

fa268b1

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Update src/order/ideal.lean

ad910d6

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Update src/order/ideal.lean

79b765d

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Update src/order/ideal.lean

4d2b2da

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Update src/order/ideal.lean

0ff4f09

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Update src/order/ideal.lean

6e472a5

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Update src/order/ideal.lean

c6d2b3d

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

starting to work on is_prime_of_is_maximal

ae380c3

Update ideal.lean

663f793

Merge remote-tracking branch 'refs/remotes/origin/prime_ideal' into p…

d6076c7

…rime_ideal

Merge branch 'prime_ideal' of github.com:leanprover-community/mathlib…

3e76e40

… into prime_ideal

Update ideal.lean

3217ff6

fixed bugs

2be706e

Merge remote-tracking branch 'refs/remotes/origin/prime_ideal' into p…

9cd7320

…rime_ideal

Update ideal.lean

e0c3590

Update ideal.lean

7cb44dc

removed prime_of_is_maximal

f6a3300

Merge branch 'prime_ideal' of github.com:leanprover-community/mathlib…

2d337d8

… into prime_ideal

Update src/order/ideal.lean

ed01b5f

Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>

Made the lattice instance of I more general.

8c597f1

To show that `ideal P` is a lattice, it now suffices to check that `P` has joins and that the intersection of any two ideals is nonempty. Also added an equivalent characteristic of the join ideal when `P` is a lattice.

Changed proper to is_proper

472ebac

Merge branch 'prime_ideal' of github.com:leanprover-community/mathlib…

e63fe2b

… into prime_ideal

is_prime, is_maximal now extend is_proper.

926c4ed

made is_maximal and is_prime to typeclasses.

8fc4dcf

Update src/order/ideal.lean

1d1dbfe

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Update src/order/ideal.lean

6bab0df

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

added is_ideal, is_filter, prime_pair

7813092

Merge branch 'prime_ideal' into is_prime_of_is_maximal

e3a09e8

Update prime_ideal.lean

52ae523

jcommelin reviewed Apr 6, 2021

View reviewed changes

src/order/ideal.lean Outdated Show resolved Hide resolved

src/order/pfilter.lean Outdated Show resolved Hide resolved

src/order/ideal.lean Outdated Show resolved Hide resolved

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 Apr 6, 2021

atarnoam and others added 2 commits April 8, 2021 21:43

Update src/order/ideal.lean

1d2bf9b

Co-authored-by: Johan Commelin <johan@commelin.net>

changed mem_def to mem_coe

667a4a2

atarnoam 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 labels Apr 8, 2021

mguaypaq reviewed Apr 9, 2021

View reviewed changes

mguaypaq 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 Apr 11, 2021

atarnoam added 2 commits April 11, 2021 15:02

applied CR

06ac08d

applied CR

a028592

atarnoam 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 labels Apr 11, 2021

mguaypaq approved these changes Apr 12, 2021

View reviewed changes

mguaypaq added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 12, 2021

awainverse added awaiting-review The author would like community review of the PR and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Apr 12, 2021

Update src/order/ideal.lean

b91a965

Co-authored-by: Mathieu Guay-Paquet <mathieu.guaypaquet@gmail.com>

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 14, 2021

bors bot closed this Apr 15, 2021

bors bot deleted the is_prime_of_is_maximal branch April 15, 2021 03:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime #6924

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime #6924

atarnoam commented Mar 28, 2021 •

edited by bryangingechen

jcommelin left a comment

mguaypaq left a comment

mguaypaq Apr 9, 2021

mguaypaq left a comment •

edited

awainverse commented Apr 12, 2021

bryangingechen commented Apr 13, 2021

bryangingechen commented Apr 14, 2021

bors bot commented Apr 15, 2021

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added ideal_inter_nonempty, proved that a maximal ideal is prime #6924

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added ideal_inter_nonempty, proved that a maximal ideal is prime #6924

Conversation

atarnoam commented Mar 28, 2021 • edited by bryangingechen

jcommelin left a comment

Choose a reason for hiding this comment

mguaypaq left a comment

Choose a reason for hiding this comment

mguaypaq Apr 9, 2021

Choose a reason for hiding this comment

mguaypaq left a comment • edited

Choose a reason for hiding this comment

awainverse commented Apr 12, 2021

bryangingechen commented Apr 13, 2021

bryangingechen commented Apr 14, 2021

bors bot commented Apr 15, 2021

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime #6924

[Merged by Bors] - feat(order/ideal, order/pfilter, order/prime_ideal): added `ideal_inter_nonempty`, proved that a maximal ideal is prime #6924

atarnoam commented Mar 28, 2021 •

edited by bryangingechen

mguaypaq left a comment •

edited