algHom_ext_of_eq_adjoin — Mathlib

English

If S is an intermediate field with S = adjoin F s, then two AlgHom from S that agree on s are equal.

Русский

Если S = adjoin F s, то любые две AlgHom из S, совпадающие на s, равны.

LaTeX

$$$\\\\text{algHom\_ext\_of\_eq\_adjoin}_{F,S}(hS) : (\\\\forall x \\\\in s, φ_1 x = φ_2 x) \\\\Rightarrow φ_1 = φ_2.$$$

Lean4

theorem algHom_ext_of_eq_adjoin {S : IntermediateField F E} {s : Set E} (hS : S = adjoin F s) ⦃φ₁ φ₂ : S →ₐ[F] K⦄
    (h : ∀ x hx, φ₁ ⟨x, hS.ge (subset_adjoin _ _ hx)⟩ = φ₂ ⟨x, hS.ge (subset_adjoin _ _ hx)⟩) : φ₁ = φ₂ := by subst hS;
  exact adjoin_algHom_ext F h

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