isConj_eq_isConj — Mathlib

English

Any two CM-field conjugations over the maximal real subfield coincide; i.e., all choices of σ, τ yield σ = τ.

Русский

Любые два сопряжения CM‑поля над максимальным вещественным подпредполем совпадают; σ = τ.

LaTeX

$$$\\sigma = \\tau$.$$

Lean4

/-- All the conjugations of a CM-field over its maximal real subfield are the same.
-/
theorem isConj_eq_isConj {φ ψ : K →+* ℂ} {σ τ : K ≃ₐ[K⁺] K} (hφ : IsConj φ σ) (hψ : IsConj ψ τ) : σ = τ :=
  by
  have : Nat.card (K ≃ₐ[K⁺] K) = 2 := (IsQuadraticExtension.finrank_eq_two K⁺ K) ▸ IsGalois.card_aut_eq_finrank K⁺ K
  rw [Nat.card_eq_two_iff' 1] at this
  exact
    ExistsUnique.unique this ((isConj_ne_one_iff hφ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ)
      ((isConj_ne_one_iff hψ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal ψ)

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