English
If K and L are uncountable algebraically closed fields with the same characteristic, then they are isomorphic provided a ring equivalence exists.
Русский
Если K и L — невычисляемые алгебраически замкнутые поля с одинаковой характеристикой, то они изоморфны при наличии кольцевого эквивалента.
LaTeX
$$If K,L uncountable and IsAlgClosed K,L and Char(K)=Char(L), then Nonempty (K ≃+* L).$$
Lean4
/-- If `K` is an uncountable algebraically closed field, then its
cardinality is the same as that of a transcendence basis.
For a simpler, but less universe-polymorphic statement, see
`IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'` -/
theorem cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt [Nontrivial R] (hv : IsTranscendenceBasis R v)
(hR : #R ≤ ℵ₀) (hK : ℵ₀ < #K) : Cardinal.lift.{w} #K = Cardinal.lift.{v} #ι :=
have : ℵ₀ ≤ Cardinal.lift.{max u v} #ι :=
le_of_not_gt fun h =>
not_le_of_gt (show ℵ₀ < Cardinal.lift.{max u w} #K by simpa) <|
calc
Cardinal.lift.{max u w, v} #K ≤
max (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀ :=
cardinal_le_max_transcendence_basis v hv
_ ≤ _ := max_le (max_le (by simpa) (by simpa using le_of_lt h)) le_rfl
suffices Cardinal.lift.{max u w} #K = Cardinal.lift.{max u v} #ι from Cardinal.lift_injective.{u, max v w} (by simpa)
le_antisymm
(calc
Cardinal.lift.{max u w} #K ≤ max (max (Cardinal.lift.{max v w} #R) (Cardinal.lift.{max u v} #ι)) ℵ₀ :=
cardinal_le_max_transcendence_basis v hv
_ = Cardinal.lift #ι := by
rw [max_eq_left, max_eq_right]
· exact le_trans (by simpa using hR) this
· exact le_max_of_le_right this)
(lift_mk_le.2 ⟨⟨v, hv.1.injective⟩⟩)
