English
For x in the ring of integers 𝓞K, complex conjugation fixes x if and only if x lies in the image of 𝓞K^+ under the natural inclusion; i.e., x = algebraMap_{𝓞K^+→𝓞K}(y) for some y ∈ 𝓞K^+.
Русский
Для x ∈ 𝓞K сопряжение Fix, если и только если x лежит в образе 𝓞K^+ под естественным включением; то есть x = algebraMap_{𝓞K^+→𝓞K}(y) для некоторых y ∈ 𝓞K^+.
LaTeX
$$$\\mathrm{complexConj}_K(x)=x \\iff \\exists y \\in \\mathcal{O}_{K^+}, \\; \\mathrm{algebraMap}_{\\mathcal{O}_{K^+}\\to \\mathcal{O}_K}(y)=x$$$
Lean4
protected theorem complexConj_eq_self_iff (u : (𝓞 K)ˣ) :
complexConj K u = u ↔ ∃ v : (𝓞 K⁺)ˣ, algebraMap (𝓞 K⁺) K v = u :=
by
rw [RingOfIntegers.complexConj_eq_self_iff, Units.coe_coe]
refine ⟨fun ⟨y, hy⟩ ↦ ?_, fun ⟨v, hv⟩ ↦ ⟨v, by rw [hv]⟩⟩
have : IsUnit y := by
apply IsUnit.of_map (algebraMap (𝓞 K⁺) (𝓞 K))
rw [show algebraMap (𝓞 K⁺) (𝓞 K) y = u by exact RingOfIntegers.ext hy]
exact u.isUnit
exact ⟨this.unit, by simp [hy]⟩
