[Merged by Bors] - feat(LinearAlgebra): the Erdős-Kaplansky theorem #9159
Conversation
alreadydone
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
added
the
merge-conflict
| refine Finset.sum_eq_zero fun i hi ↦ ?_ | ||
| replace eq0 := congr_arg L.subtype (congr_fun eq0 ⟨i, hi⟩) | ||
| rw [Finset.sum_apply, map_sum] at eq0 | ||
| have : SMulCommClass Lᵐᵒᵖ K K := ⟨fun _ _ _ ↦ mul_assoc _ _ _⟩ |
There was a problem hiding this comment.
Shouldn't this SMulCommClass exist somewhere in mathlib? either as an instance, or at least
as something that can be invoked right away?
There was a problem hiding this comment.
The action of Lᵐᵒᵖ on K is itself obtained manually earlier in the proof rather than automatically:
letI := Module.compHom K (RingHom.op L.subtype)
So we can't expect Lean to know about the SMulCommClass here. I think mathlib currently lack actions by MulOpposite of subobjects and it feels like a big project to add them all, although actions by subobjects of MulOpposite should already be obtainable via typeclass inference, but we seem to be lacking a Subring analogue of Subgroup.op.
| rw [e.rank_eq, e.toEquiv.cardinal_eq] | ||
| apply rank_pi_infinite | ||
|
|
||
| theorem lift_rank_lt_rank_dual' {V : Type v} [AddCommGroup V] [Module K V] |
There was a problem hiding this comment.
(untested) can this theorem be proved as a lt_of_le_of_lt from a general lift_le type lemma, and the Erdös-Kaplansky?
There was a problem hiding this comment.
I'm not sure what you have in mind? The main content of this proof is that any field K is Nontrivial, so r < 2^r ≤ #(K^r) = rank_K(K^r) (where r = Module.rank K V and the equality is by Erdös-Kaplansky).
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
alreadydone
removed
the
merge-conflict
| erw [nat_lt_lift_iff, one_lt_iff_nontrivial] | ||
| infer_instance | ||
|
|
||
| theorem lift_rank_lt_rank_dual {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] |
There was a problem hiding this comment.
Should we have versions of these last two results in the equi-universic setting, that avoid the Cardinal.lift?
Maybe they should have a ' in their name, and the results should come with docstrings that cross-ref each other.
There was a problem hiding this comment.
Certainly! No need of ', just remove lift from the names. (I use ' for the division ring version and no ' for the field version in this PR.)
|
✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
alreadydone
added
the
auto-merge-after-CI
|
As this PR is labelled bors merge |
The dimension of an infinite dimensional dual space is equal to its cardinality. As a consequence (`linearEquiv_dual_iff_finiteDimensional`), a vector space is isomorphic to its dual iff it's finite dimensional. The [main argument](https://github.com/leanprover-community/mathlib4/pull/9159/files#diff-cb173017e1157ddc4b9f868be06c18ec2a38f8cf82e856e18d59ed49f97395d8R146) is from https://mathoverflow.net/a/168624. There is a [slicker proof](https://mathoverflow.net/a/420455/3332) in the field case but Vandermonde determinants don't work in a non-commutative ring. Resolves [TODO item](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Dual.html#TODO) posed by Julian Külshammer - [x] depends on: #8941 - [x] depends on: #8942 Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
The dimension of an infinite dimensional dual space is equal to its cardinality. As a consequence (
linearEquiv_dual_iff_finiteDimensional), a vector space is isomorphic to its dual iff it's finite dimensional.The main argument is from https://mathoverflow.net/a/168624. There is a slicker proof in the field case but Vandermonde determinants don't work in a non-commutative ring.
Resolves TODO item posed by Julian Külshammer
Subfield.closure#8942