English
Two uncountable algebraically closed fields of characteristic zero are isomorphic if they have the same cardinality and the same characteristic.
Русский
Два невычислимых алгебраически замкнутых поля характеристик ноль с одинаковой кардинальностью изоморфны.
LaTeX
$$IsAlgClosed.ringEquiv_of_equiv_of_charZero hK hKL$$
Lean4
/-- Two uncountable algebraically closed fields of characteristic zero are isomorphic
if they have the same cardinality. -/
theorem ringEquiv_of_equiv_of_charZero [CharZero K] [CharZero L] (hK : ℵ₀ < #K) (hKL : Nonempty (K ≃ L)) :
Nonempty (K ≃+* L) := by
obtain ⟨s, hs⟩ := exists_isTranscendenceBasis ℤ K
obtain ⟨t, ht⟩ := exists_isTranscendenceBasis ℤ L
have hL : ℵ₀ < #L := by rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t :=
by
rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (le_of_eq mk_int) hK), ←
lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (le_of_eq mk_int) hL)]
exact Cardinal.lift_mk_eq'.2 hKL
obtain ⟨e⟩ := Cardinal.lift_mk_eq'.1 this
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
