Basic facts about indexed tensor products #
If every element of one factor is its own additive inverse, then so is every element of an
indexed tensor product. This holds over a ring of characteristic two
and also, for instance, for a module of 𝔽₂-valued cochains regarded over ℤ; it is how terms
appearing twice cancel in sign-free constructions on tensor powers. Over a single index, every
element of a tensor power is a pure tensor.
Main results #
PiTensorProduct.add_self_eq_zero: if every element of one factor is its own additive inverse, so is every element of the indexed tensor product.TauCeti.PiTensorProduct.exists_eq_tprod_of_subsingleton: over a single index, every element of a tensor power is a pure tensor.
theorem
PiTensorProduct.add_self_eq_zero
{ι : Type uι}
{R : Type uR}
[CommSemiring R]
{M : ι → Type uM}
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
(x : PiTensorProduct R fun (i : ι) => M i)
(i : ι)
(hM : ∀ (m : M i), m + m = 0)
:
If every element of the factor at i is its own additive inverse, then so is every element
of the indexed tensor product. No hypothesis is needed on the other factors.
theorem
TauCeti.PiTensorProduct.exists_eq_tprod_of_subsingleton
{ι : Type uι}
{R : Type uR}
{M : Type uM}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[Subsingleton ι]
(i₀ : ι)
(x : PiTensorProduct R fun (x : ι) => M)
:
∃ (y : M), x = (PiTensorProduct.tprod R) fun (x : ι) => y
Over a single index i₀, every element of a tensor power of M is a pure tensor
tprod R fun _ ↦ y.