## Stream: condensed mathematics

### Topic: shift of complexes

#### Johan Commelin (Mar 08 2021 at 14:04):

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 (Mar 08 2021 at 14:08):

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 (Mar 08 2021 at 14:10):

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

#### Johan Commelin (Mar 08 2021 at 14:10):

So we need some sort of preadditive category, I guess

#### Bhavik Mehta (Mar 08 2021 at 14:12):

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

#### Adam Topaz (Mar 08 2021 at 14:13):

And noremdgroup already has this instance @Johan Commelin

#### Adam Topaz (Mar 08 2021 at 14:14):

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)

Awesome!

#### Johan Commelin (Mar 08 2021 at 15:04):

I pushed a has_shift instance to the jmc-complex branch

#### Kevin Buzzard (Mar 08 2021 at 15:22):

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 (Mar 08 2021 at 15:24):

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

#### Johan Commelin (Mar 08 2021 at 15:25):

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

#### Kevin Buzzard (Mar 08 2021 at 15:29):

So do the boundary maps change sign if you shift?

yes

#### Damiano Testa (Mar 08 2021 at 15:30):

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 (Mar 08 2021 at 15:30):

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

#### Johan Commelin (Mar 08 2021 at 15:30):

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

#### Adam Topaz (Mar 08 2021 at 15:30):

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

#### Damiano Testa (Mar 08 2021 at 15:31):

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 (Mar 08 2021 at 15:33):

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

#### Adam Topaz (Mar 08 2021 at 15:33):

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 (Mar 08 2021 at 15:34):

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 (Mar 08 2021 at 15:36):

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

#### Damiano Testa (Mar 08 2021 at 15:37):

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 (Mar 08 2021 at 15:49):

(I just pushed has_shift for system_of_complexes)

#### Adam Topaz (Mar 08 2021 at 15:51):

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

#### Adam Topaz (Mar 08 2021 at 15:54):

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


done!

#### Johan Commelin (Mar 08 2021 at 15:56):

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 (Mar 08 2021 at 18:34):

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

#### Johan Commelin (Mar 08 2021 at 18:35):

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 (Mar 08 2021 at 19:36):

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

We should

#### Johan Commelin (Mar 08 2021 at 20:01):

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

#### Johan Commelin (Mar 08 2021 at 20:01):

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

#### Adam Topaz (Mar 08 2021 at 20:04):

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 (Mar 08 2021 at 20:18):

I agree. But we have to find the correct statements

#### Kevin Buzzard (Mar 08 2021 at 21:59):

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 (Mar 09 2021 at 05:37):

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 (Mar 09 2021 at 07:05):

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

Last updated: May 09 2021 at 15:11 UTC