English
The maximal of aleph0 and the cardinality of K is bounded by the rank of the function space K^N over N.
Русский
Наибольшее между ℵ0 и мощностью поля K ограничено ранговым размером пространства функций K^N.
LaTeX
$$$\max(\aleph_0, \#K) \le \operatorname{Module.rank}_K(\mathbb{N} \to K)$$$
Lean4
/-- 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 DFunLike.coe_injective)
refine max_le aleph0_le ?_
obtain card_K | card_K := le_or_gt #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 :=
by
refine (Subfield.cardinalMk_closure_le_max _).trans_lt (max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩)
rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', 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 := by
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.linearCombination_repr (bL ∘ e)
rw [Finsupp.linearCombination_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_ge 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]
