Point separation after tensoring

Points of a reduced finite-type algebra valued in an algebraically closed extension detect not only its elements but also tensors with any vector space. This allows identities in a family of vectors to be checked at every geometric point of the parameter algebra.

theorem TauCeti.tensor_eq_of_forall_map_algHom_eq {k : Type u_1} {B : Type u_2} {M : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsAlgClosed K] [CommRing B] [Algebra k B] [Algebra.FiniteType k B] [IsReduced B] [AddCommGroup M] [Module k M] {x y : TensorProduct k B M} (h : ∀ (p : B →ₐ[k] K), (TensorProduct.map p.toLinearMap LinearMap.id) x = (TensorProduct.map p.toLinearMap LinearMap.id) y) : x = y

Algebraically closed specializations of the first factor detect equality of tensors when that factor is a reduced finite-type algebra over a field.