[Merged by Bors] - feat(field_theory/tower): tower law #3355
Conversation
kckennylau
commented
Jul 10, 2020
kckennylau
commented
src/field_theory/tower.lean
Outdated
| open is_algebra_tower | ||
|
|
||
| theorem smul_mem_span_smul_of_mem {s : set S} {t : set A} {k : S} (hks : k ∈ span R s) | ||
| {x : A} (hx : x ∈ t) : k • x ∈ span R (s • t) := |
There was a problem hiding this comment.
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.
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.
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 of is_basis.smul.
There was a problem hiding this comment.
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.
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.
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.
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.
Presumably those lemmas should just be in ring_theory/algebra_tower.
There was a problem hiding this comment.
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?
|
|
||
| namespace finite_dimensional | ||
|
|
||
| theorem trans [finite_dimensional F K] [finite_dimensional K A] : finite_dimensional F A := |
There was a problem hiding this comment.
Do we have something like this already for restrict_scalars? Could that be reused here?
There was a problem hiding this comment.
what is the name of the theorem?
There was a problem hiding this comment.
I think we don't have it yet.
There was a problem hiding this comment.
I was thinking of something like
variables (V : Type*) [add_comm_group V] [vector_space K V]
theorem trans' [finite_dimensional F K] [finite_dimensional K V] :
finite_dimensional F (module.restrict_scalars F K V) :=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.
this is precisely what algebra_tower aims to deprecate. btw what I proved implies what you want, after I've made an instance is_algebra_tower F K V (oh and after I've generalized is_algebra_tower to has_scalar)
There was a problem hiding this comment.
Aah right... I forgot that this should really be done for is_scalar_tower 😉 Yup, that's better!
src/field_theory/tower.lean
Outdated
| open is_algebra_tower | ||
|
|
||
| theorem smul_mem_span_smul_of_mem {s : set S} {t : set A} {k : S} (hks : k ∈ span R s) | ||
| {x : A} (hx : x ∈ t) : k • x ∈ span R (s • t) := |
There was a problem hiding this comment.
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.
src/field_theory/tower.lean
Outdated
| open is_algebra_tower | ||
|
|
||
| theorem smul_mem_span_smul_of_mem {s : set S} {t : set A} {k : S} (hks : k ∈ span R s) | ||
| {x : A} (hx : x ∈ t) : k • x ∈ span R (s • t) := |
There was a problem hiding this comment.
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?
Co-authored-by: Johan Commelin <johan@commelin.net>
robertylewis
added
the
awaiting-author
kckennylau
added
the
awaiting-review
bryangingechen
removed
the
awaiting-author
|
bors d+ |
|
✌️ kckennylau can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
semorrison
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
