boundary of a manifold

Stream: maths

[Johan Commelin]

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

[Sebastien Gouezel]

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]

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]

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

[Kenny Lau]

time to discretize homology?

[Johan Commelin]

What do you mean?

[Kenny Lau]

let's make homology computable or something like that

[Kenny Lau]

isn't that the whole point of CW-complex

[Kenny Lau]

and simplicial complex

[Johan Commelin]

Sure

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

can we take homology of a simplicial set?

[Kenny Lau]

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?

[Kenny Lau]

does this work?

[Johan Commelin]

Kenny Lau said:

let's make homology computable or something like that

(Un)fortunately finsupp.add_comm_group is noncomputable

[Kenny Lau]

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

[Kenny Lau]

that's not what I mean by computable

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

Yup

[Kenny Lau]

I thought I just made it up 10 seconds ago

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

wow your sset branch is really impressive

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Markus Himmel]

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]

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/