Detecting zero tensors by rational points #
Families of rational points detecting zero in two algebras also detect zero in their tensor product over a commutative semiring when the right algebra is projective as a module. This lets one check tensor vanishing on products of those families, without any finite-type or algebraic-closedness hypothesis. Over a field, every module is projective.
theorem
TauCeti.tensor_eq_zero_of_forall_productMap_eq_zero
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[Semiring B]
[Algebra R B]
[Module.Projective R B]
(f : ι → A →ₐ[R] R)
(g : κ → B →ₐ[R] R)
(hf : ∀ (a : A), (∀ (i : ι), (f i) a = 0) → a = 0)
(hg : ∀ (b : B), (∀ (j : κ), (g j) b = 0) → b = 0)
(x : TensorProduct R A B)
(hx : ∀ (i : ι) (j : κ), (Algebra.TensorProduct.productMap (f i) (g j)) x = 0)
:
Products of families of rational points detecting zero in each algebra detect zero in the tensor product when the right algebra is projective as a module.