English
The only closed subfields of ℂ are ℝ and ℂ.
Русский
Единственные замкнутые подполе ℂ — ℝ и ℂ.
LaTeX
$$The real subfield or the whole field, i.e. K = ℝ or K = ℂ.$$
Lean4
/-- The only closed subfields of `ℂ` are `ℝ` and `ℂ`. -/
theorem subfield_eq_of_closed {K : Subfield ℂ} (hc : IsClosed (K : Set ℂ)) : K = ofRealHom.fieldRange ∨ K = ⊤ :=
by
suffices range (ofReal : ℝ → ℂ) ⊆ K
by
rw [range_subset_iff, ← coe_algebraMap] at this
have :=
(Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
(Subfield.toIntermediateField K this).toSubalgebra
simp_rw [← SetLike.coe_set_eq, IntermediateField.coe_toSubalgebra] at this ⊢
exact this
suffices range (ofReal : ℝ → ℂ) ⊆ closure (Set.range ((ofReal : ℝ → ℂ) ∘ ((↑) : ℚ → ℝ)))
by
refine subset_trans this ?_
rw [← IsClosed.closure_eq hc]
apply closure_mono
rintro _ ⟨_, rfl⟩
simp only [Function.comp_apply, ofReal_ratCast, SetLike.mem_coe, SubfieldClass.ratCast_mem]
nth_rw 1 [range_comp]
refine subset_trans ?_ (image_closure_subset_closure_image continuous_ofReal)
rw [DenseRange.closure_range Rat.isDenseEmbedding_coe_real.dense]
simp only [image_univ]
rfl
