English
If φ and σ satisfy a conjugacy relation, then mk φ unramified corresponds to σ = 1.
Русский
Если φ и σ удовлетворяют сопряженности, то mk φ неразморожено соответствует σ = 1.
LaTeX
$$$\\text{isUnramified}(k, (mk\\ φ)) \\iff σ = 1$$$
Lean4
theorem isUnramified_mk_iff_forall_isConj [IsGalois k K] {φ : K →+* ℂ} :
IsUnramified k (mk φ) ↔ ∀ σ : K ≃ₐ[k] K, ComplexEmbedding.IsConj φ σ → σ = 1 :=
by
refine ⟨fun H σ hσ ↦ hσ.isUnramified_mk_iff.mp H, fun H ↦ ?_⟩
by_contra hφ
rw [not_isUnramified_iff] at hφ
rw [comap_mk, isReal_mk_iff, ← not_isReal_iff_isComplex, isReal_mk_iff, ←
ComplexEmbedding.isConj_one_iff (k := k)] at hφ
letI := (φ.comp (algebraMap k K)).toAlgebra
letI := φ.toAlgebra
have : IsScalarTower k K ℂ := IsScalarTower.of_algebraMap_eq' rfl
let φ' : K →ₐ[k] ℂ := { star φ with commutes' := fun r ↦ by simpa using RingHom.congr_fun hφ.2 r }
have : ComplexEmbedding.IsConj φ (AlgHom.restrictNormal' φ' K) :=
(RingHom.ext <| AlgHom.restrictNormal_commutes φ' K).symm
exact hφ.1 (H _ this ▸ this)
