Zulip Chat Archive

Hi, I'm new to Lean and I noticed that there doesn't seem to be a whole lot of algebraic topology. I'd like to contribute by adding definitions for homology and homotopy groups and proving some main results. I think it would make sense to start by introducing some basic category-theoretic definitions, such as the category of pointed spaces, the category of pairs, and the category of pointed pairs. Where would be a good place to make these definitions? Maybe in topology.category.Top.basic?

Yaël Dillies (Nov 10 2021 at 19:18):

^ @Shing Tak Lam

Johan Commelin (Nov 10 2021 at 20:18):

@Jonathan Welcome! There's some stuff there, but there's certainly a lot of low-hanging fruit as well. We have simplicial sets, and there's a bunch of abstract homological algebraic. (E.g. computing homology of a chain complex.)
Shing has been adding homotopies, and there's an open PR with the definition of π₁. It would be good to coordinate with him.

Johan Commelin (Nov 10 2021 at 20:19):

Defining those categories that you suggest sounds like a useful thing to do.

Jonathan (Nov 10 2021 at 20:35):

Johan Commelin said:

Jonathan Welcome! There's some stuff there, but there's certainly a lot of low-hanging fruit as well. We have simplicial sets, and there's a bunch of abstract homological algebraic. (E.g. computing homology of a chain complex.)
Shing has been adding homotopies, and there's an open PR with the definition of π₁. It would be good to coordinate with him.

Thanks for the pointers! I'll get in touch with him

Scott Morrison (Nov 10 2021 at 21:14):

We have over categories and arrow categories, and these should probably be used when defining the category of pointed spaces, and possibly when defining the category of pairs.

Jonathan (Nov 10 2021 at 23:12):

Ah yes, seems like under categories are perfect for the category of pointed spaces. Is there a preferred single-point space in existence, or should I define one?

Adam Topaz (Nov 10 2021 at 23:22):

@Jonathan it depends how explicit you want to be. If you're in category theory land, you can use a noncomputable terminal object using docs#category_theory.limits.terminal