Zulip Chat Archive

Stream: maths

Topic: boundary of a manifold


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 17 2020 at 07:20):

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

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:20):

time to discretize homology?

view this post on Zulip Johan Commelin (Aug 17 2020 at 07:20):

What do you mean?

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:21):

let's make homology computable or something like that

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:21):

isn't that the whole point of CW-complex

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:21):

and simplicial complex

view this post on Zulip Johan Commelin (Aug 17 2020 at 07:21):

Sure

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:21):

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

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:22):

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

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:22):

can we take homology of a simplicial set?

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:23):

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

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:23):

does this work?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:24):

that's not what I mean by computable

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:25):

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

view this post on Zulip Johan Commelin (Aug 17 2020 at 07:25):

Yup

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:25):

I thought I just made it up 10 seconds ago

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 17 2020 at 07:26):

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

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:28):

wow your sset branch is really impressive

view this post on Zulip Kenny Lau (Aug 17 2020 at 07:28):

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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Aug 17 2020 at 07:30):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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