English
A totally complex field that has a unique complex conjugation is CM.
Русский
Поле полностью комплексное, имеющее единственноe комплексное сопряжение, является CM-полем.
LaTeX
$$$\\text{If } K \\text{ is totally complex and there exists a unique } \\sigma\\text{ with } ∀\\phi:K\\to\\mathbb{C}, IsConj(\\phi,\\sigma), \\text{ then } K \\text{ is CM}.$$$
Lean4
/-- A totally complex field that has a unique complex conjugation is CM.
-/
theorem _root_.NumberField.IsCMField.of_forall_isConj {σ : K ≃ₐ[ℚ] K} (hσ : ∀ φ : K →+* ℂ, IsConj φ σ) : IsCMField K :=
by
have : IsTotallyReal (fixedField (Subgroup.zpowers σ)) :=
⟨fun w ↦ by
obtain ⟨W, rfl⟩ := w.comap_surjective (K := K)
let τ := subgroupEquivAlgEquiv _ ⟨σ, Subgroup.mem_zpowers σ⟩
have hτ : IsConj W.embedding τ := hσ _
simpa [← isReal_mk_iff, ← InfinitePlace.comap_mk, mk_embedding] using hτ.isReal_comp⟩
have : IsQuadraticExtension (fixedField (Subgroup.zpowers σ)) K :=
⟨by
let φ : K →+* ℂ := Classical.choice (inferInstance : Nonempty _)
have hσ' : σ ≠ 1 := (isConj_ne_one_iff (hσ φ)).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ
rw [finrank_fixedField_eq_card, Nat.card_zpowers, orderOf_isConj_two_of_ne_one (hσ φ) hσ']⟩
exact IsCMField.ofCMExtension (fixedField (Subgroup.zpowers σ)) K
