feat(LinearAlgebra): the Erdős-Kaplansky theorem (#9159)

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>

Author: alreadydone

Mathlib/LinearAlgebra/Dimension.lean

@@ -108,6 +108,9 @@ protected irreducible_def Module.rank : Cardinal :=
   ⨆ ι : { s : Set V // LinearIndependent K ((↑) : s → V) }, (#ι.1)
 #align module.rank Module.rank
 
+theorem rank_le_card : Module.rank K V ≤ #V :=
+  (Module.rank_def _ _).trans_le (ciSup_le' fun _ ↦ mk_set_le _)
+
 lemma nonempty_linearIndependent_set : Nonempty {s : Set V // LinearIndependent K ((↑) : s → V)} :=
   ⟨⟨∅, linearIndependent_empty _ _⟩⟩
 
@@ -1672,8 +1675,8 @@ theorem rank_finset_sum_le {η} (s : Finset η) (f : η → V →ₗ[K] V') :
 #align linear_map.rank_finset_sum_le LinearMap.rank_finset_sum_le
 
 theorem le_rank_iff_exists_linearIndependent {c : Cardinal} {f : V →ₗ[K] V'} :
-    c ≤ rank f ↔ ∃ s : Set V, Cardinal.lift.{v'} #s =
-    Cardinal.lift.{v} c ∧ LinearIndependent K fun x : s => f x := by
+    c ≤ rank f ↔ ∃ s : Set V,
+    Cardinal.lift.{v'} #s = Cardinal.lift.{v} c ∧ LinearIndependent K (fun x : s => f x) := by
   rcases f.rangeRestrict.exists_rightInverse_of_surjective f.range_rangeRestrict with ⟨g, hg⟩
   have fg : LeftInverse f.rangeRestrict g := LinearMap.congr_fun hg
   refine' ⟨fun h => _, _⟩

Mathlib/LinearAlgebra/Dual.lean

@@ -90,10 +90,6 @@ The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to
   * `Subspace.dualQuotDistrib W` is an equivalence
     `Dual K (V₁ ⧸ W) ≃ₗ[K] Dual K V₁ ⧸ W.dualLift.range` from an arbitrary choice of
     splitting of `V₁`.
-
-## TODO
-
-Erdős-Kaplansky theorem about the dimension of a dual vector space in case of infinite dimension.
 -/
 
 noncomputable section
@@ -408,6 +404,18 @@ theorem toDualEquiv_apply (m : M) : b.toDualEquiv m = b.toDual m :=
   rfl
 #align basis.to_dual_equiv_apply Basis.toDualEquiv_apply
 
+-- Not sure whether this is true for free modules over a commutative ring
+/-- A vector space over a field is isomorphic to its dual if and only if it is finite-dimensional:
+  a consequence of the Erdős-Kaplansky theorem. -/
+theorem linearEquiv_dual_iff_finiteDimensional [Field K] [AddCommGroup V] [Module K V] :
+    Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V := by
+  refine ⟨fun ⟨e⟩ ↦ ?_, fun h ↦ ⟨(Module.Free.chooseBasis K V).toDualEquiv⟩⟩
+  rw [FiniteDimensional, ← Module.rank_lt_alpeh0_iff]
+  by_contra!
+  apply (lift_rank_lt_rank_dual this).ne
+  have := e.lift_rank_eq
+  rwa [lift_umax.{uV,uK}, lift_id'.{uV,uK}] at this
+
 /-- Maps a basis for `V` to a basis for the dual space. -/
 def dualBasis : Basis ι R (Dual R M) :=
   b.map b.toDualEquiv

Mathlib/LinearAlgebra/FreeModule/Rank.lean

@@ -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]
+    (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]
+    (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