English
If K/F is a CM-extension, then K is a CM-field; in particular, if K is a totally complex abelian extension of Q, it is CM.
Русский
Если K/F — CM-подполе, то K является CM-полем; в частности, если K — полностью комплексное абелеево расширение над Q, то оно CM.
LaTeX
$$$K/F \\text{ CM-extension} \\Rightarrow K \\text{ CM-field}$$$
Lean4
/-- A totally complex abelian extension of `ℚ` is CM.
-/
instance of_isMulCommutative [IsGalois ℚ K] [IsMulCommutative (K ≃ₐ[ℚ] K)] : IsCMField K :=
by
let φ : K →+* ℂ := Classical.choice (inferInstance : Nonempty _)
obtain ⟨σ, hσ₁⟩ : ∃ σ : K ≃ₐ[ℚ] K, ComplexEmbedding.IsConj φ σ :=
exists_isConj_of_isRamified <| isRamified_iff.mpr ⟨IsTotallyComplex.isComplex _, IsTotallyReal.isReal _⟩
have hσ₂ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ :=
by
intro ψ
obtain ⟨ν, rfl⟩ := exists_comp_symm_eq_of_comp_eq (k := ℚ) φ ψ (by ext; simp)
rw [show σ = ν.symm⁻¹ * σ * ν.symm by simp]
exact hσ₁.comp _
exact IsCMField.of_forall_isConj K hσ₂
