Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/finsupp): lattice structure on finsupp #3335

Closed
wants to merge 30 commits into from
Closed

[Merged by Bors] - feat(data/finsupp): lattice structure on finsupp #3335

wants to merge 30 commits into from

Conversation

awainverse
Copy link
Collaborator

@awainverse awainverse commented Jul 9, 2020 •
edited by jcommelin
Loading

adds facts about order_isos respecting lattice operations
defines lattice structures on finsupps to N
constructs an order_iso out of finsupp.to_multiset

@awainverse awainverse mentioned this pull request Jul 9, 2020
Closed
@jcommelin jcommelin changed the title Finsupp lattice feat(data/finsupp): lattice structure on finsupp Jul 9, 2020
jcommelin
jcommelin reviewed Jul 9, 2020
View reviewed changes
src/data/finsupp.lean Outdated Show resolved Hide resolved
src/data/finsupp.lean Outdated Show resolved Hide resolved
@robertylewis robertylewis added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 9, 2020
jcommelin
jcommelin reviewed Jul 14, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

The changes on order embeddings seem uncontroversial. If you want to get them merged, you could split them into another PR.
The part on lattice structure on finsupp still needs some polishing. I'm sorry that I don't have a good suggestion... I'll try to think more about it, but I'm quite busy. All I know right now, is that it feels like there is some abstraction right around the corner, and we should try to figure out what it is.

src/order/order_iso.lean Outdated Show resolved Hide resolved
src/order/order_iso.lean Outdated Show resolved Hide resolved
src/order/order_iso.lean Outdated Show resolved Hide resolved
src/order/order_iso.lean Outdated Show resolved Hide resolved
@awainverse awainverse removed the request for review from semorrison July 14, 2020 22:42
@robertylewis
Copy link
Member

I see this is blocking a few other PRs. Is it ready for review once the build is fixed?

@awainverse
Copy link
Collaborator Author

Yeah, I'm getting back to making this build today, and then it should be reviewable. Unfortunately I've had some recurrent olean problems, so it's been hard for me to even code on this.

@semorrison
Copy link
Collaborator

Just in case you're having trouble building --- this currently builds fine for me, giving the same error as reported by CI. Let us know on zulip if you're having trouble with oleans.

@awainverse awainverse 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 Jul 22, 2020
@bryangingechen
Copy link
Collaborator

Do you mind running git merge origin/master into this branch to fix the crazy diff on GitHub? The remaining linter errors are unused arguments: https://github.com/leanprover-community/mathlib/pull/3335/checks?check_run_id=897104215#step:5:12

@robertylewis robertylewis 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 Jul 22, 2020
@awainverse
Copy link
Collaborator Author

Looks good. Lots of minor comments, but overall looks sound.

Could you add that finsupp.to_fun is monotone?

I've added that, and also added an order_embedding version of it.

@awainverse awainverse 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 Jul 25, 2020
semorrison
semorrison reviewed Jul 25, 2020
View reviewed changes
src/data/finsupp/lattice.lean Outdated

variable [partial_order β]

/-- The order on `finsupp`s over a partial order-embeds into that on functions -/
Copy link
Collaborator

Choose a reason for hiding this comment

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

Garbled?

@semorrison
Copy link
Collaborator

Looks good --- one last doc-string request, and then you can hit merge. Thanks!

bors d+

@bors
Copy link

bors bot commented Jul 25, 2020

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

@semorrison semorrison added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 25, 2020
@awainverse
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Jul 25, 2020
@awainverse @bryangingechen
feat(data/finsupp): lattice structure on finsupp (#3335)
2d29f80 
adds facts about order_isos respecting lattice operations
defines lattice structures on finsupps to N
constructs an order_iso out of finsupp.to_multiset



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

bors bot commented Jul 25, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/finsupp): lattice structure on finsupp [Merged by Bors] - feat(data/finsupp): lattice structure on finsupp Jul 25, 2020
@bors bors bot closed this Jul 25, 2020
@bors bors bot deleted the finsupp_lattice branch July 25, 2020 06:32
@YaelDillies YaelDillies mentioned this pull request Dec 25, 2021
Closed
bors bot pushed a commit that referenced this pull request Dec 26, 2021
@YaelDillies
split(data/finsupp/order): Split off data.finsupp.basic (#11045)
f72ff5c 
This moves all order instances about `finsupp` from `data.finsupp.basic` and `data.finsupp.lattice` to a new file `data.finsupp.order`.

I'm crediting
* Johan for #1216, #1244
* Aaron Anderson for #3335
bors bot pushed a commit that referenced this pull request Dec 27, 2021
@YaelDillies
split(data/finsupp/order): Split off data.finsupp.basic (#11045)
ca2c344 
This moves all order instances about `finsupp` from `data.finsupp.basic` and `data.finsupp.lattice` to a new file `data.finsupp.order`.

I'm crediting
* Johan for #1216, #1244
* Aaron Anderson for #3335
erdOne pushed a commit that referenced this pull request Jan 1, 2022
@YaelDillies @erdOne
split(data/finsupp/order): Split off data.finsupp.basic (#11045)
25835df 
This moves all order instances about `finsupp` from `data.finsupp.basic` and `data.finsupp.lattice` to a new file `data.finsupp.order`.

I'm crediting
* Johan for #1216, #1244
* Aaron Anderson for #3335
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@semorrison semorrison semorrison left review comments

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@awainverse @robertylewis @semorrison @bryangingechen @jcommelin