ext_of_adjoin_eq_top — Mathlib

English

Let S be a subalgebra with S = adjoin R s. Then two AlgHoms from S to B are equal if they agree on s.

Русский

Пусть S — подалгебра с S = adjoin_R s. Тогда две AlgHom из S в B равны, если они согласны на s.

LaTeX

$$$\\forall φ_1 φ_2:\\ S \\to_{} B,\\ (∀ x∈s, φ_1 x = φ_2 x) \\Rightarrow φ_1 = φ_2$$$

Lean4

theorem ext_of_adjoin_eq_top {s : Set A} (h : adjoin R s = ⊤) ⦃φ₁ φ₂ : A →ₐ[R] B⦄ (hs : s.EqOn φ₁ φ₂) : φ₁ = φ₂ :=
  ext fun _x => adjoin_le_equalizer φ₁ φ₂ hs <| h.symm ▸ trivial

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