feat(linear_algebra/finite_dimensional): finite dimensional vector spaces #1241
Conversation
|
|
||
| namespace finite_dimensional | ||
|
|
||
| lemma finite_of_linear_independent {ι : Type w} [decidable_eq V] [decidable_eq ι] |
There was a problem hiding this comment.
I think something like this is true for arbitrary noetherian modules, right. How much of this file can be done in the general setting?
There was a problem hiding this comment.
I don't think it is true, though I can't think of a counter example. Just because a submodule has a finite basis doesn't necessarily mean that every basis for that submodule is finite? Otherwise why is the definition of noetherian not just that the module is finitely generated, rather than every submodule? I'd be interested to know the counterexample.
There was a problem hiding this comment.
If you have an infinite basis you can create an infinite increasing chain of submodules:
span {v_1} \subset span {v_1, v_2} \subset ...
this contradicts being noetherian.
There was a problem hiding this comment.
Of course. This is quite a hard proof.
There was a problem hiding this comment.
Generalized to noetherian modules
|
|
||
| Definition and basic properties of finite dimensional vector spaces. | ||
|
|
||
| The class `finite_dimensional` is defined to be `is_noetherian`, for ease of transfer of proofs. |
There was a problem hiding this comment.
It might be a bit awkward at first, but shouldn't we just use is_noetherian? (Just like we shouldn't have vector_space in the first place.
@digama0 What do you think? Should this be a reducible def? Or an abbreviation? Or should it not be there at all?
There was a problem hiding this comment.
This is slightly different than how it's done with vector spaces. It's a reducible der, so you shouldn't have to define an instance when there's already an is_noetherian instance floating around.
There was a problem hiding this comment.
If we do use is_noetherian there definitely should be clear documentation of this somewhere, so people know where to look for finite dimensional vector spaces
jcommelin
added
the
ready-to-merge
…aces (leanprover-community#1241) * feat(linear_algebra/finite_dimensional): finite dimensional vector spaces * rw `of_span_finite_eq_top` to `of_fg` * prove infinite.nat_embedding * generalize finite_of_linear_independent to noetherian modules * fix build * fix build (ring_theory/polynomial)
Finite dimensional vector spaces and their properties. Finite dimensional is a proposition, and defined to be
is_noetherian, with a more sensible constructor providedof_span_finite_eq_top.There was some discussion about having a non Prop valued definition demanding an explicit basis. The downside to that is that there may well be diamonds, which is why I chose to make a Prop definition. Maybe the constructive version should exist as well.
Some of the proofs are very high powered. I use very general theorems about cardinals, and noetherian rings.
Even
principal_ideal_domainis mentioned (the instance to provefieldimpliesis_noetherianis viaeuclidean_domainandprincipal_ideal_domain). Not sure if this is a problem.TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list