## Stream: homology

### Topic: Singular homology of the sphere

#### Brendan Seamas Murphy (Aug 27 2022 at 23:54):

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 (Aug 27 2022 at 23:57):

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 (Aug 28 2022 at 01:20):

Great work! I look forward to those PRs ;)

#### Junyan Xu (Aug 28 2022 at 01:51):

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 (Aug 28 2022 at 02:15):

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 (Aug 28 2022 at 02:21):

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 (Aug 28 2022 at 06:33):

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

#### Yaël Dillies (Aug 28 2022 at 06:33):

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 (Aug 28 2022 at 07:55):

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 (Aug 29 2022 at 00:28):

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 (Aug 29 2022 at 00:30):

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

Last updated: Dec 20 2023 at 11:08 UTC