## Stream: new members

### Topic: algebraic topology

#### Jonathan (Nov 10 2021 at 19:09):

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?

^ @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

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

(there is a nice notation for this: ⊤_ , see
https://github.com/leanprover-community/mathlib/blob/3c2bc2e797d010b8c0b5ea13fb404b9c4213bf3b/src/category_theory/limits/shapes/terminal.lean#L141

#### Adam Topaz (Nov 10 2021 at 23:24):

Alternatively, I think docs#punit should have a topology instance, so you could use Top.of punit for the "explicit" single-point space.

#### Adam Topaz (Nov 10 2021 at 23:26):

docs#punit.topological_space

#### Scott Morrison (Nov 10 2021 at 23:38):

I would encourage using ⊤_ , and perhaps make the definition of pointed C for any C with a terminal object, not just Top!

#### Scott Morrison (Nov 10 2021 at 23:41):

https://ncatlab.org/nlab/show/pointed+object could keep one busy for a while!

#### Adam Topaz (Nov 10 2021 at 23:46):

In general it would be nice to build up a theory for concrete categories where the forgetful functor is representable.

#### Scott Morrison (Nov 10 2021 at 23:54):

The random issue bot just mentioned @Bhavik Mehta's previous effort in this direction #7436. I agree it would be nice to revive / continue this!

#### Johan Commelin (Nov 11 2021 at 06:29):

@Jonathan :up:

Last updated: Dec 20 2023 at 11:08 UTC