Singular homology of the sphere

Stream: homology

[Brendan Seamas Murphy]

I have formally verified a calculation in Lean of the singular homology group Hₖ(∂Δⁿ; R) for all n, k, and (nonzero) coefficient rings R!
image.png
image.png
image.png
image.png
image.png

[Brendan Seamas Murphy]

Code is here https://github.com/Shamrock-Frost/BrouwerFixedPoint

[Brendan Seamas Murphy]

I intend to prove that any nonempty convex compact set in the plane is homeomorphic to the unit ball and use this to calculate H_k(S^n) and prove the Brouwer fixed point theorem (and then I promise I will start PRing!)

[Adam Topaz]

Great work! I look forward to those PRs ;)

[Junyan Xu]

That's great news!
I wonder what comm_ring buys you over add_comm_group though. Apparently the universal coefficient theorem for homology can be stated (and holds) for any abelian group.
As for the homeomorphism proof, it feels like you could make use of the stuff around docs#gauge, but no results explicitly about continuity is stated in the file (of course continuity and bijectivity suffice for homeomorphism between two compact spaces). @Yaël Dillies probably knows the way to go. (By the way, you would need to exclude the degenerate case, as an interval is also a nonempty convex compact set, or maybe you mean the unit ball of the same dimension as the affine span of the convex set.)

[Brendan Seamas Murphy]

Ah sorry, I meant to say "with nonempty interior" (that's how it's stated in the reference I was looking at, introduction to topological manifolds by Lee). For the comm_ring thing, it was a pretty uninformed design decision at the start of the project. I was just thinking that I usually only use ring coefficients and that I'd like homology to be a functor into R-Mod when R is a ring (which I couldn't see how to do without baking it into the defintion)

[Brendan Seamas Murphy]

I also meant to say "in R^n" and not "in the plane"... I am currently infected with covid and feeling a little loopy :sneezing:

[Yaël Dillies]

Hey! I'm afraid I don't know more than what is in analysis.convex.gauge.

[Yaël Dillies]

But just for your information I still have plans to prove Kakutani's fixed point theorem from Sperner's lemma. Can the homological approach prove that too?

[Junyan Xu]

There's a "Correspondence between open convex sets and positive continuous sublinear functions" at the bottom of https://en.m.wikipedia.org/wiki/Minkowski_functional#CITEREFNariciBeckenstein2011 that should go into the gauge file.

[Moritz Doll]

It's funny, we did not need anything about continuity of Minkowski functionals for proving the equivalence of with_seminorm and is_locally_convex and I had thought we will never need the continuity results then

[Moritz Doll]

Yaël Dillies said:

But just for your information I still have plans to prove Kakutani's fixed point theorem from Sperner's lemma. Can the homological approach prove that too?

yeah, that should is possible: you can upgrade Brouwer's fixed point theorem to Schauder's fixed point theorem and then to Kakutani's. I forgot what the details were, but I co-supervised this for a Bachelor's thesis so it can't be that hard