homology

Stream: maths

[Kenny Lau]

what is the progress of simplicial/singular homology?

[Kevin Buzzard]

I guess Luca Gerolla is doing fundamental groups and that's all I know.

[Reid Barton]

I think Johan Commelin has been refactoring the construction of singular homology (https://github.com/leanprover/mathlib/pull/144) in category-theoretic terms, but he's currently on vacation AFAIK.

[Reid Barton]

Obvious goals would be to prove that simplicial homology satisfies the Eilenberg-Steenrod axioms (homotopy invariance, additivity, dimension axiom etc.) I don't think anyone has taken a crack at this. I'm not even sure of the best way to organize the theory here--this is one question I'm very interested in.

[Reid Barton]

My feeling is that typing Hatcher into Lean is probably not the best approach.

[Johan Commelin]

Right, I haven't been doing much Lean the last two weeks. This should change, next week in Orsay (-;

[Johan Commelin]

Also, I've been looking into too many different directions in Lean. I should get back to the homology project (-;

[Johan Commelin]

@Kenny Lau Was there something specific you were looking for or aiming at?

[Kenny Lau]

not really

[Patrick Massot]

My feeling is that typing Hatcher into Lean is probably not the best approach.

From a fun project perspective, typing parts of Hatcher could be nice, but this is certainly not the way to go for mathlib. Hatcher is too pedagogical. We certainly need something more abstract and systematic. What Johan did is already more abstract, since it's based on simplicial sets. But clearly we also need abstract homological algebra for lots of other stuff.