Tensor products of graded objects / chain complexes

Stream: maths

[Scott Morrison]

I would really like to see the monoidal structure on chain complexes, which will unlock many interesting bits of maths.

Unfortunately it seems hard to implement. In fact, even forgetting about differentials and just defining it on graded objects, where

$(X ⊗ Y)_i = ⊕_{i=j+k} X_j ⊗ Y_k$

seems quite difficult. I'm happy to restrict to ℕ-graded objects, as I think the additional difficulties for bounded complexes are of a different sort. (Note that graded objects are a helpful stepping stone to chain complexes, as the forgetful functor is faithful, so if you can check the pentagon equation for graded objects you'll get it for free for chain complexes.)

So the first question is just: is there some abstract nonsense way of thinking about this tensor product that I am missing? Something that magically combines the additive monoidal structures on the ambient category, the fact that ℕ is a discrete monoidal category under additional, and naturally makes use of the direct sums?

Doing things directly, the tensor product itself is not difficult. I can then define the associator for tensor product of graded objects, although it is a somewhat grungy combination of six maps:

((X ⊗ Y) ⊗ Z)_i = ⊕_{i=ab+c} (⊕_{ab=a+b} X_a ⊗ Y_b) ⊗ Z_c  := rfl
  _ ≅ ⊕ ⊕ (X_a ⊗ Y_b) ⊗ Z_c                                := distributivity
  _ ≅ ⊕_{((a,b),c)} (X_a ⊗ Y_b) ⊗ Z_c                      := iterated biproducts are biproducts over a sigma type
  _ ≅ ⊕_{(a,(b,c))} (X_a ⊗ Y_b) ⊗ Z_c                      := reindexing use associativity of antidiagonal
  _ ≅ ⊕_{(a,(b,c))} X_a ⊗ (Y_b ⊗ Z_c)                      := the associator in the ambient category
  _ ≅ ⊕ ⊕ X_a ⊗ (Y_b ⊗ Z_c)                                := iterated biproducts are biproducts over a sigma type
  _ ≅ ⊕_{i=a+bc} X_a ⊗ (⊕_{bc=b+c} Y_b Z_c)                := distributivity
  _ = (X ⊗ (Y ⊗ Z))_i                                      := rfl

However with this definition checking the pentagon equation seems intractable (it's an equation involving 30 morphisms, and a lot of rewriting, and simp only gets you so far). I've made a few recent PRs that make this a bit easier, but it still looks too hard.

[Scott Morrison]

The second question is if anyone has advice for tackling the pentagon equation if this is the best we can do for the associator.

The third question is if anyone is interested in working on this. :-) I won't be doing more on this in the near future, but I think it is important for lots of homological algebra.

[Eric Wieser]

I had a branch somewhere that worked with (the ring structure implied by) graded tensor products in ZMod 2, defined with

$(a\otimes b)(a^{\prime}\otimes b^{\prime})=(-1)^{(\operatorname{deg}b)(\operatorname{deg}a^{\prime})}aa^{\prime}\otimes bb^{\prime}$

but I don't remember how far I got with it, or whether the definition coincides with yours

[Matthew Ballard]

What about an inductive construction where you induct on the length of the complex(es)? Or maybe this is what you have already?

[Scott Morrison]

@Matthew Ballard, I'm not even sure what this would mean. The definition of the tensor product on objects and morphisms is straightforward:

/-- The tensor product of graded objects `X` and `Y` is, in each degree `i`,
the biproduct over `a + b = i` of `X a ⊗ Y b`. -/
def tensorObj (X Y : GradedObject ℕ V) (i : ℕ) : V :=
  biproduct (fun p : Finset.Nat.antidiagonal i => (X p.1.1) ⊗ (Y p.1.2))

/-- The tensor product of morphisms between graded objects is the diagonal map
consisting of tensor products of components. -/
def tensorHom {W X Y Z : GradedObject ℕ V} (f : W ⟶ X) (g : Y ⟶ Z) :
    tensorObj W Y ⟶ tensorObj X Z :=
  fun _ => biproduct.map fun p => f p.1.1 ⊗ g p.1.2

The associator I can at least write down (see branch#monoidal_complex, in Mathlib.CategoryTheory.GradedObject.Monoidal) but then the pentagon equation seems nightmarish.

[Scott Morrison]

I guess I'm hoping to summon a sealed horror from nlab that will tell me a cheap way to do this, at the price of some nonsense about extensions or coends or ... :-)

[Joël Riou]

I did not manage to compile the monoidal_complex branch, but my guess is that we would need suitable ext lemmas (but it seems that the MonoidalPreadditive API provides these) so that it should reduce to a computation on each indivual term W p ⊗ X q ⊗ Y r ⊗ Z s, and then we would need suitable lemmas which would identity the restriction of the associator maps on these, and for that the most annoying thing is that we may have to use arithmetical identities, like the associativity of the addition in the natural numbers. (I have encountered related issues when I studied the cochain complex of abelian groups of morphisms from a cochain complex to another.)

[Scott Morrison]

I will try to get the branch working for you, sorry!

[Scott Morrison]

The necessary ext lemmas are there, but I could not convince simp to actually deal with all the resulting biproduct.ι and biproduct.πs that appear. The naturality of biproduct.lift/desc seems to get in the way of having a simp normal form that goes all the way --- although I'm certainly not saying this is impossible, just intimidating. :-)

[Kevin Buzzard]

I had to prove some lemmas about biproducts when I was translating the LFTCM20 category theory exercises into Lean 4 for the students in Copenhagen, and it struck me that they have this same property as cohomology of a complex -- they're both a limit and a colimit, which makes them interesting to work with :-)

[Scott Morrison]

I fixed the badly botched merge on branch#monoidal_complex, and it is compiling again now.

[Kevin Buzzard]

I thought for too long about speeding up mathlib and now I have to spend a week or so doing real life things like reading PhD theses so I can examine them, but my naive thoughts on this matter say that the right ext lemma just reduces you to checking everything on pure tensors a x b x c x d where it is hopefully rfl. What is wrong with my thought experiment?

[Scott Morrison]

By themselves all the ext lemmas do is make things more complicated: they introduce lots of "inclusion into this summand" and "projection onto this summand" morphisms at either either of the big composite of morphisms.

We then need simp to actually combine those with the structural maps (e.g. distributors, biproduct reindexing maps, etc) so that we actually get down to something about pure tensors. This is far from working at the moment.

Possibly we also need "ext lemmas on the inside", i.e. to locate places in the middle of the composition where we "visit" a large direct sum, and insert that fact that the identity is the sum over of the index set of the biproduct.π _ j ≫ biproduct.ι _ j maps, which will hopefully then induce further simplification as these maps hit the structural morphisms on the inside. But this hopefully isn't essentially: naturality should hopefully propagate the biproduct.ιs inwards from the left and the biproduct.πs inwards from the right until they actually meet in the middle and annihilate.

However with ~18 morphisms on the LHS of the pentagon, and ~12 on the RHS, we are asking a lot of simp normal form to successfully push the extra morphisms introduced by ext all the way through. Apparently asking too much at present!

[Scott Morrison]

A typical place where the current simp set gets stuck is something that looks schematically like:

biproduct.ι _ j ≫ biproduct.lift _ (fun i => biproduct.π _ k ≫ z)

If k did not depend on i, then by "naturality" we could pull the biproduct.π out of the biproduct.lift, after which it would annihilate with the biproduct.ι via biproduct.ι_π_assoc. However it does depend, so the only choice seems to be to push the biproduct.ι inside the the biproduct.lift, which seems slightly scary. Perhaps it is okay to always do this? Or should we only do it when we can see that there is a biproduct.π already inside the biproduct.lift for it to collide with?

(Sorry, writing this without the branch open, may be nonsensical. :-)

[Scott Morrison]

As a general principal, lemmas "pushing biproduct.ι to the right" (and dually pushing biproduct.π to the left) are pretty easy to justify, so maybe we should just be braver.

[Matthew Ballard]

Sorry what I meant boils down the following. I rarely need much more than

• we know this construction on whatever objects we are building chain complexes with
• it commutes with colimits
• it takes cones to cones

Usually statements I care about are closed under those operations so you get a reduction quickly.

What can you say about the full subcategory where the pentagon equality holds?

[Joël Riou]

Using the strategy I had suggested above (where I would like to stress the importance of the arithmetical identities, here the associativity in the natural numbers), I have reduced the pentagon identity to a very basic equational lemma for the associator. Then, in principle, it should not be too hard to complete the proof. See branch#monoidal_complex_jriou https://github.com/leanprover-community/mathlib4/blob/monoidal_complex_jriou/Mathlib/CategoryTheory/GradedObject/Monoidal.lean

(It is certainly better for me not to work more on this anytime soon: I am in Chennai working on a non-math project...)

[Scott Morrison]

Thank you @Joël Riou, that made it much more manageable. I needed to add quite a bit of further API for biproduct, but I've now finished the proof of the pentagon equation.

[Scott Morrison]

For now I've just pushed to your branch, and left it in a fairly messy state, but hopefully soon I will do the unitors as well (hopefully much much easier!) and clean up.

[Scott Morrison]

Oh -- and the abstract nonsense words I was probably looking for earlier are "Day convolution", although I'm not sure you actually get any savings on the monoidal structure by generalizing in that direction.

[Joël Riou]

I have refactored @Scott Morrison's PR #6379 as #7389, which is still a draft, but the first PR out of it #7425 is ready. In order to construct the tensor product on graded objects by an additive monoid I in a category C, I extend the tensor product on C to a functor GradedObject I C ⥤ GradedObject I C ⥤ GradedObject (I × I) C and then I use the "pushforward" by the addition I × I → I which is a functor GradedObject (I × I) C ⥤ GradedObject I C. Eventually, if X₁ X₂ : GradedObject I C, (X₁ ⊗ X₂) j is the coproduct of the X₁ i₁ ⊗ X₂ i₂ for i₁ + i₂ = j. The associator (X₁ ⊗ X₂) ⊗ X₃ ≅ X₁ ⊗ (X₂ ⊗ X₃) is obtained by showing that in degree j, both sides identifies to a coproduct indexed by triples (i₁, i₂, i₃) such that i₁ + i₂ + i₃ = j (this is the most technical part of the construction https://github.com/leanprover-community/mathlib4/blob/graded-monoidal/Mathlib/CategoryTheory/GradedObject/Trifunctor.lean#L245-L246 which is done more generally for trifunctors obtained by composing bifunctors). The pentagon relation is now obtained in a much cleaner way than I initially did: https://github.com/leanprover-community/mathlib4/blob/graded-monoidal/Mathlib/CategoryTheory/GradedObject/Monoidal.lean#L577-L611 (the proof is now mostly a sequence of rw, and no longer a series of lemmas in a random order).

Using @Eric Wieser's #7237 it should be relatively easy to deduce the monoidal structure on chain complexes in an additive monoidal category. I have made as little assumptions as possible so that eventually this could also be used to get a monoidal structure on unbounded complexes.

[Eric Wieser]

I'm consistently impressed by how often someone else ends up needing something I only just worked on

[Eric Wieser]

(and vice versa!)

[Kevin Buzzard]

This was first flagged in the class group paper several years ago; it is a surprisingly common phenomenon.

Screenshot-from-2023-09-29-08-52-25.png

This is precisely the big edge that mathlib has over things like AFP.

[Eric Wieser]

Eric Wieser said:

I had a branch somewhere that worked with (the ring structure implied by) graded tensor products in ZMod 2 [snip] but I don't remember how far I got with it, or whether the definition coincides with yours

This is now sorry-free in #7394

[Antoine Chambert-Loir]

Can one apply this work on the categorical part of mathlib to the type theoretic part? use graded objects in categories to redefine/handle GradedModule, etc.?

[Eric Wieser]

If nothing else it would be good to show a link between the two approaches

[Antoine Chambert-Loir]

The questions is whether we do need to have two approaches.

1. Many typeclasses in mathlib give rise naturally to categories, in the mathematical sense.
   docs#AddMonoid with docs#AddMonoidHom, docs#Module with docs#LinearMap (the latter category being parameterized by a docs#Semiring), etc.
   It is certainly important to define systematically as such the categories that already exist in mathlib.

2. Probably, very generic type classes (such as docs#AddMonoidHomClass) will imply that some category is of an important type (additive, monoidal, etc.) and here as well, some relation has to be stated.

3. Some constructions can be stated at a categorical level (graded objects, for example), and certainly the relation should be done, but it would also be important to be able to inherit automatically from the categorical results.

4. Maybe this can be incorporated in a general hierarchy builder such as the one that @Cyril Cohen and his coauthors proposed for Coq. I believe it would be great to incorporate that effort into mathlib.

[Eric Wieser]

Note that right now, inheriting in full generality from category theoretic results is impossible; the category-theoretic results are less universe-polymorphic than the Type counterparts (you can't build a morphism between modules in different universes)

[Eric Wieser]

Of course, you could fairly argue that the polymorphism is (mostly) worthless, and those who need it should just suffer through some extra ULifts

[Scott Morrison]

As @Eric Wieser might remember from slim_check, I'd prefer we don't let desiring more universe polymorphism get in the way of ... well, anything.

[Eric Wieser]

I think a more realistic example of why we can't use the category theory library for everything is that AFAIK there's no direct analog to is_scalar_tower, because the things we'd want to quantify over are bundled

[Antoine Chambert-Loir]

IsScalarTower R A M is not very far from what mathematicians do implicitly when they consider modules M over an R-algebra A

[Antoine Chambert-Loir]

And I'm not arguing that everything should be done automatically.
One could imagine a system that gives you what it can do, and asks you about the rest.