Separating tensors by linear functionals #
Separating families of linear functionals detect zero tensors by contraction, first in one factor and then in both, over a commutative semiring with a projective right factor. These lemmas supply the shared separation step for rational-point separation and reducedness of tensor products of algebras. Over a field, every module is projective.
theorem
TauCeti.tensor_eq_zero_of_forall_lid_rTensor_eq_zero
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[Module.Projective R N]
(f : ι → M →ₗ[R] R)
(hf : ∀ (m : M), (∀ (i : ι), (f i) m = 0) → m = 0)
(x : TensorProduct R M N)
(hx : ∀ (i : ι), (TensorProduct.lid R N) ((LinearMap.rTensor N (f i)) x) = 0)
:
Contracting against a separating family in the left factor detects zero tensors when the right factor is projective.
theorem
TauCeti.tensor_eq_zero_of_forall_lid_map_eq_zero
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid N]
[Module R N]
[Module.Projective R N]
(f : ι → M →ₗ[R] R)
(g : κ → N →ₗ[R] R)
(hf : ∀ (m : M), (∀ (i : ι), (f i) m = 0) → m = 0)
(hg : ∀ (n : N), (∀ (j : κ), (g j) n = 0) → n = 0)
(x : TensorProduct R M N)
(hx : ∀ (i : ι) (j : κ), (TensorProduct.lid R R) ((TensorProduct.map (f i) (g j)) x) = 0)
:
Products of separating families of linear functionals detect zero tensors when the right factor is projective.