Erdős-Kaplansky theorem #
For modules over a division ring, we have
rank_dual_eq_card_dual_of_aleph0_le_rank: The Erdős-Kaplansky Theorem which says that the dimension of an infinite-dimensional dual space over a division ring has dimension equal to its cardinality.
theorem
max_aleph0_card_le_rank_fun_nat
(K : Type u)
[DivisionRing K]
:
Cardinal.aleph0 ⊔ Cardinal.mk K ≤ Module.rank K (ℕ → K)
Key lemma towards the Erdős-Kaplansky theorem from https://mathoverflow.net/a/168624
theorem
rank_fun_infinite
{K : Type u}
[DivisionRing K]
{ι : Type v}
[hι : Infinite ι]
:
Module.rank K (ι → K) = Cardinal.mk (ι → K)
theorem
rank_dual_eq_card_dual_of_aleph0_le_rank'
{K : Type u}
[DivisionRing K]
{V : Type u_1}
[AddCommGroup V]
[Module K V]
(h : Cardinal.aleph0 ≤ Module.rank K V)
:
Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)
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
{K : Type u_1}
{V : Type u_2}
[Field K]
[AddCommGroup V]
[Module K V]
(h : Cardinal.aleph0 ≤ Module.rank K V)
:
Module.rank K (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)
The Erdős-Kaplansky Theorem over a field.
theorem
lift_rank_lt_rank_dual'
{K : Type u}
[DivisionRing K]
{V : Type v}
[AddCommGroup V]
[Module K V]
(h : Cardinal.aleph0 ≤ Module.rank K V)
:
Cardinal.lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
theorem
lift_rank_lt_rank_dual
{K : Type u}
{V : Type v}
[Field K]
[AddCommGroup V]
[Module K V]
(h : Cardinal.aleph0 ≤ Module.rank K V)
:
Cardinal.lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)
theorem
rank_lt_rank_dual'
{K : Type u}
[DivisionRing K]
{V : Type u}
[AddCommGroup V]
[Module K V]
(h : Cardinal.aleph0 ≤ Module.rank K V)
:
Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
theorem
rank_lt_rank_dual
{K V : Type u}
[Field K]
[AddCommGroup V]
[Module K V]
(h : Cardinal.aleph0 ≤ Module.rank K V)
:
Module.rank K V < Module.rank K (V →ₗ[K] K)