shift of complexes

Stream: condensed mathematics

[Johan Commelin]

if we want to implement shift of complexes correctly, we have to flip all the differentials by a - sign. This requires add_comm_group on the hom sets. @Scott Morrison @Bhavik Mehta what is the current status here?

[Riccardo Brasca]

You mean between normed groups ? They already are additive groups

instance : add_comm_group (normed_group_hom V₁ V₂)

They also have a norm (I'm going to make them a normed group later this week)

[Johan Commelin]

Well, I was thinking for complexes with objects from an arbitrary category

[Johan Commelin]

So we need some sort of preadditive category, I guess

[Bhavik Mehta]

docs#category_theory.preadditive

[Bhavik Mehta]

This is exactly add_comm_group on the homsets with the sensible composition structure :)

[Adam Topaz]

And noremdgroup already has this instance @Johan Commelin

[Adam Topaz]

I added it as part of the definition of the completion of a system of complexes (completion has an additive functor instance, which assumed preadditivity on the source and target)

[Johan Commelin]

Awesome!

[Johan Commelin]

I pushed a has_shift instance to the jmc-complex branch

[Kevin Buzzard]

Wait what? Shifting a complex changes d by a sign? This doesn't even change the complex up to isomorphism. Is this just some convention?

[Johan Commelin]

https://stacks.math.columbia.edu/tag/0119

[Johan Commelin]

I will immediately admit that I haven't thoroughly studied the literature to know whether this is a common convention

[Kevin Buzzard]

So do the boundary maps change sign if you shift?

[Adam Topaz]

yes

[Damiano Testa]

For what its worth, I would also think that there can be a sign associated to a shift, depending on conventions, and I would normally imagine it to be there. This is related to the fact that several squares in homotopies, usually commute "up to signs", which sometimes are there, sometimes not...

[Adam Topaz]

But note this is incompatible with mathlib's shift for chain complexes

[Johan Commelin]

Yes, but we are redesigning chain complexes anayway...

[Adam Topaz]

Yeah, exactly, you either introduce a sign here, or somewhere else

[Damiano Testa]

Yes, there is a lingering sign, and you can push it around, but you have to get to grips with it at some point.

[Julian Külshammer]

My impression is also that having a sign in the shift is the most common convention.

[Adam Topaz]

If you look at that stacks project page, there's a good explanation for the sign arising from homotopy of morphisms of complexes

[Kevin Buzzard]

I noticed in Amelia's work on tensor product of chain complexes that her degree n term was sum(i+j=n) Ci tensor Dj, which looks fine, but then the differentials specifically chose one of i and j in the sense that they twist by (-1)^i. This means that tensor product of complexes is slightly less symmetric than you might think, but of course it's all fine up to isomorphism

[Julian Külshammer]

For tensor products, Koszul sign convention is a great way to remember at least most of the signs.

[Damiano Testa]

I am not really sure whether this is actually the case, but, when working with complexes, there is the Euler characteristic that always permeates everything. For it, you assign different sign choices to "even" and "odd" degrees. I think that the usual sign convention on the shift is the one compatible with choosing a + sign for the even terms.

Not entirely sure of this, but I store it like this in my mind.

[Johan Commelin]

(I just pushed has_shift for system_of_complexes)

[Adam Topaz]

@Johan Commelin You might want to use docs#category_theory.equivalence.congr_right for the functor.has_shift instance

[Adam Topaz]

def functor.has_shift (C D : Type*) [category C] [category D] [has_shift D] :
  has_shift (C ⥤ D) := has_shift.mk $ (shift _).congr_right

[Johan Commelin]

@Adam Topaz Please refactor!

[Adam Topaz]

done!

[Johan Commelin]

now we need lemmas that say that if the system M is (weak) bounded exact in degrees le m, then M[k] is (weak) bounded exact in degrees le m+k

[Johan Commelin]

To do that, we'll need the isom between C[n]_i and C_{n+i}

[Johan Commelin]

Should we just do this hands on, or does someone see a nice way to build an API for maps of degree n?

[Adam Topaz]

I wonder whether we can come up with something like an "induction principle" for C[n]?

[Johan Commelin]

We should

[Johan Commelin]

I just pushed a little bit about shifts and bounded exactness.

[Johan Commelin]

It feels like we hit all the DTT pain all over again

[Adam Topaz]

If all the DTT hell is encapsulated in one proof of some induction principle and the user never has to see it, then maybe it's not that bad?

[Johan Commelin]

I agree. But we have to find the correct statements

[Kevin Buzzard]

I think the best way of finding them is by just pressing on and seeing what we run into rather than theorising. We seem to have agreed on a definition involving changing the sign of the d's, so now we can start on the theorems. NB I don't care that we can't shift exact seqences of monoids, they are not the correct objects I don't think, at least right now. My impression is that exact sequences are the correct object when there is some kind of canonical isomorphism between isomorphism classes of subobjects of an object and isomorphism classes of quotient objects of the object (this is what the concept of a short exact sequence encapsulates somehow), and this is true for abelian groups and R-modules but not true for abelian monoids.

The other point of view: note that for monoids there is only one way to shift -- you don't change any signs. For groups this "naive shift" is isomorphic to the proposed (-d) shift, but the analogue of this isomorphism (which is multiplication by -1 on each odd C_i) does not exist for monoids. In some sense this is an argument for not twisting d, on the grounds that it is the more natural construction as it works in more generality. I went through all this hell once, with different people using different notations: class field theory can be normalised in two different ways, so Shimura varieties can be normalised in two different ways, there are geometric and arithmetic frobenius and Tate modules of elliptic curves vs etale cohomology. Writing BDJ was a lot of work because of all these dualities, especially when some people did not clarify which normalisations they were using.

[Johan Commelin]

I agree that there are arguments both ways. But for now, I'm inclined to stick with the "mathsy" convention, until we find a need for shifts of complexes of monoids.

[Kevin Buzzard]

I think that this is a very pragmatic response -- the sign convention must be there for a reason and we should trust those who have thought hard about it. My impression of the arithmetic v geometric normalisation of class field theory and hence the theory of Shimura varieties was that the people like Deligne doing etale cohomology of Shimura varieties wanted one convention because it made the signs come out nicer in their formulas for char polys, and the people doing things like Heegner points wanted in many cases the other convention because they were explicitly interested in rational points where Artin's convention worked better. There is no one best answer -- this is why Wikipedia's article on canonical maps is basically so rubbish