exists_comp_symm_eq_of_comp_eq — Mathlib

English

If two maps φ and ψ agree on the base field, then there exists a Galois automorphism σ with φ ∘ σ^{-1} = ψ.

Русский

Если две карты согласованы на базовом поле, существует галуа-автоморфизм σ с φ ∘ σ^{-1} = ψ.

LaTeX

$$$ \exists \sigma : K \simeq_k K, \; φ \circ σ^{-1} = ψ $$$

Lean4

theorem exists_comp_symm_eq_of_comp_eq [IsGalois k K] (φ ψ : K →+* ℂ)
    (h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)) : ∃ σ : K ≃ₐ[k] K, φ.comp σ.symm = ψ :=
  NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq φ ψ h

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