Hamel basis and reals isomorphic to the complexes as an a...

Stream: Is there code for X?

[Yakov Pechersky]

Do we have that R is isomorphic to C as an additive group? Likely, this would be shown via an argument about the construction of a Hamel basis for C using the basis from R.

[Jireh Loreaux]

I don't think we have this, but I don't think we even have the Module.rank of ℝ or ℂ over ℚ either. Once we prove that (which is a relatively simple cardinality argument), it follows directly from LinearEquiv.ofRankEq. The first lemma can definitely be generalized so that R and M don't have to live in the same universe, but I was lazy because I knew where I was headed.

import Mathlib

lemma Module.rank_eq_cardinal_mk_of_lt (R M : Type) [Ring R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Infinite R] [StrongRankCondition R] (h_lt : Cardinal.mk R < Cardinal.mk M) :
    Module.rank R M = Cardinal.mk M := by
  have : Infinite M :=
    Cardinal.infinite_iff.mpr <| (Cardinal.infinite_iff.mp inferInstance).trans h_lt.le
  have h := ((Module.Free.chooseBasis R M).repr : M ≃ (Module.Free.ChooseBasisIndex R M →₀ R)).cardinal_eq
  simp only [Cardinal.mk_finsupp_lift_of_infinite', Cardinal.lift_id', ge_iff_le,
    ← Module.Free.rank_eq_card_chooseBasisIndex] at h
  exact ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ h_lt.ne).left

@[simp]
lemma Real.rank_rat_real : Module.rank ℚ ℝ = Cardinal.continuum := by
  refine (Module.rank_eq_cardinal_mk_of_lt ℚ ℝ ?_).trans Cardinal.mk_real
  simpa [Cardinal.mk_real] using Cardinal.aleph0_lt_continuum

@[simp]
lemma Complex.rank_rat_complex : Module.rank ℚ ℂ = Cardinal.continuum := by
  refine (Module.rank_eq_cardinal_mk_of_lt ℚ ℂ ?_).trans mk_complex
  simpa [Cardinal.mk_real] using Cardinal.aleph0_lt_continuum

noncomputable def Complex.linearEquiv_rat_real : ℂ ≃ₗ[ℚ] ℝ :=
  LinearEquiv.ofRankEq ℂ ℝ <| by simp

[Jireh Loreaux]

#6672