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)