Status of actual homology theory

Stream: homology

[Patrick Massot]

I see many commits in Mathlib about abstract homology but I have no idea where we stand when it comes to actual homological theories. Do we have singular (co)homology in Mathlib? Do we have any of the standard corollaries of existence of a (co)homology theory for topological spaces?

[Kevin Buzzard]

The word "homology" is often being used generally just to mean "kernel of d quotiented by image of d for an arbitrary complex of abelian groups" rather than an actual homology theory.

[Patrick Massot]

That's why I'm asking about singular homology.

[Junyan Xu]

I think vaguely recall that Brendan Murphy's work is still waiting for @Joël Riou's refactor: redefinition of homology + derived categories #4197 to enter mathlib.

[Patrick Massot]

More importantly, I'm asking about corollaries. It is well known from any textbook on algebraic topology that there is a list of standard corollaries that will follow from the existence of any reasonable theory for topological spaces. For instance if you know there are functors $H_n$ from topological space to abelian groups for every $n$ that you can compute for Euclidean spaces and spheres then you get a bunch of corollaries.

[Patrick Massot]

Even better, the computations for Euclidean spaces and spheres follow from homotopy invariance and Mayer-Vietoris without any extra input.

[Junyan Xu]

I think the $H_n$ s are gonna be constructed as a derived functor ...

(Hmm, is that the plan? https://mathoverflow.net/questions/66401/singular-homology-cohomology-as-a-derived-functor doesn't have a definitive answer apparently.)

[Adam Topaz]

This is clearly the right point of view: "Quillen thought of homology as "derived abelianisation""

[Adam Topaz]

(from the last answer on that MO page)

[Patrick Massot]

Does that make anything easier?

[Patrick Massot]

The painful points of singular homology are very clearly identified. Suffering comes from subdividing stuff. The main example is barycentric subdivisions, but there are also prism subdivisions. That that magically goes away with derived functors? If yes, where does pain migrate?

[Junyan Xu]

I guess you'd get the long exact sequence from the general machinery. Probably other Eilenberg-Steenrod axioms still require hard work. Brendan talked about the "very very annoying" barycentric subdivision around 22:44 in his talk. Not sure whether he proved all the axioms; he says he computed homology of spheres in an ad-hoc way. HOL Light apparently has all the axioms (page 36).

[Patrick Massot]

What I had in mind as the painful points is the content of page 37 in Harrison's talk.

[Junyan Xu]

Apparently Brendan got homotopy invariance from the acyclic models theorem, circumventing prismatic subdivision. Excision is from barycentric subdivision (this is about simplicial sets, right? Is it in mathlib yet?).

[Yaël Dillies]

FWIW I am thinking of formalising the chromatic number of the Kneser graph assuming Borsuk-Ulam as an axiom (or more precisely using a [BorsukUlam] assumption, where class BorsukUlam has a field containing the statement of Borsuk-Ulam).

[Yaël Dillies]

Then I don't have to wait for homology computations to catch up.

[Joël Riou]

About the homology refactor, it is mostly done (after about 60 PR). For example, we already have the snake lemma docs#CategoryTheory.ShortComplex.SnakeInput.snake_lemma and the homology sequence attached to an exact sequence of homological complexes will soon follow (cc @Brendan Seamas Murphy). An API is also developed for doing computations in categories of abelian groups or categories of modules, and it shall soon be used by @Amelia Livingston in order to identify group cohomology in low degree.

Then, there should no longer be any significant obstacle for the development of singular homology of topological spaces X in mathlib, by defining the simplicial set Sing X, applying the free abelian group functor, taking the alternating face map complex, and finally homology.

[Joël Riou]

The last significant PR of the homology refactor is #8706. After that, it will be possible to remove the old homology API (after double-checking that all statements of the old API also exists in some form in the new API).

[Johan Commelin]

This is a massive milestone! Awesome work!

[Johan Commelin]

What I like about this PR is that the API got a lot larger, but the places where the API gets used, the proofs/defs/constructions mostly become shorter.