Zulip Chat Archive

Stream: maths

Topic: homology


view this post on Zulip Kenny Lau (Aug 21 2018 at 15:00):

what is the progress of simplicial/singular homology?

view this post on Zulip Kevin Buzzard (Aug 21 2018 at 17:19):

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

view this post on Zulip Reid Barton (Aug 21 2018 at 17:38):

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.

view this post on Zulip Reid Barton (Aug 21 2018 at 17:53):

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.

view this post on Zulip Reid Barton (Aug 21 2018 at 17:55):

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

view this post on Zulip Johan Commelin (Aug 21 2018 at 18:00):

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

view this post on Zulip Johan Commelin (Aug 21 2018 at 18:00):

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

view this post on Zulip Johan Commelin (Aug 21 2018 at 18:38):

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

view this post on Zulip Kenny Lau (Aug 21 2018 at 18:38):

not really

view this post on Zulip Patrick Massot (Aug 21 2018 at 20:34):

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.


Last updated: May 14 2021 at 18:28 UTC