defining total complex

Stream: maths

[Jujian Zhang]

I played around with collapsing double complex into a total complex recently. The problem is because rows and columns can be indexed by either integers or natural numbers or even fin n for shorter complexes and the complex_shape of rows and columns can either be complex_shape.up or complex_shape.down. In order to not repeat too much, I toyed around the following approach:

we generalize to allow the homological bicomplex with anti-commutative squares to have a row shape $a$ indexed by $\alpha$ and a column shape $b$ indexed by $\beta$. Then we collect $\operatorname{Tot}^{\oplus}$ using a new shape $c$ on $\gamma$. To achieve this, we need a heterogeneous addition function $(+) : \alpha \to \beta \to \gamma$ such that

• for all $i, i' \in \alpha$ and $j \in \beta$, $i \to_a i'$ if and only if $i + j \to_c i' + j$;
• for all $j, j' \in \beta$ and $i \in \alpha$, $j \to_b j'$ if and only if $i+j\to_c i + j'$;
• addition is cancellative on both input: $i + j = i' + j$ if and only if $i = i'$ and $i + j = i + j'$ if and only if $j = j'$;
• if $i+j\to_c k \to_c \operatorname{succ}(i) + \operatorname{succ}(j)$ then $k$ is equal to both $\operatorname{succ}(i) + j$ and $i + \operatorname{succ}(j)$ (here successor means whatever comes next according to the complex shape, not necessarily plus one) ;

and the shapes $a, b, c$ must all be irreflexive i.e. nothing is related to themselves. Then the total differential $\bigoplus_{i+j=k}\to \bigoplus_{m+n=k'}$ is defined to be the linear map whose $(i,j)$-th projection is

$$\sum_{m=i~\mathrm{or}~n=j}\left(C_{i,j}\stackrel{D}{\to} C_{m,n}\hookrightarrow\bigoplus_{m+n=k}\right),$$

where

$$D =\left\{ \begin{aligned} d_h & & i = j \\ d_v & & m = n \\ 0 & & \text{otherwise} \end{aligned}\right..$$

The experiment can be found at https://github.com/jjaassoonn/flat/blob/master/src/bicomplex3.lean. It contains the definition of total complex according to above and instances of heterogeneous addition when row shape, column shape and result shape are all complex_shape.up nat and complex_shape.down nat. I believe it should also work for column shape indexed by fin n as long as n > 2, but I haven't formalised the proof yet.

[Kevin Buzzard]

In what generality do people need to collapse double complexes? I've only ever seen it for first quadrant complexes but then again I've only ever seen first quadrant spectral sequences in my work

[Matthew Ballard]

Sum totalization vs Prod totalization is also a thing

[Jujian Zhang]

I believe this approach can be made to a total complex by product by changing necessary universal property of direct sum to modules.

[Kevin Buzzard]

The approach seems to work for any "convex subset" of the integers

[Yaël Dillies]

Did someone say order? :D

[Kevin Buzzard]

@Johan Commelin @Adam Topaz @Joël Riou @Matthew Ballard do any of you know whether one ever has to collapse a double complex into a single complex in any setting other than a first quadrant one (with maps either all going towards the origin or away from it)? What do you think of Jujian's approach? It's pretty general and seems to work.

[Adam Topaz]

IIRC there is some spectral sequence double complex that shows up in the new stuff about THH which is not just first-quadrant

[Adam Topaz]

let me see if I can refresh my memory

[Adam Topaz]

okay, yeah, a similar double complex also exists for the usual Hochschild homology, and it's not concentrated in any quadrant. See the first few minutes of this arizona winter school lecture: https://arizona.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=647315c3-a74f-4971-90a3-aa05016008f6

[Joël Riou]

Signs can be annoying... It seems that in the literature, both differentials on bicomplexes tend to commute rather than anticommute, and instead, signs are introduced in the definition of the total complex. For example, it is so in the Stacks project https://stacks.math.columbia.edu/tag/0FNB and in Verdier's Des catégories dérivées des catégories abéliennes.

I have already used total complexes of bicomplexes which spans over only finitely with columns, but each column can be unbounded on both sides, so that it is not in any quadrant. (For example, take a morphism f of complexes, consider it as a bicomplex with two columns: the total complex identifies to the cone of f.)

[Jujian Zhang]

In the above approach, if we change $D$ to be

$$D =\left\{ \begin{aligned} d_h & & i = j \\ i \bullet d_v & & m = n \\ 0 & & \text{otherwise} \end{aligned}\right.,$$

then we can ask the double complex to be commutative as usual (I will experiment this later). $i \bullet x$ can be made to be alternating like this:

class has_sign :=
(sign : α → zmod 2)
(rel : ∀ (i i' : α), a.rel i i' → sign i ≠ sign i')

instance [has_sign a] (T : Type*) [has_neg T] : has_smul α T :=
{ smul := λ x f, if has_sign.sign a x = 0 then f else - f }

[Joël Riou]

But then, the definition of bicomplexes could be more simple, like:

abbreviation homological_bicomplex :=
  homological_complex (homological_complex V a) b

[Jujian Zhang]

Yes, I spelled it out because I don’t want choose between chain of rows or chain of columns.

[Jujian Zhang]

Joël Riou said:

But then, the definition of bicomplexes could be more simple, like:

abbreviation homological_bicomplex :=
  homological_complex (homological_complex V a) b

I will experiment to see if this approach can be adapted to chain of chains by changing the definition of $D$ to incorporate signs.

[Matthew Ballard]

Adam Topaz said:

okay, yeah, a similar double complex also exists for the usual Hochschild homology, and it's not concentrated in any quadrant. See the first few minutes of this arizona winter school lecture: https://arizona.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=647315c3-a74f-4971-90a3-aa05016008f6

Funny $HH_\ast$ is the example you give. That was the one most fresh in my mind. $\bigoplus$-totalization and $\prod$-totalization can give difference answers.

Another example, similar to what @Joël Riou mentioned: given two complexes $C^\bullet$ and $D^\bullet$ the complex $Hom^n(C^\bullet, D^\bullet) = \prod_{j-i =n} \operatorname{Hom}(C^i,D^j)$ with $D \phi = d_D \phi \pm \phi d_C$ is a natural one to consider as $H^0$ computes homotopy classes of chain maps.

It seems like there is a lot of space between constructions of graded things and things happening with complexes.

[Scott Morrison]

Any time you want to take the tensor product of finitely supported \int-indexed complexes you're not in the first quadrant case.

[Scott Morrison]

The complexes appearing in link homology are all \int-indexed, not \nat, and you spend a lot of time taking tensor products of them. In fact there they are really indexed in an \int-torsor, although most people manage to ignore this.

[Kevin Buzzard]

Oh interesting! Jujian pointed out that what he did also seemed to with for \int-torsors, although to collapse a double complex to a single complex you need an "addition" map A x B to C where A,B,C are your indexing sets. Jujian has axiomatised what you need from this map in order to get d^2=0 from the collapsed complex

[Scott Morrison]

For link homology, one of the gradings is naturally by framings of a tangle. These have an "obvious" addition map coming from gluing endpoints of tangles together! Sadly you won't find this in the literature, where instead people perform violence.

[David Loeffler]

Do any of you know whether one ever has to collapse a double complex into a single complex in any setting other than a first quadrant one (with maps either all going towards the origin or away from it)

@Kevin: perhaps you should ask my PhD supervisor (whoever that was), who once instructed me to read a paper by Ash--Stevens about p-adic modular forms, which definitely involved a second-quadrant spectral sequence relating group cohomology and tensor products. (It was something like $Tor_{-j}^R(H^i(G, M), R / I) \Longrightarrow H^{i-j}(G, M / IM)$, where M is an $R$-flat $R[G]$ module ; very likely I have misremembered the indices and/or signs, but it definitely was in one of the "off" quadrants).

[Kevin Buzzard]

I told you to read it precisely so you could tell me what was in it

[Jujian Zhang]

I have tested at here that this approach also works when double complex is defined as

def homological_bicomplex (a : complex_shape α) (b : complex_shape β) :=
  homological_complex (homological_complex V a) b

(So the squares are commutative now instead of anticommutative.)

In this case $D$ is defined as

$$D =\left\{ \begin{aligned} d_h & & i = j \\ j \bullet d_v & & m = n \\ 0 & & \text{otherwise} \end{aligned}\right.,$$

with the help of has_sign class

class has_sign (a : complex_shape α) :=
(sign : α → zmod 2)
(rel : ∀ (i i' : α), a.rel i i' → sign i ≠ sign i')

@[reducible]
def complex_shape.smul (i : α)  (f : T) [has_neg T] : T :=
if has_sign.sign a i = 0 then f else - f

[Adam Topaz]

Have we given any thought to generalizing complex_shape itself to accommodate double (triple, etc.) complexes as well?

[Johan Commelin]

I think we discussed it somewhere in #condensed mathematics...

[Kevin Buzzard]

It seemed to me when I talked about this with Jujian that a double complex really was not a complex_shape in some sense (for example d^2 isn't zero if one of the d's is horizontal and the other is vertical and they compose). Right now I was envisaging just having a typeclass for double complexes and one for triple complexes when we actually need them, a bit like quotient_induction_on\3 rather than quotient_induction_on_n. It's hard to imagine us needing quadru-complexes any time soon...

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/complexes.2C.20d.2C.20dtt contains a lot of discussions about how painful homological algebra was in mathlib a few years ago

[Joël Riou]

About the signs conventions, the most correct reference is the introduction to Brian Conrad's Grothendieck Duality and Base Change, and it seems that for him, the horizontal and vertical differentials anticommute (see page 7). Then, eventually, I would think it is very much ok to define double complexes like this, but it would be convenient to have equivalences with the "recursive definition".
Once a definition is fixed, I think that the major fact we should prove about bicomplexes is that the total complex is filtered (with the stupid filtration on rows (or columns)), and the graded pieces identify to the individual rows (resp. columns) up to shifts. This is the basis of some dévissages that one usually does using spectral sequences (or long exact homology exact).

[Kevin Buzzard]

I'm not an expert in this area. It seems to me that given a complex of complexes, choosing whether to use (-1)^i or (-1)^j when making the double complex anticommute will change the sign of some maps, and hence perhaps do things like "change the orientation of the cohomology groups". Does this make any sense?

[Joël Riou]

If you have a complex of complexes, the horiz. and vert. differentials commute. Then, in order to get an "anticommuting bicomplex", we have to change some signs, and for that, Conrad's says we should multiply by $(-1)^p$ the differentials in the pth column. (When I had to deal with precise signs on étale cohomology when writing chapters of a book on the works by Ofer Gabber, he was referring to this book by Conrad, so that it is safe to assume that these signs conventions are good!)

[Kevin Buzzard]

I'm just saying that if you have a complex of complexes, take the transpose and then apply this sign convention to get a double complex, it's a different answer to applying the sign convention and then taking the transpose.

[Joël Riou]

Yes, sure!

[Kevin Buzzard]

And I'm asking if this matters :-) I think the upshot is that when you collapse the double complex to a single complex, 50% of the d's have changed sign.

[Joël Riou]

Even though the signs are changed, the two total complex you would get are still isomorphic (on the term corresponding to (i, j), multiply the identity by $(-1)^{ij}$). This is the way the symmetry iso K ⊗ L ≅ L ⊗ K of the tensor product of chain complexes is defined, and this is also related to the signs in the "graded commutativity" (i.e. commutativity up to some signs) of some cohomology algebras.

So, I do not think it matters too much, but when it enters mathlib4, it would be better if the signs conventions are the same as in Conrad's book.

[Joël Riou]

I have experimented further. Since Scott and I have worked on tensor products of graded objects (see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Tensor.20products.20of.20graded.20objects.20.2F.20chain.20complexes/near/393807746 ), I have tried to check the compatibilities that are needed in order to lift the monoidal structure on graded objects to homological complexes. The definition of the tensor product is very much related to the construction of an extension to complexes HomologicalComplex C₁ c₁ ⥤ HomologicalComplex C₂ c₂ ⥤ HomologicalComplex C c of a functor F : C₁ ⥤ C₂ ⥤ C: given two complexes K₁ and K₂, we consider the double complex (i₁, i₂) => F(K₁ i₁, K₂ i₂), and want to take the total complex. (For the tensor product of complexes, we apply this with F : C ⥤ C ⥤ C the tensor product on a monoidal category C.)

[Joël Riou]

In this situation, what we easily get is a "commuting page" F(K₁ i₁, K₂ i₂) which can be considered as an object in HomologicalComplex (HomologicalComplex C₂ c₂) c₁ (for which Scott has already written some API in mathlib: see Algebra.Homology.Flip.) Let us denote this category HomologicalComplex₂ C c₁ c₂. To do this, we do not yet need choices of signs. Then, for K : HomologicalComplex₂ C c₁ c₂, we have to attach a total complex in HomologicalComplex C c. This needs a map I₁ × I₂ → I on the underlying index sets of the shapes c₁, c₂, c, some compatibilities and the introduction of choices of signs for the horizontal/vertical differentials in the total complex. I have found slightly weaker conditions as @Jujian Zhang, see the definition of [TotalComplexShape c₁ c₂ c] in https://github.com/leanprover-community/mathlib4/blob/chain-complex-monoidal/Mathlib/Algebra/Homology/ComplexShapeExtra.lean#L13-L22

[Joël Riou]

Then, I would think that "anticommuting" bicomplexes are only a not so necessary intermediate step between "commuting" bicomplexes and their total complexes: it is not more difficult to define directly the total complex of a "commuting" bicomplex.

[Joël Riou]

I have developed this further in order to formulate the symmetry of the total complex with the flip, the associativity, braiding and symmetry of the tensor product of complexes, see https://github.com/leanprover-community/mathlib4/blob/chain-complex-monoidal/Mathlib/Algebra/Homology/Symmetry.lean For the associativity, I have developed a "heterogeneous" version which should allow to get isomorphisms like HOM(K ⊗ L, M) ≅ HOM(K, HOM(L, M)) on internal Hom of complexes which are sometimes referred to as "isomorphisme cher à Cartan" in French.