Skip to content

[Merged by Bors] - feat(RingTheory/TwoSidedIdeal): add lattice structure to two-sided-ideals#14456

Closed
jjaassoonn wants to merge 13 commits intomasterfrom
zjj/twosidedIdeal-lattice
Closed

[Merged by Bors] - feat(RingTheory/TwoSidedIdeal): add lattice structure to two-sided-ideals#14456
jjaassoonn wants to merge 13 commits intomasterfrom
zjj/twosidedIdeal-lattice

Conversation

@jjaassoonn
Copy link
Copy Markdown
Collaborator

@jjaassoonn jjaassoonn commented Jul 5, 2024

Open in Gitpod

@jjaassoonn jjaassoonn added awaiting-review t-algebra Algebra (groups, rings, fields, etc) help-wanted The author needs attention to resolve issues labels Jul 5, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 5, 2024 •
edited
Loading

PR summary 5863cc672d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.TwoSidedIdeal.Lattice 571

Declarations diff

+ bot_ringCon
+ iInf_ringCon
+ iSup_ringCon
+ inf_ringCon
+ instance : Bot (TwoSidedIdeal R)
+ instance : CompleteLattice (TwoSidedIdeal R)
+ instance : CompleteSemilatticeInf (TwoSidedIdeal R)
+ instance : CompleteSemilatticeSup (TwoSidedIdeal R)
+ instance : Inf (TwoSidedIdeal R)
+ instance : InfSet (TwoSidedIdeal R)
+ instance : SemilatticeInf (TwoSidedIdeal R)
+ instance : SemilatticeSup (TwoSidedIdeal R)
+ instance : Sup (TwoSidedIdeal R)
+ instance : SupSet (TwoSidedIdeal R)
+ instance : Top (TwoSidedIdeal R)
+ mem_bot
+ mem_iInf
+ mem_inf
+ mem_sInf
+ mem_sup
+ mem_sup_left
+ mem_sup_right
+ orderIsoRingCon
+ ringCon_injective
+ ringCon_le_iff
+ sInf_ringCon
+ sSup_ringCon
+ sup_ringCon
+ top_ringCon

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

jjaassoonn
jjaassoonn commented Jul 5, 2024
View reviewed changes
@jjaassoonn jjaassoonn removed the help-wanted The author needs attention to resolve issues label Jul 5, 2024
@jjaassoonn
Copy link
Copy Markdown
Collaborator Author

jjaassoonn commented Jul 5, 2024

I didn't use Function.Injective.completeLattice is to avoid instance diamond between SetLike.instPartialOrder and CompleteLattice.instPartialOrder

@jjaassoonn jjaassoonn mentioned this pull request Jul 5, 2024
Closed
1 task
eric-wieser
eric-wieser reviewed Jul 5, 2024
View reviewed changes
eric-wieser
eric-wieser reviewed Jul 5, 2024
View reviewed changes
eric-wieser
eric-wieser reviewed Jul 5, 2024
View reviewed changes
Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
Comment on lines +106 to +109
__ := (inferInstance : SemilatticeSup (TwoSidedIdeal R))
__ := (inferInstance : SemilatticeInf (TwoSidedIdeal R))
__ := (inferInstance : CompleteSemilatticeSup (TwoSidedIdeal R))
__ := (inferInstance : CompleteSemilatticeInf (TwoSidedIdeal R))
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Jul 5, 2024

Choose a reason for hiding this comment

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

I suspect you can drop these and Lean works it out automatically?

Copy link
Copy Markdown
Collaborator Author

@jjaassoonn jjaassoonn Jul 6, 2024

Choose a reason for hiding this comment

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

unfortunately not. Lean complains

fields missing: 'inf_le_left', 'inf_le_right', 'le_inf', 'le_sSup', 'sSup_le', 'sInf_le', 'le_sInf'

eric-wieser
eric-wieser reviewed Jul 5, 2024
View reviewed changes
@jjaassoonn jjaassoonn added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jul 6, 2024
jjaassoonn and others added 6 commits July 6, 2024 12:30
@jjaassoonn @eric-wieser
Update Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
58aa16f 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@jjaassoonn
Merge remote-tracking branch 'origin/master' into zjj/twosidedIdeal-l…
f9f38e7 
…attice
@jjaassoonn
Merge branch 'zjj/twosidedIdeal-lattice' of https://github.com/leanpr…
045af87 
…over-community/mathlib4 into zjj/twosidedIdeal-lattice
@jjaassoonn
add lemma
899b348
@jjaassoonn @github-actions
Update Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
4cf212a 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jjaassoonn @github-actions
Update Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
94824ba 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@jjaassoonn jjaassoonn added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jul 6, 2024
jjaassoonn
jjaassoonn commented Jul 6, 2024
View reviewed changes
kbuzzard
kbuzzard approved these changes Jul 7, 2024
View reviewed changes
@jjaassoonn @kbuzzard
Apply suggestions from code review
1f0796d 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@jjaassoonn jjaassoonn mentioned this pull request Jul 8, 2024
Closed
1 task
@jjaassoonn jjaassoonn requested a review from eric-wieser July 8, 2024 23:07
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jul 14, 2024

I am busy until Wednesday, but I can have a look later.

@jjaassoonn
Copy link
Copy Markdown
Collaborator Author

jjaassoonn commented Jul 14, 2024

I am busy until Wednesday, but I can have a look later.

No rush! Thank you very much!

riccardobrasca
riccardobrasca approved these changes Jul 16, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

LGTM, thanks!

@eric-wieser there is still a question for you :)

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Jul 16, 2024

I have a big question: why aren't we just pulling the entire CompleteLattice structure (aside from the LE, which comes via the SetLike instance) through the order isomorphism all at once? Is that not easily doable?

@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 16, 2024
@jjaassoonn
Copy link
Copy Markdown
Collaborator Author

jjaassoonn commented Jul 16, 2024

I have a big question: why aren't we just pulling the entire CompleteLattice structure (aside from the LE, which comes via the SetLike instance) through the order isomorphism all at once? Is that not easily doable?

Because pulling back the order of ringcon results in a diamond: the “smaller than” from the pulling back is not definitionally equal to that from setlike instance

@jjaassoonn jjaassoonn removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 16, 2024
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Jul 17, 2024

Right, but I'm talking about leaving the existing order alone and pulling the rest back.

@jjaassoonn
Copy link
Copy Markdown
Collaborator Author

jjaassoonn commented Jul 17, 2024

Right, but I'm talking about leaving the existing order alone and pulling the rest back.

Ah, I tried this as well. Lean will complain about the diamond (this is how I discovered it), so we need to reprove all the axiom anyway.

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Jul 17, 2024

Sounds like we want a CompleteLattice.replacePartialOrder declaration marked as reducible for things like this. But that's for a separate PR, so I'll leave this alone.

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Jul 17, 2024

I addressed the comment directed at Eric (I think satisfactorily), and given that there are two other approving reviews:

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 17, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 17, 2024
@jjaassoonn
feat(RingTheory/TwoSidedIdeal): add lattice structure to two-sided-id…
7269094 
…eals (#14456)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/TwoSidedIdeal): add lattice structure to two-sided-ideals [Merged by Bors] - feat(RingTheory/TwoSidedIdeal): add lattice structure to two-sided-ideals Jul 17, 2024
@mathlib-bors mathlib-bors bot closed this Jul 17, 2024
@mathlib-bors mathlib-bors bot deleted the zjj/twosidedIdeal-lattice branch July 17, 2024 08:03
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

@kbuzzard kbuzzard kbuzzard approved these changes

@riccardobrasca riccardobrasca riccardobrasca approved these changes

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@jjaassoonn @riccardobrasca @j-loreaux @eric-wieser @kbuzzard @kim-em