English
For φ, ψ : K →+* ℂ, mk φ = mk ψ if and only if φ = ψ or φ equals the complex conjugate of ψ.
Русский
Для гомоморфизмов φ, ψ: K →+* ℂ верно: mk φ = mk ψ тогда и только тогда, когда φ = ψ или φ = conj(ψ).
LaTeX
$$$\\\\forall {φ \\\\psi : K \\\\to+* \\\\mathbb{C}}, \\\\mathrm{mk} \\\\varphi = \\\\mathrm{mk} \\\\psi \\\\iff \\\\varphi = \\\\psi \\\\lor \\\\mathrm{ComplexEmbedding}.\\\\mathrm{conjugate} \\\\varphi = \\\\psi.$$$
Lean4
@[simp]
theorem mk_eq_iff {φ ψ : K →+* ℂ} : mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ :=
by
constructor
· -- We prove that the map ψ ∘ φ⁻¹ between φ(K) and ℂ is uniform continuous, thus it is either the
-- inclusion or the complex conjugation using `Complex.uniformContinuous_ringHom_eq_id_or_conj`
intro h₀
obtain ⟨j, hiφ⟩ := (φ.injective).hasLeftInverse
let ι := RingEquiv.ofLeftInverse hiφ
have hlip : LipschitzWith 1 (RingHom.comp ψ ι.symm.toRingHom) :=
by
change LipschitzWith 1 (ψ ∘ ι.symm)
apply LipschitzWith.of_dist_le_mul
intro x y
rw [NNReal.coe_one, one_mul, NormedField.dist_eq, Function.comp_apply, Function.comp_apply, ← map_sub, ← map_sub]
apply le_of_eq
suffices ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
by
rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _]
rfl
exact congrFun (congrArg (↑) h₀) _
cases Complex.uniformContinuous_ringHom_eq_id_or_conj φ.fieldRange hlip.uniformContinuous with
| inl h =>
left; ext1 x
conv_rhs => rw [← hiφ x]
exact (congrFun h (ι x)).symm
| inr h =>
right; ext1 x
conv_rhs => rw [← hiφ x]
exact (congrFun h (ι x)).symm
· rintro (⟨h⟩ | ⟨h⟩)
· exact congr_arg mk h
· rw [← mk_conjugate_eq]
exact congr_arg mk h
