English
Let K be a subfield of ℂ and ψ: K →+* ℂ a uniform continuous ring homomorphism. Then ψ equals the inclusion map or the composition with complex conjugation.
Русский
Пусть K — подполе ℂ и ψ: K →+* ℂ — равномерно непрерывная гомоморфия колец. Тогда ψ равна включению или композиции включения с комплексным сопряжением.
LaTeX
$$$\psi = K\text{-subtype} \quad \lor \quad \psi = \text{conj} \circ K\text{-subtype}.$$$
Lean4
/-- Let `K` a subfield of `ℂ` and let `ψ : K →+* ℂ` a ring homomorphism. Assume that `ψ` is uniform
continuous, then `ψ` is either the inclusion map or the composition of the inclusion map with the
complex conjugation. -/
theorem uniformContinuous_ringHom_eq_id_or_conj (K : Subfield ℂ) {ψ : K →+* ℂ} (hc : UniformContinuous ψ) :
ψ.toFun = K.subtype ∨ ψ.toFun = conj ∘ K.subtype :=
by
letI : IsTopologicalDivisionRing ℂ := IsTopologicalDivisionRing.mk
letI : IsTopologicalRing K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
set ι : K → K.topologicalClosure := ⇑(Subfield.inclusion K.le_topologicalClosure)
have ui : IsUniformInducing ι :=
⟨by
rw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
congr⟩
let di := ui.isDenseInducing (?_ : DenseRange ι)
· -- extψ : closure(K) →+* ℂ is the extension of ψ : K →+* ℂ
let extψ := IsDenseInducing.extendRingHom ui di.dense hc
haveI hψ := (uniformContinuous_uniformly_extend ui di.dense hc).continuous
rcases Complex.subfield_eq_of_closed (Subfield.isClosed_topologicalClosure K) with h | h
· left
let j := RingEquiv.subfieldCongr h
let ψ₁ :=
RingHom.comp extψ
(RingHom.comp j.symm.toRingHom ofRealHom.rangeRestrict)
-- Porting note: was `by continuity!` and was used inline
have hψ₁ : Continuous ψ₁ := by
simpa only [RingHom.coe_comp] using hψ.comp ((continuous_algebraMap ℝ ℂ).subtype_mk _)
ext1 x
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ofRealHom.rangeRestrict r = j (ι x)
· have := RingHom.congr_fun (ringHom_eq_ofReal_of_continuous hψ₁) r
rw [RingHom.comp_apply, RingHom.comp_apply] at this
erw [hr] at this
rw [RingEquiv.toRingHom_eq_coe] at this
convert this using 1
· exact (IsDenseInducing.extend_eq di hc.continuous _).symm
· rw [← ofRealHom.coe_rangeRestrict, hr]
rfl
obtain ⟨r, hr⟩ := SetLike.coe_mem (j (ι x))
exact ⟨r, Subtype.ext hr⟩
· -- ψ₁ is the continuous ring hom `ℂ →+* ℂ` constructed from `closure (K) ≃+* ℂ`
-- and `extψ : closure (K) →+* ℂ`
let ψ₁ :=
RingHom.comp extψ
(RingHom.comp (RingEquiv.subfieldCongr h).symm.toRingHom (@Subfield.topEquiv ℂ _).symm.toRingHom)
-- Porting note: was `by continuity!` and was used inline
have hψ₁ : Continuous ψ₁ := by simpa only [RingHom.coe_comp] using hψ.comp (continuous_id.subtype_mk _)
rcases ringHom_eq_id_or_conj_of_continuous hψ₁ with h | h
· left
ext1 z
convert RingHom.congr_fun h z using 1
exact (IsDenseInducing.extend_eq di hc.continuous z).symm
· right
ext1 z
convert RingHom.congr_fun h z using 1
exact (IsDenseInducing.extend_eq di hc.continuous z).symm
· let j : { x // x ∈ closure (id '' {x | (K : Set ℂ) x}) } → (K.topologicalClosure : Set ℂ) := fun x =>
⟨x, by
convert x.prop
simp only [id, Set.image_id']
rfl⟩
convert
DenseRange.comp (Function.Surjective.denseRange _) (IsDenseEmbedding.id.subtype (K : Set ℂ)).dense
(by fun_prop : Continuous j)
rintro ⟨y, hy⟩
use
⟨y, by
convert hy
simp only [id, Set.image_id']
rfl⟩
