Universal coefficient theorem

Stream: Is there code for X?

[Edison Xie]

Do we have universal coefficient theorem in current mathlib (i.e do we have the exact sequence:
$0 \to M \otimes_{\mathbb{Z}} H_n(G, \mathbb{Z}) \to H_n(G, M) \to Tor_1^{\mathbb{Z}}(M, H_{n-1}(G, \mathbb{Z})) \to 0$ for a $\mathbb{Z}$-mod $M$ with trivial $G$ action) ?

[Michael Rothgang]

I think the answer depends on what H_n is. In a very abstract setting, mathlib certainly has the homology of a complex, and derived functors. (Does it have the Tor functor already? I'm not sure; @Joël Riou probably knows.)

As far as I know, this hasn't really been specialised to e.g. H_n being singular homology. Mathlib barely has the definition of singular homology; I imagine the long exact sequence (from the Eilenberg-Steenrod axioms) would be easy to prove. You may need to prove that abelian groups always have a projective resolution of length 2, for example. I don't know to what extend the universal coefficient theorem can be abstracted to a more general setting --- or if you also need to work in the concrete setting.

[Michael Rothgang]

I would certainly love to see this result in mathlib, algebraic topology is very under-developed!

[Jz Pan]

That seems to be group homology.

[Joël Riou]

Mathlib has a definition of Tor, but we cannot prove much with it. It will take a certain time before we get the tensor product on the derived category of the category of R-modules (but I am working on it, for example #22539 will be used to construct functorial flat resolutions, which will eventually allow deriving the tensor product). The exact sequence above could be obtained as a consequence of a spectral sequence relating the homology of M ⊗^L K (with K a complex) and modules Tor_q (H_n K, M), because in the case of integers, the global dimension 1 (mentionned by @Michael Rothgang) implies that there will only be two nonzero consecutive rows (or colums) in the spectral sequence, so that it simplifies as a family of short exact sequences.

[Kevin Buzzard]

I think Amelia is slowly PRing group homology (see for example #21766 )

[Edison Xie]

Joël Riou said:

The exact sequence above could be obtained as a consequence of a spectral sequence relating the homology of M ⊗^L K (with K a complex) and modules Tor_q (H_n K, M), because in the case of integers, the global dimension 1 (mentionned by Michael Rothgang) implies that there will only be two nonzero consecutive rows (or colums) in the spectral sequence, so that it simplifies as a family of short exact sequences.

Do we have spectral sequences? I remember @Andrew Yang said he's gonna make it at some point, is there any progress on that?

[Joël Riou]

I have a full implementation of spectral sequences (see https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/Algebra/Homology/SpectralSequence/Examples/Grothendieck.lean for the Grothendieck spectral sequence of composition of derived functors), but it will take a certain time before it enters mathlib.

[Andrew Yang]

No I don't have any plans on it. The formalization in that repo looks very promising! Though I recall there is a more abstract theory using exact couples that applies not only to double complexes but to e.g. filtered complexes. I wonder if we would want them in that generality? Or is that formulation too incompatible with the current design (where we talk explicitly about complexes and not a differential object in some random category)?

[Joël Riou]

Andrew Yang said:

No I don't have any plans on it. The formalization in that repo looks very promising! Though I recall there is a more abstract theory using exact couples that applies not only to double complexes but to e.g. filtered complexes. I wonder if we would want them in that generality? Or is that formulation too incompatible with the current design (where we talk explicitly about complexes and not a differential object in some random category)?

My formalization obviously applies to filtered complexes as well! (And in the future, it will also apply to filtered spectra in stable homotopy...)
I am using the formalism of spectral objects (in triangulated categories, and in abelian category). A spectral sequence is attached to any spectral object in an abelian category (and I already have the API to construct such a spectral object from a filtered complex). In the literature, there is another construction of spectral sequences using exact couples (which contain slightly less information than spectral objects), but I have chosen this approach because everything in the spectral sequence (each page, the page at infinity, convergence, etc) can be described quite directly in terms of the spectral object (while in the case of exact couple, there is only an inductive construction as far as I know).

[Andrew Yang]

Ah I see it now. Then it's fantastic. I was just mislead by spectralSequenceNat (u : ℤ × ℤ) : ComplexShape (ℕ × ℕ) on the top of the file.