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(LinearAlgebra): the Erdős-Kaplansky theorem #9159
Changes from all commits
7b18437
5727181
1b7e850
3b260fe
f2a3978
b499365
1a241ab
a475741
86c0da5
f1dd579
e1d3048
0b0a420
b5ef4dd
aec66cb
8d7fa43
01767d9
1dc85c6
b2af569
647e529
f87fcb7
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. | |
Authors: Riccardo Brasca | ||
-/ | ||
import Mathlib.LinearAlgebra.Dimension | ||
import Mathlib.SetTheory.Cardinal.Subfield | ||
|
||
#align_import linear_algebra.free_module.rank from "leanprover-community/mathlib"@"465d4301d8da5945ef1dc1b29fb34c2f2b315ac4" | ||
|
||
|
@@ -13,6 +14,10 @@ import Mathlib.LinearAlgebra.Dimension | |
|
||
This file contains some extra results not in `LinearAlgebra.Dimension`. | ||
|
||
It also contains a proof of the Erdős-Kaplansky theorem (`rank_dual_eq_card_dual_of_aleph0_le_rank`) | ||
which says that the dimension of an infinite-dimensional dual space over a division ring | ||
has dimension equal to its cardinality. | ||
|
||
-/ | ||
|
||
|
||
|
@@ -57,6 +62,19 @@ theorem rank_finsupp_self (ι : Type w) : Module.rank R (ι →₀ R) = Cardinal | |
theorem rank_finsupp_self' {ι : Type u} : Module.rank R (ι →₀ R) = #ι := by simp | ||
#align rank_finsupp_self' rank_finsupp_self' | ||
|
||
variable {R M} | ||
theorem rank_eq_cardinal_basis {ι : Type w} (b : Basis ι R M) : | ||
Cardinal.lift.{w} (Module.rank R M) = Cardinal.lift.{v} #ι := by | ||
apply Cardinal.lift_injective.{u} | ||
simp_rw [Cardinal.lift_lift] | ||
have := b.repr.lift_rank_eq | ||
rwa [rank_finsupp_self, Cardinal.lift_lift] at this | ||
|
||
theorem rank_eq_cardinal_basis' {ι : Type v} (b : Basis ι R M) : Module.rank R M = #ι := | ||
Cardinal.lift_injective.{v} (rank_eq_cardinal_basis b) | ||
|
||
variable (R M) | ||
|
||
/-- The rank of the direct sum is the sum of the ranks. -/ | ||
@[simp] | ||
theorem rank_directSum {ι : Type v} (M : ι → Type w) [∀ i : ι, AddCommGroup (M i)] | ||
|
@@ -123,3 +141,117 @@ theorem rank_tensorProduct' (N : Type v) [AddCommGroup N] [Module R N] [Module.F | |
#align rank_tensor_product' rank_tensorProduct' | ||
|
||
end CommRing | ||
|
||
section DivisionRing | ||
|
||
variable (K : Type u) [DivisionRing K] | ||
|
||
/-- Key lemma towards the Erdős-Kaplansky theorem from https://mathoverflow.net/a/168624 -/ | ||
theorem max_aleph0_card_le_rank_fun_nat : max ℵ₀ #K ≤ Module.rank K (ℕ → K) := by | ||
have aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K) := (rank_finsupp_self K ℕ).symm.trans_le | ||
(Finsupp.lcoeFun.rank_le_of_injective <| by exact FunLike.coe_injective) | ||
refine max_le aleph0_le ?_ | ||
obtain card_K | card_K := le_or_lt #K ℵ₀ | ||
· exact card_K.trans aleph0_le | ||
by_contra! | ||
obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ℕ → K) | ||
let L := Subfield.closure (Set.range (fun i : ιK × ℕ ↦ bK i.1 i.2)) | ||
have hLK : #L < #K | ||
· refine (Subfield.cardinal_mk_closure_le_max _).trans_lt | ||
(max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩) | ||
rwa [mk_prod, ← aleph0, lift_uzero, ← rank_eq_cardinal_basis' bK, mul_aleph0_eq aleph0_le] | ||
letI := Module.compHom K (RingHom.op L.subtype) | ||
obtain ⟨⟨ιL, bL⟩⟩ := Module.Free.exists_basis (R := Lᵐᵒᵖ) (M := K) | ||
have card_ιL : ℵ₀ ≤ #ιL | ||
· contrapose! hLK | ||
haveI := @Fintype.ofFinite _ (lt_aleph0_iff_finite.mp hLK) | ||
rw [bL.repr.toEquiv.cardinal_eq, mk_finsupp_of_fintype, | ||
← MulOpposite.opEquiv.cardinal_eq] at card_K ⊢ | ||
apply power_nat_le | ||
contrapose! card_K | ||
exact (power_lt_aleph0 card_K <| nat_lt_aleph0 _).le | ||
obtain ⟨e⟩ := lift_mk_le'.mp (card_ιL.trans_eq (lift_uzero #ιL).symm) | ||
have rep_e := bK.total_repr (bL ∘ e) | ||
rw [Finsupp.total_apply, Finsupp.sum] at rep_e | ||
set c := bK.repr (bL ∘ e) | ||
set s := c.support | ||
let f i (j : s) : L := ⟨bK j i, Subfield.subset_closure ⟨(j, i), rfl⟩⟩ | ||
have : ¬LinearIndependent Lᵐᵒᵖ f := fun h ↦ by | ||
have := h.cardinal_lift_le_rank | ||
rw [lift_uzero, (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Lᵐᵒᵖ).rank_eq, | ||
rank_fun'] at this | ||
exact (nat_lt_aleph0 _).not_le this | ||
obtain ⟨t, g, eq0, i, hi, hgi⟩ := not_linearIndependent_iff.mp this | ||
refine hgi (linearIndependent_iff'.mp (bL.linearIndependent.comp e e.injective) t g ?_ i hi) | ||
clear_value c s | ||
simp_rw [← rep_e, Finset.sum_apply, Pi.smul_apply, Finset.smul_sum] | ||
rw [Finset.sum_comm] | ||
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 _ _ _⟩ | ||
simp_rw [smul_comm _ (c i), ← Finset.smul_sum] | ||
erw [eq0, smul_zero] | ||
|
||
variable {K} | ||
|
||
open Function in | ||
theorem rank_fun_infinite {ι : Type v} [hι : Infinite ι] : Module.rank K (ι → K) = #(ι → K) := by | ||
obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ι → K) | ||
obtain ⟨e⟩ := lift_mk_le'.mp ((aleph0_le_mk_iff.mpr hι).trans_eq (lift_uzero #ι).symm) | ||
have := LinearMap.lift_rank_le_of_injective _ <| | ||
LinearMap.funLeft_injective_of_surjective K K _ (invFun_surjective e.injective) | ||
rw [lift_umax.{u,v}, lift_id'.{u,v}] at this | ||
have key := (lift_le.{v}.mpr <| max_aleph0_card_le_rank_fun_nat K).trans this | ||
rw [lift_max, lift_aleph0, max_le_iff] at key | ||
haveI : Infinite ιK := by | ||
rw [← aleph0_le_mk_iff, ← rank_eq_cardinal_basis' bK]; exact key.1 | ||
rw [bK.repr.toEquiv.cardinal_eq, mk_finsupp_lift_of_infinite, | ||
lift_umax.{u,v}, lift_id'.{u,v}, ← rank_eq_cardinal_basis' bK, eq_comm, max_eq_left] | ||
exact key.2 | ||
|
||
/-- The **Erdős-Kaplansky Theorem**: the dual of an infinite-dimensional vector space | ||
over a division ring has dimension equal to its cardinality. -/ | ||
theorem rank_dual_eq_card_dual_of_aleph0_le_rank' {V : Type*} [AddCommGroup V] [Module K V] | ||
(h : ℵ₀ ≤ Module.rank K V) : Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K) := by | ||
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V) | ||
rw [rank_eq_cardinal_basis' b, aleph0_le_mk_iff] at h | ||
have e := (b.constr Kᵐᵒᵖ (M' := K)).symm.trans | ||
(LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Kᵐᵒᵖ) | ||
rw [e.rank_eq, e.toEquiv.cardinal_eq] | ||
apply rank_fun_infinite | ||
|
||
/-- The **Erdős-Kaplansky Theorem** over a field. -/ | ||
theorem rank_dual_eq_card_dual_of_aleph0_le_rank {K V} [Field K] [AddCommGroup V] [Module K V] | ||
(h : ℵ₀ ≤ Module.rank K V) : Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K) := by | ||
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V) | ||
rw [rank_eq_cardinal_basis' b, aleph0_le_mk_iff] at h | ||
have e := (b.constr K (M' := K)).symm | ||
rw [e.rank_eq, e.toEquiv.cardinal_eq] | ||
apply rank_fun_infinite | ||
|
||
theorem lift_rank_lt_rank_dual' {V : Type v} [AddCommGroup V] [Module K V] | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. (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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm not sure what you have in mind? The main content of this proof is that any field K is Nontrivial, so |
||
(h : ℵ₀ ≤ Module.rank K V) : | ||
Cardinal.lift.{u} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K) := by | ||
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V) | ||
rw [rank_eq_cardinal_basis' b, rank_dual_eq_card_dual_of_aleph0_le_rank' h, | ||
← (b.constr ℕ (M' := K)).toEquiv.cardinal_eq, mk_arrow] | ||
apply cantor' | ||
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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Should we have versions of these last two results in the equi-universic setting, that avoid the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Certainly! No need of |
||
(h : ℵ₀ ≤ Module.rank K V) : | ||
Cardinal.lift.{u} (Module.rank K V) < Module.rank K (V →ₗ[K] K) := by | ||
rw [rank_dual_eq_card_dual_of_aleph0_le_rank h, ← rank_dual_eq_card_dual_of_aleph0_le_rank' h] | ||
exact lift_rank_lt_rank_dual' h | ||
|
||
theorem rank_lt_rank_dual' {V : Type u} [AddCommGroup V] [Module K V] (h : ℵ₀ ≤ Module.rank K V) : | ||
Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K) := by | ||
convert lift_rank_lt_rank_dual' h; rw [lift_id] | ||
|
||
theorem rank_lt_rank_dual {K V : Type u} [Field K] [AddCommGroup V] [Module K V] | ||
(h : ℵ₀ ≤ Module.rank K V) : Module.rank K V < Module.rank K (V →ₗ[K] K) := by | ||
convert lift_rank_lt_rank_dual h; rw [lift_id] | ||
|
||
end DivisionRing |
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.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The action of
Lᵐᵒᵖ
onK
is itself obtained manually earlier in the proof rather than automatically: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.