glueing complexes

Stream: mathlib4

[Kevin Buzzard]

There is a complex docs#groupCohomology.inhomogeneousCochains which computes cohomology of a group and it looks like $A_0\to A_1\to A_2\to \cdots$. There is another complex docs#groupHomology.inhomogeneousChains which computes homology of a group and it looks like $\cdots\to B_2\to B_1\to B_0$ (the arrows are the other way because one of these complexes has type ChainComplex and the other has type CochainComplex).

If the group is furthermore finite then Tate wrote down a map $B_0\to A_0$ and could thus glue the complexes together to make a new complex $(C_n)$ indexed by $n\in\Z$ with $C_n=A_n$ for $n\geq0$ and $C_{-1-n}=B_n$ for $n\geq0$. The cohomology of $C_n$ is called Tate cohomology of the finite group.

In the currently secret class field theory repo (going live next month to coincide with the Clay class field theory workshop in Oxford) Richard Hill glues these complexes together. We now want to claim that the cohomology of $C_n$ in positive degree is obviously group cohomology, with the proof being ker(C_{n+1}->C_{n+2})/im(C_n->C_{n+1})=ker(A_{n+1}->A_{n+2})/im(A_n->A_{n+1}) because C_n is defined to equal A_n for n>=0. Here is some code doing this gluing and stating what we want:

import Mathlib

open CategoryTheory Limits groupCohomology groupHomology Rep LinearMap

variable {R : Type} [CommRing R]
variable {G : Type} [Group G] [Finite G] [DecidableEq G]

noncomputable section

namespace groupCohomology

-- we have a definition of this in the repo but it's irrelevant
def TateNorm (M : Rep R G) : (inhomogeneousChains M).X 0 ⟶ (inhomogeneousCochains M).X 0 := sorry

def TateComplex (M : Rep R G) : CochainComplex (ModuleCat R) ℤ where
  X
  | Int.ofNat n => (inhomogeneousCochains M).X n
  | Int.negSucc n => (inhomogeneousChains M).X n
  d
  | Int.ofNat i, Int.ofNat j            => (inhomogeneousCochains M).d i j
  | Int.ofNat _, Int.negSucc _          => 0
  | -1,0                                => TateNorm M
  | -1, Int.ofNat (j + 1)               => 0
  | -1, Int.negSucc _                   => 0
  | Int.negSucc (i + 1), Int.ofNat j    => 0
  | Int.negSucc (i + 1), Int.negSucc j  => (inhomogeneousChains M).d (i + 1) j
  shape := sorry
  d_comp_d' i j k hij hjk := sorry

def TateComplexFunctor : Rep R G ⥤ CochainComplex (ModuleCat R) ℤ where
  obj M := TateComplex M
  map φ := {
    f
    | Int.ofNat i => ((cochainsFunctor R G).map φ).f ↑i
    | Int.negSucc i => (chainsMap (MonoidHom.id G) φ).f i
    comm' := sorry
  }
  map_id := sorry
  map_comp := sorry

def TateCohomology (n : ℤ) : Rep R G ⥤ ModuleCat R :=
  TateComplexFunctor ⋙ HomologicalComplex.homologyFunctor _ _ n

def TateCohomology.iso_groupCohomology (n : ℕ) (M : Rep R G) :
    TateCohomology (n + 1) ≅ groupCohomology.functor R G (n + 1) := by
  -- maybe?
  convert Iso.refl _
  -- aargh
  sorry

What's left is unfortunately not rfl and I think that this is because if n is a natural and then I look at the integer n+1 and apply this prev function that we use in homology theory I don't get something defeq to the image of n in $\Z$.

So two questions:
1) what is a clean way of dealing with this?
2) Should there be general API for gluing two $\mathbb{N}$-valued complexes to get a $\Z$-valued complex or is this situation I'm describing above the only time it ever happens? @Joël Riou did you say that you knew another example?

[Floris van Doorn]

One issue seems to be that after unfolding a bunch of definitions docs#CategoryTheory.ShortComplex.homologyData uses choice, which will block any computation.

[Floris van Doorn]

If computation on integers is important: you can define the predecessor function on the integers that can at least cancel n+1-1 for natural numbers n:

import Mathlib.Data.Int.Basic

def myIntPred : ℤ → ℤ := fun
  | .ofNat 0 => -1
  | .ofNat (n + 1) => n
  | .negSucc n => .negSucc (n + 1)

example (n : ℕ) : myIntPred ((n : ℤ) + 1) = n := by rfl
example (n : ℤ) : myIntPred ((n : ℤ) + 1) = n := by sorry -- this will not be rfl

[Joël Riou]

I did the API https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Homology/Embedding/Connect.html precisely so as to allow the definition of Tate cohomology! This API could be expanded though. The comparison isomorphisms in cohomology should be relatively easy in degrees different from 0 and -1. It should be possible to do that in terms of the structure ConnectData.

[Joël Riou]

The idea is that if we have h : ConnectData K L, then the stupid truncation (greater than or equal to 0) of h.cochainComplexshould identify to L. Using basic properties of homology objects of the stupid truncations (combining results in Algebra.Homology.Embedding.ExtendHomology and Embedding.RestrictionHomology), this should give the expected isomorphism in cohomology in degree $\geq 1$. (Similar arguments should apply for degrees $\leq -2$.)

[Robin Carlier]

Is it true (and if it is, do we have?) that the cochain complex of a connect data identifies to the cone of the map between a positive degree complex to a negative degree complex that the connect data seem to define? Excuse my imprecisions, but I vaguely remember being told that Tate cohomology is the "cofiber of a norm map from (derived) coinvariants to (derived) invariants", which hopefully should translate to what I ask in this case?

[Joël Riou]

Yes, there is such a result. It could be nice to formalize it at some point, but in terms of homological complexes as they are formalized, it would be slightly more indirect (and be annoying because of signs...): we would have to extend K and L from (co)chains complexes indexed by the natural numbers to cochains complexes indexed by the integers, etc.

[Joël Riou]

The computation of the homology of the "restriction" by an embedding of complex shapes is at #26535, and the computation of the homology of a glued complex is at #26520.