## Stream: maths

### Topic: boundary of a manifold

#### Johan Commelin (Aug 17 2020 at 05:09):

@Sebastien Gouezel how hard would it be to define the boundary of a manifold, as manifold, in lean?

#### Sebastien Gouezel (Aug 17 2020 at 07:12):

It woudn't be harder than in maths. But the problem is that it's nontrivial in maths: you need to know that a local homeo of the upper half space maps the boundary to the boundary, which is not easy (it should be a close cousin of the invariance of domain theorem)

#### Kenny Lau (Aug 17 2020 at 07:19):

can't you just compare the local homology? if you remove a point on the boundary you get no homology, but if you remove a point not on the boundary you get (n-1)th homology

#### Johan Commelin (Aug 17 2020 at 07:20):

Kenny, sure that sounds very easy to do in mathlib (-;

#### Kenny Lau (Aug 17 2020 at 07:20):

time to discretize homology?

#### Johan Commelin (Aug 17 2020 at 07:20):

What do you mean?

#### Kenny Lau (Aug 17 2020 at 07:21):

let's make homology computable or something like that

#### Kenny Lau (Aug 17 2020 at 07:21):

isn't that the whole point of CW-complex

#### Kenny Lau (Aug 17 2020 at 07:21):

and simplicial complex

Sure

#### Kenny Lau (Aug 17 2020 at 07:21):

if you remove a point on the interior you can deformation retract to S^(n-1)

#### Kenny Lau (Aug 17 2020 at 07:22):

which is nothing more than $\partial \Delta^n$

#### Kenny Lau (Aug 17 2020 at 07:22):

can we take homology of a simplicial set?

#### Kenny Lau (Aug 17 2020 at 07:23):

given a simplicial set (mathlib-sset!) $X_n$ consider the free abelian group generated by $X_n$ and do the usual thing with kernel quotient image?

does this work?

#### Johan Commelin (Aug 17 2020 at 07:24):

Kenny Lau said:

let's make homology computable or something like that

(Un)fortunately finsupp.add_comm_group is noncomputable

#### Kenny Lau (Aug 17 2020 at 07:24):

I mean, the whole theory of homology could be formalized right? It isn't like it involves some handwavy arguments

#### Kenny Lau (Aug 17 2020 at 07:24):

that's not what I mean by computable

#### Johan Commelin (Aug 17 2020 at 07:25):

Ooh, if that's not what you meant, than all the definitions are already there in mathlib:sset

#### Kenny Lau (Aug 17 2020 at 07:25):

you have in mathlib:sset the homology of a simplicial set?

Yup

#### Kenny Lau (Aug 17 2020 at 07:25):

I thought I just made it up 10 seconds ago

#### Johan Commelin (Aug 17 2020 at 07:26):

Also the singular simplicial set associated with a X : Top and the geometric realization of a simplicial set.

#### Johan Commelin (Aug 17 2020 at 07:26):

I'm working on showing that it is an adjunction.

#### Kenny Lau (Aug 17 2020 at 07:28):

wow your sset branch is really impressive

#### Kenny Lau (Aug 17 2020 at 07:28):

now we need the five lemma to show that the homologies agree

#### Kenny Lau (Aug 17 2020 at 07:29):

or we can just use the usual MV proof to compute the homology of S^(n-1)

#### Johan Commelin (Aug 17 2020 at 07:30):

Five lemma is around the corner (right?, @Markus Himmel)

#### Johan Commelin (Aug 17 2020 at 07:32):

@Kenny Lau The adjunction is not so easy... I think I might need to zoom out and use more abstract nonsense.

#### Markus Himmel (Aug 17 2020 at 07:33):

Johan Commelin said:

Five lemma is around the corner (right?, Markus Himmel)

It's not currently on my personal roadmap, so if anyone really wants it, feel free to select one of the options I described in #3803 and work on it.

#### Sebastien Gouezel (Aug 17 2020 at 07:34):

Yes, the standard proof is by homology, but you need to know that the version of homology you use is invariant under homeos. So homology of finite simplicial sets is not enough, and one should use singular homology (or Cech cohomology). There's also an elementary proof relying only on Brouwer at https://terrytao.wordpress.com/tag/invariance-of-domain/

Last updated: May 06 2021 at 18:20 UTC