Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(field_theory/intermediate_field): dsimp lemma #15188

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat(field_theory/intermediate_field): dsimp lemma #15188

wants to merge 6 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Jul 8, 2022 •
edited by github-actions bot

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Jul 8, 2022
@YaelDillies YaelDillies mentioned this pull request Jul 8, 2022
Open
2 tasks
@eric-wieser
Copy link
Member

It's not immediately clear to me that these are good simp lemmas; do we have anything comparable for other subobjects?

In particular, simplifying map to set.image means that you lose the fact the subtype is closed under multiplication.

@YaelDillies
Copy link
Collaborator Author

I am not sure about ↥(S.map f) = ↥(f '' S), but I am sure we want ↥(↑E : intermediate_field K L) = ↥E because it's a clear simplification of the type, and indeed #13307 needs this lemma.

@eric-wieser
Copy link
Member

Those coercions seem bizarre to me anyway; I guess that's the same as having a lemma for ↥(S.restrict_scalars R') = ↥S' for S : subalgebra R A`? Do we already have that lemma?

@eric-wieser
Copy link
Member

eric-wieser commented Jul 8, 2022 •
edited

I'm going to make a PR to remove lift2 in favor of restrict_scalars... (edit: #15191)

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jul 10, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

YaelDillies and others added 2 commits July 14, 2022 10:27
@YaelDillies @eric-wieser
dedup mem_restrict_scalars
daa50fe 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@YaelDillies
coe_sort_map
3f76deb
@eric-wieser
Copy link
Member

I've made it so that #13307 no longer depends on this

eric-wieser
eric-wieser requested changes Jul 19, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Just to register that the only lemma in this PR that I think is worth having is coe_map; and even that I'm not sure is good as a simp lemma (as it probably gets applied before set_like.mem_coe).

@YaelDillies
Copy link
Collaborator Author

I think the difference with the similar dsimp lemmas I already PRed is that the simplified types had more instances (if X : PartialOrder, then X is a partial_order but X.to_Preorder is only a preorder) and were not type synonyms.

@YaelDillies YaelDillies changed the title feat(field_theory/intermediate_field): dsimp lemmas feat(field_theory/intermediate_field): dsimp lemma Jul 19, 2022
eric-wieser
eric-wieser reviewed Jul 19, 2022
View reviewed changes
src/field_theory/intermediate_field.lean
@@ -273,6 +273,8 @@ def map (f : L →ₐ[K] L') : intermediate_field K L' :=
neg_mem' := λ x hx, (S.to_subalgebra.map f).neg_mem hx,
.. S.to_subalgebra.map f}

@[simp] lemma coe_map (f : L →ₐ[K] L') : (S.map f : set L') = f '' S := rfl
Copy link
Member

Choose a reason for hiding this comment

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

Do we have this lemma for submodules etc already? If not, I think we should add them all at the same time, as that's a good way to verify that the lemma is safe as simp

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It's submodule.map_coe, subgroup.coe_map, submonoid.coe_map.

Copy link
Member

Choose a reason for hiding this comment

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

All of which are simp?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes.

eric-wieser
eric-wieser approved these changes Jul 20, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Thanks!

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Jul 20, 2022
bors bot pushed a commit that referenced this pull request Jul 20, 2022
@YaelDillies
feat(field_theory/intermediate_field): dsimp lemma (#15188)
4359e48
@bors
Copy link

bors bot commented Jul 20, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(field_theory/intermediate_field): dsimp lemma [Merged by Bors] - feat(field_theory/intermediate_field): dsimp lemma Jul 20, 2022
@bors bors bot closed this Jul 20, 2022
@bors bors bot deleted the intermediate_field_coe_sort branch July 20, 2022 13:20
joelriou pushed a commit that referenced this pull request Jul 23, 2022
@YaelDillies @joelriou
feat(field_theory/intermediate_field): dsimp lemma (#15188)
e6581d5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@YaelDillies @eric-wieser @mathlib-dependent-issues-bot @Vierkantor @leanprover-community-bot-assistant