algHom_ext — Mathlib

English

If two algebra homomorphisms f,g: S → S' agree on the generator pb.gen, then f = g.

Русский

Если две алгебра-гомоморфизмы f,g: S → S' совпадают на основном генераторе pb.gen, то f = g.

LaTeX

$$$\\forall f,g: S \\to_{R} S',\\; f(pb.gen)=g(pb.gen) \\Rightarrow f=g$.$$

Lean4

theorem algHom_ext {S' : Type*} [Semiring S'] [Algebra R S'] (pb : PowerBasis R S) ⦃f g : S →ₐ[R] S'⦄
    (h : f pb.gen = g pb.gen) : f = g := by
  ext x
  obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
  rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]

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