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
Closed
Closed
Changes from all commits
Commits
Show all changes
7 commits
Select commit
Hold shift + click to select a range
030aeaa
feat(field_theory/tower): tower law
kckennylau 010361f
make lint happy
kckennylau efa3457
make lint happy
kckennylau 7a57cd3
Update src/linear_algebra/basis.lean
kckennylau 1be6215
fix errors
kckennylau 1d2bf29
verbose
kckennylau d9ffe18
move lemmas, rewrite module docs
semorrison File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,79 @@ | ||
/- | ||
Copyright (c) 2020 Kenny Lau. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Kenny Lau | ||
-/ | ||
|
||
import ring_theory.algebra_tower | ||
import linear_algebra.finite_dimensional | ||
|
||
/-! | ||
# Tower of field extensions | ||
|
||
In this file we prove the tower law for arbitrary extensions and finite extensions. | ||
Suppose `L` is a field extension of `K` and `K` is a field extension of `F`. | ||
Then `[L:F] = [L:K] [K:F]` where `[E₁:E₂]` means the `E₂`-dimension of `E₁`. | ||
|
||
In fact we generalize it to algebras, where `L` is not necessarily a field, but just a `K`-algebra. | ||
|
||
## Implementation notes | ||
|
||
We prove two versions, since there are two notions of dimensions: `vector_space.dim` which gives | ||
the dimension of an arbitrary vector space as a cardinal, and `finite_dimensional.findim` which | ||
gives the dimension of a finitely-dimensional vector space as a natural number. | ||
|
||
## Tags | ||
|
||
tower law | ||
|
||
-/ | ||
|
||
universes u v w u₁ v₁ w₁ | ||
open_locale classical big_operators | ||
|
||
section field | ||
|
||
open cardinal | ||
|
||
variables (F : Type u) (K : Type v) (A : Type w) | ||
variables [field F] [field K] [ring A] | ||
variables [algebra F K] [algebra K A] [algebra F A] [is_algebra_tower F K A] | ||
|
||
/-- Tower law: if `A` is a `K`-algebra and `K` is a field extension of `F` then | ||
`dim_F(A) = dim_F(K) * dim_K(A)`. -/ | ||
theorem dim_mul_dim' : | ||
(cardinal.lift.{v w} (vector_space.dim F K) * | ||
cardinal.lift.{w v} (vector_space.dim K A) : cardinal.{max w v}) = | ||
cardinal.lift.{w v} (vector_space.dim F A) := | ||
let ⟨b, hb⟩ := exists_is_basis F K, ⟨c, hc⟩ := exists_is_basis K A in | ||
by rw [← (vector_space.dim F K).lift_id, ← hb.mk_eq_dim, | ||
← (vector_space.dim K A).lift_id, ← hc.mk_eq_dim, | ||
← lift_umax.{w v}, ← (hb.smul hc).mk_eq_dim, mk_prod, lift_mul, | ||
lift_lift, lift_lift, lift_lift, lift_lift, lift_umax] | ||
|
||
/-- Tower law: if `A` is a `K`-algebra and `K` is a field extension of `F` then | ||
`dim_F(A) = dim_F(K) * dim_K(A)`. -/ | ||
theorem dim_mul_dim (F : Type u) (K A : Type v) [field F] [field K] [ring A] | ||
[algebra F K] [algebra K A] [algebra F A] [is_algebra_tower F K A] : | ||
vector_space.dim F K * vector_space.dim K A = vector_space.dim F A := | ||
by convert dim_mul_dim' F K A; rw lift_id | ||
|
||
namespace finite_dimensional | ||
|
||
theorem trans [finite_dimensional F K] [finite_dimensional K A] : finite_dimensional F A := | ||
let ⟨b, hb⟩ := finite_dimensional.exists_is_basis_finset F K in | ||
let ⟨c, hc⟩ := finite_dimensional.exists_is_basis_finset K A in | ||
finite_dimensional.of_finite_basis $ hb.smul hc | ||
|
||
/-- Tower law: if `A` is a `K`-algebra and `K` is a field extension of `F` then | ||
`dim_F(A) = dim_F(K) * dim_K(A)`. -/ | ||
theorem findim_mul_findim [finite_dimensional F K] [finite_dimensional K A] : | ||
findim F K * findim K A = findim F A := | ||
let ⟨b, hb⟩ := finite_dimensional.exists_is_basis_finset F K in | ||
let ⟨c, hc⟩ := finite_dimensional.exists_is_basis_finset K A in | ||
by rw [findim_eq_card_basis hb, findim_eq_card_basis hc, | ||
findim_eq_card_basis (hb.smul hc), fintype.card_prod] | ||
|
||
end finite_dimensional | ||
|
||
end field |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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.
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!