English
A high-level extensional principle for AlgHoms on PiTensorProduct: equality of all single-factor compositions implies equality of the whole homomorphisms.
Русский
Высокий экстенсиональный принцип для гомоморфизмов на PiTensorProduct: равенство по всем композициям с одиночными факторами вносит равенство самих гомоморфизмов.
LaTeX
$$$\\text{algHom\_ext}$$$
Lean4
/-- To show two algebra morphisms from finite tensor products are equal, it suffices to show that
they agree on elements of the form $1 ⊗ ⋯ ⊗ a ⊗ 1 ⊗ ⋯$. -/
@[ext high]
theorem algHom_ext {S : Type*} [Finite ι] [DecidableEq ι] [Semiring S] [Algebra R S] ⦃f g : (⨂[R] i, A i) →ₐ[R] S⦄
(h : ∀ i, f.comp (singleAlgHom i) = g.comp (singleAlgHom i)) : f = g :=
AlgHom.toLinearMap_injective <|
PiTensorProduct.ext <|
MultilinearMap.ext fun x =>
suffices f.toMonoidHom.comp (tprodMonoidHom R) = g.toMonoidHom.comp (tprodMonoidHom R) from
DFunLike.congr_fun this x
MonoidHom.pi_ext fun i xi => DFunLike.congr_fun (h i) xi
