Complex.uniformContinuous_ringHom_eq_id_or_conj
theorem Complex.uniformContinuous_ringHom_eq_id_or_conj :
∀ (K : Subfield ℂ) {ψ : ↥K →+* ℂ},
UniformContinuous ⇑ψ → ψ.toFun = ⇑K.subtype ∨ ψ.toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
The theorem `Complex.uniformContinuous_ringHom_eq_id_or_conj` states that for any subfield `K` of the complex numbers `ℂ` and any ring homomorphism `ψ` from `K` to `ℂ` that is uniformly continuous, `ψ` is either the inclusion map or the composition of the inclusion map with the complex conjugation. In other words, if `ψ` is a uniformly continuous function from `K` to `ℂ`, then it must map each element of `K` directly to its counterpart in `ℂ` (inclusion), or it must map each element of `K` to the complex conjugate of its counterpart in `ℂ` (complex conjugation).
More concisely: A uniformly continuous ring homomorphism from a subfield of the complex numbers to the complex numbers is either the inclusion map or the composition of the inclusion map with complex conjugation.
|
Complex.subfield_eq_of_closed
theorem Complex.subfield_eq_of_closed : ∀ {K : Subfield ℂ}, IsClosed ↑K → K = Complex.ofReal.fieldRange ∨ K = ⊤ := by
sorry
This theorem states that for any given subfield `K` of the complex numbers (`ℂ`), if `K` is a closed set, then `K` must be either the set of real numbers (`ℝ`) represented as a subfield of complex numbers, or `K` must be the entire set of complex numbers (`ℂ`). Here, the real numbers `ℝ` are embedded into the complex numbers `ℂ` using the function `Complex.ofReal.fieldRange`. The symbol `⊤` represents the entire set of complex numbers.
More concisely: A subfield K of the complex numbers is closed if and only if it is either the set of real numbers or the entire set of complex numbers.
|