English
An extensionality lemma for algebra homomorphisms: two AlgHoms from MvPolynomial to B are equal if they agree on all X_i and on the canonical embedding of the base ring.
Русский
Лемма экстенсиональности для алгебра-гомоморфизмов: если два AlgHom с MvPolynomial в B согласны по всем X_i и по каноническому вложению базового кольца, они равны.
LaTeX
$$$\\\\forall f,g: MvPolynomial\\\\sigma\\\\,A \\\\to_A B, \\\\Big( f \\circ (IsScalarTower.toAlgHom R A (MvPolynomial\\\\sigma\\\\,A)) = g \\circ (IsScalarTower.toAlgHom R A (MvPolynomial\\\\sigma\\\\,A)) \\\\Big) \\\\land \\\\Big( \\\\forall i, f(X i) = g(X i) \\\\Big) \\\\Rightarrow f = g$$$
Lean4
@[ext 1100]
theorem algHom_ext' {A B : Type*} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B]
{f g : MvPolynomial σ A →ₐ[R] B}
(h₁ :
f.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = g.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)))
(h₂ : ∀ i, f (X i) = g (X i)) : f = g :=
AlgHom.coe_ringHom_injective (MvPolynomial.ringHom_ext' (congr_arg AlgHom.toRingHom h₁) h₂)
