Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.
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
[Merged by Bors] - feat(field_theory/tower): tower law #3355
[Merged by Bors] - feat(field_theory/tower): tower law #3355
Changes from 3 commits
030aeaa
010361f
efa3457
7a57cd3
1be6215
1d2bf29
d9ffe18
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I this and the next few lemmas specific to towers? They look like they should be moved to earlier files.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
tbh the whole import hierarchy is a bit messy. maybe algebera_tower should occupy a very low position in the import hierarchy (i.e. imported by a lot of files) and this file should not exist at all.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I wanted to put the lemmas in this file because they use the
span R s = ⊤
assumption, so they're directly related to the spanning part ofis_basis.smul
.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think I agree with Patrick.
If the import hierarchy is messy, we better clean it up, before adding stuff and (potentially) making it harder to untangle later on.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So if you have an idea how to improve the import situation, I would be really happy with a refactor PR after this one. What do you think?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you agree, I suggest that we merge this like it is, but then take a step back to refactor things a bit, and untangle the import hierarchy.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
sure
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This conversation sounded like an agreement to punt on this one, with everyone agreeing that they don't really feel like refactoring. Can't we just move these lemmas earlier, as @PatrickMassot suggested?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Presumably those lemmas should just be in
ring_theory/algebra_tower
.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Okay, I just did it myself.
I also added a module-doc to
ring_theory/algebra_tower
, and explained the division of the material between the two files. @kckennylau, could you check if I said anything stupid?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we have something like this already for
restrict_scalars
? Could that be reused here?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
what is the name of the theorem?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we don't have it yet.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was thinking of something like
But maybe this requires extra glue and congruence lemmas. If so, guess we would need those anyway, but maybe not in this PR.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this is precisely what
algebra_tower
aims to deprecate. btw what I proved implies what you want, after I've made an instanceis_algebra_tower F K V
(oh and after I've generalizedis_algebra_tower
tohas_scalar
)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Aah right... I forgot that this should really be done for
is_scalar_tower
😉 Yup, that's better!