ringOfIntegersComplexConj_eq_self_iff

English

A unit u of 𝓞K is fixed by complex conjugation if and only if u comes from 𝓞K^+; equivalently, there exists v in (𝓞K^+)^× with algebraMap(v)=u.

Русский

Единица u из 𝓞K фиксируется сопряжением тогда и только тогда, когда она происходит из 𝓞K^+; эквивалентно существует v ∈ (𝓞K^+)^× с algebraMap(v)=u.

LaTeX

$$$$\\\\mathrm{complexConj}_K(u)=u \\iff \\exists v \\in (\\\\mathcal{O}_{K^+})^{\\times}, \\\\mathrm{algebraMap}_{\\\\mathcal{O}_{K^+} \\to \\\\mathcal{O}_K}(v)=u.$$$$

Lean4

theorem ringOfIntegersComplexConj_eq_self_iff (x : 𝓞 K) :
    ringOfIntegersComplexConj K x = x ↔ x ∈ Set.range (algebraMap (𝓞 K⁺) (𝓞 K)) :=
  by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rw [RingOfIntegers.ext_iff, coe_ringOfIntegersComplexConj, RingOfIntegers.complexConj_eq_self_iff] at h
    obtain ⟨y, hy⟩ := h
    exact ⟨y, RingOfIntegers.ext_iff.mpr hy⟩
  · rintro ⟨y, rfl⟩
    simp

Похожие утверждения