English
For x in the ring of integers 𝓞K, complex conjugation fixes x exactly when x comes from the ring of integers of the real subfield; equivalently, there exists y in 𝓞K^+ with algebraMap(𝓞K^+) to 𝓞K of y equal to x.
Русский
Для x из кольца целых чисел 𝓞K фиксатируется сопряжением тогда и только тогда, когда x исходит из кольца целых чисел вещественного подполя; эквивалентно, существует y в 𝓞K^+, такой что алгебраическое отображение 𝓞K^+ → 𝓞K отправляет y в x.
LaTeX
$$$\\mathrm{complexConj}_K(x)=x \\iff \\exists y \\in \\mathcal{O}_{K^+}, \\; \\iota(y)=x$$$
Lean4
protected theorem complexConj_eq_self_iff (x : 𝓞 K) : complexConj K x = x ↔ ∃ y : 𝓞 K⁺, algebraMap (𝓞 K⁺) K y = x :=
by
rw [complexConj_eq_self_iff]
refine ⟨fun h ↦ ?_, fun ⟨y, hy⟩ ↦ ?_⟩
· have : IsIntegral ℤ (⟨x, h⟩ : K⁺) :=
(isIntegral_algebraMap_iff (FaithfulSMul.algebraMap_injective K⁺ K)).mp x.isIntegral_coe
refine ⟨⟨⟨x, h⟩, this⟩, ?_⟩
rw [IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺, RingOfIntegers.map_mk]
rfl
· rw [← hy, IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺]
exact SetLike.coe_mem _
