exists_comp_symm_eq_of_comp_eq — Mathlib

English

If φ, ψ: K → ℂ have the same restriction to k via algebra maps, then there exists σ ∈ Aut_k(K) such that φ ∘ σ^{-1} = ψ.

Русский

Если отображения φ, ψ: K → ℂ совпадают при ограничении к K над k, тогда существует σ в Aut_k(K) such that φ ∘ σ^{-1} = ψ.

LaTeX

$$$\bigl( φ \circ (\mathrm{algebraMap}\ k K) = ψ \circ (\mathrm{algebraMap}\ k K) \bigr) \Rightarrow ∃ σ ∈ \mathrm{Aut}_k(K),\; φ \circ σ^{-1} = ψ$$$

Lean4

theorem exists_comp_symm_eq_of_comp_eq [Algebra k K] [IsGalois k K] (φ ψ : K →+* ℂ)
    (h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)) : ∃ σ : K ≃ₐ[k] K, φ.comp σ.symm = ψ :=
  by
  letI := (φ.comp (algebraMap k K)).toAlgebra
  letI := φ.toAlgebra
  have : IsScalarTower k K ℂ := IsScalarTower.of_algebraMap_eq' rfl
  let ψ' : K →ₐ[k] ℂ := { ψ with commutes' := fun r ↦ (RingHom.congr_fun h r).symm }
  use (AlgHom.restrictNormal' ψ' K).symm
  ext1 x
  exact AlgHom.restrictNormal_commutes ψ' K x

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