The Tensor Product of Abelian Groups

Various maps A × B → C from the cartesian product of two abelian groups to another abelian group are "biadditive" (also called "bilinear"), meaning that they are group homomorphisms when we fix the left or right argument. The tensor product of abelian groups is a construction that produces an abelian group A ⊗ B along with a biadditive map A × B → A ⊗ B which is initial among biadditive maps from A × B. This means that any biadditive map A × B → C factors uniquely through the tensor product via a group homomorphism A ⊗ B → C. Biadditive functions appear in all sorts of contexts ranging from linear algebra to analysis. Therefore having a way to systematically study them is very useful.

Construction

We define the tensor product of abelian groups as a quotient of the free abelian group on pairs of elements of the two groups by the subgroup generated by the biadditive pairs. Here we define the subgroup of biadditive pairs in two steps.

The tensor product ab_tensor_prod A B of two abelian groups A and B is defined to be a quotient of the free abelian group on pairs of elements A × B by the subgroup of biadditive pairs.

The tensor product of A and B contains formal sums and differences of pairs of elements from A and B. We denote these pairs as "simple tensors" and name them tensor.

Properties of tensors

The characterizing property of simple tensors are that they are biadditive in their arguments. A tensor of a sum distributes over the sum on the left.

A tensor of a sum distributes over the sum on the right.

Tensoring on the left is a group homomorphism.

Tensoring on the right is a group homomorphism.

Tensors preserve negation in the left argument.

Tensors preserve negation in the right argument.

Tensoring by zero on the left is zero.

Tensoring by zero on the right is zero.

The tensor map is biadditive and therefore can be written in a curried form using the internal abelian group hom.

Induction principles

Here we write down some induction principles to help us prove lemmas about the tensor product. Some of these are quite specialised but are patterns that appear often in practice. Our main recursion principle states that in order to build a homomorphism out of the tensor product, it is sufficient to provide a map out of the direct product which is biadditive, that is, a map that preserves addition in each argument of the product. We separate out the proof of this part, so we can make it opaque.

A special case that arises.

We give an induction principle for an hprop-valued type family P. It may be surprising at first that we only require P to hold for the simple tensors tensor a b and be closed under addition. It automatically follows that P 0 holds (since tensor 0 0 = 0) and that P is closed under negation (since tensor -a b = - tensor a b). This induction principle says that the simple tensors generate the tensor product as a semigroup.

As a commonly occuring special case of the above induction principle, we have the case when the predicate in question is showing that two group homomorphisms out of the tensor product are homotopic. In order to do this, it suffices to show it only for simple tensors. The homotopy is closed under addition, so we don't need to hypothesise anything else.

As an even more specialised case, we occasionally have the second homomorphism being a sum of abelian group homomorphisms. In those cases, it is easier to use this specialised lemma.

Here we give an induction principle for a triple tensor, a.k.a a dependent trilinear function.

Similar to before, we specialise the triple tensor induction principle for proving homotopies of trilinear/triadditive functions.

As explained for the biadditive and triadditive cases, we also derive an induction principle for quadruple tensors giving us dependent quadrilinear maps.

To construct a homotopy between quadrilinear maps we need only check equality for the quadruple simple tensors.

Universal Property of the Tensor Product

A function of two variables is biadditive if it preserves the operation in each variable.

The truncation level of the IsBiadditive f predicate is determined by the truncation level of the codomain. This will almost always be a hset.

The simple tensor map is biadditive.

The type of biadditive maps.

The universal property of the tensor product is that biadditive maps between abelian groups are in one-to-one corresondance with maps out of the tensor product. In this sense, the tensor product is the most perfect object describing biadditive maps between two abelian groups.

Functoriality of the Tensor Product

The tensor product produces a bifunctor and we will later show that it gives a symmetric monoidal structure on the category of abelian groups. Given a pair of maps, we can produce a homomorphism between the pairwise tensor products of the domains and codomains.

2-functoriality of the tensor product.

The tensor product functor preserves identity morphisms.

The tensor product functor preserves composition.

The tensor product functor is a 0-bifunctor.

The tensor product functor is a bifunctor.

Symmetry of the Tensor Product

The tensor product is symmetric in that the order in which we take the tensor shouldn't matter upto isomorphism. We can define a swap map which swaps the order of simple tensors.

ab_tensor_swap is involutive.

ab_tensor_swap is natural in both arguments. This means that it also acts on tensor functors.

The swap map gives us a symmetric braiding on the category of abelian groups. We will later show it is a full symmetric monoidal category.

Twisting Triple Tensors

In order to construct the symmetric monoidal category, we will use what is termed the "Twist construction" in Monoidal.v. This simplifies the data of a symmetric monoidal category by constructing it from simpler parts. For instance, instead of having to prove full associativity (A ⊗ B) ⊗ C $-> A ⊗ (B ⊗ C), we can provide a twist map A ⊗ (B ⊗ C) $-> B ⊗ (A ⊗ C) and use the symmetric braiding we have so far to prove associativity. In order to be more efficient whilst unfolding definitions, we break up the definition of a twist map into its components.

Given a triple tensor product, we have a twist map which permutes the first two components.

The twist map is involutive.

The twist map is natural in all 3 arguments. This means that the twist map acts on the triple tensor functor in the same way.

Unitality of abgroup_Z

In the symmetric monoidal structure on abelian groups, abgroup_Z is the unit. We show that tensoring with abgroup_Z on the right is isomorphic to the original group. First we characterise the action of integers via grp_pow and their interaction on tensors. This is just a generalisation of the distributivity laws for tensors. Multiplication in the first factor can be factored out.

Multiplication in the second factor can be factored out.

Multiplication can be transferred from one factor to the other. The tensor product of R-modules will include this as an extra axiom, but here we have Z-modules and we can prove it.

abgroup_Z is a right identity for the tensor product.

Checking that the inverse map is a homomorphism is easier.

We have a right unitor for the tensor product given by unit abgroup_Z. Naturality of ab_tensor_prod_Z_r is straightforward to prove.

Since we have symmetry of the tensor product, we get left unitality for free.

Symmetric Monoidal Structure of Tensor Product

Using the twist construction we can derive an associator for the tensor product. In other words, we have associativity of the tensor product of abelian groups natural in each factor.

The triangle identity is straightforward to prove using the custom induction principles we proved earlier.

The hexagon identity is also straighforward to prove. We simply have to reduce all the involved functions on the simple tensors using our custom triple tensor induction principle.

Finally, we can prove the pentagon identity using the quadruple tensor induction principle. As we did before, the work only involves reducing the involved functions on the simple tensor redexes.

We therefore have all the data of a monoidal category.

And furthermore, all the data of a symmetric monoidal category.

Preservation of Coequalizers

The tensor product of abelian groups preserves coequalizers, meaning that the coequalizer of two tensored groups is the tensor of the coequalizer. We show this is the case on the left and the right. Tensor products preserve coequalizers on the right.

The equivalence respects the natural maps from ab_tensor_prod A C.

Tensor products preserve coequalizers on the left.

The equivalence respects the natural maps from ab_tensor_prod B C.

Tensor Product of Free Abelian Groups

Tensor products distribute over direct sums

TODO: Show that the category of abelian groups is symmetric closed and therefore we have adjoint pair with the tensor and internal hom. This should allow us to prove lemmas such as tensors distributing over coproducts.