homotopy groups of spheres

Stream: Is there code for X?

[Kevin Buzzard]

Do we have enough machinery to define (not compute, just define) homotopy groups of $n$-spheres? Here by an $n$-sphere I mean of course what any set theorist would mean, namely the following:

-- To define the set you need a not-necessarily-computable sum `finsum`
-- and a noncomputable type `ℝ` with the API of a monoid.
import algebra.big_operators.finprod -- definition of `monoid` and `finsum`
import data.real.basic -- definition of `ℝ`and monoid structure (and some other things)

def real_n_sphere (n : ℕ) : Type
:= {x : fin n.succ → ℝ | finsum (λ i, (x i) *(x i)) = 1}

and if you want any structure I'll just let you know the right imports, for example we can offer you

import algebra.big_operators.finprod -- definition of `finsum`
import data.real.basic -- definition of `ℝ`
import topology.basic -- definition ot `topological_space`
-- without the next import, type class inference doesn't work, but I did not debug further than `Pi.topological_space`
import topology.metric_space.basic
import topology.constructions -- where both the instances we need are defined.

def real_n_sphere (n : ℕ) : Type
:= {x : fin n.succ → ℝ | finsum (λ i, (x i) *(x i)) = 1}

variable (n : ℕ)
noncomputable instance some_model_of_R_to_the_n_plus_one : topological_space (fin n.succ → ℝ) := Pi.topological_space

noncomputable
instance real_n_sphere.topological_space (n : ℕ) : topological_space (real_n_sphere n) :=
subtype.topological_space

How close are we of being able to define (not compute) the additive group $\pi_4(S^3)$? How close are we to being able to compute it? Note that Brunerie claims to prove $\pi_4(S^3)=\N/2$ for some value of $=$ (and by refl as I understand it -- this is such a beautiful equation, I think we should call the maths statement "Brunerie's equation", Euler's $e^{i\pi}+1=0$ covered 0 and 1 so maybe this is the next one). However I think that the $S^3$ that Brunerie is talking about when they say they have a term of some type in homotopy type theory is a much more combinatorial object than the one in the Lean code above. I am trying to work out what it means to "join up the stories" between these rival definitions of spheres, but I am independently interested in whether we can define homotopy groups of our spheres yet. Would this make a nice summer project? And where does the work of @Joseph Myers fit into all this?

[Kevin Buzzard]

Does someone out there know who first proved in pdf form that $\pi_4(S^3)=\N/2$? @Floris van Doorn I am no historian

[Kevin Buzzard]

@Mario Carneiro can we turn Brunerie's HoTT proof into a Lean proof, like you turned a metamath Dirichlet's theorem into a Lean one?

[Mario Carneiro]

One would need a model of HoTT in topological spaces, and it is not clear to me whether this actually exists. The category of topological spaces is ill-behaved in some ways and I'm not sure about all the details.

If it is possible to build a model of HoTT in lean, especially one that allows one to deduce statements about vanilla topological spaces (as compared to using simplicial sets). I would very much like to see it in mathlib. If there are any HoTT folks in the chat I'd love to collaborate on this.

[Mario Carneiro]

We would also need some stuff on infinity cats, I am not sure how far along this work is in mathlib.

[Adam Topaz]

You probably don't need infinity cats, but just simplicial sets

[Mario Carneiro]

Infinity cats (or more likely infinity groupoids) would come up if you define generic HoTT models (which would be another way to dodge the problem while setting up a full import/translation)

[Adam Topaz]

To translate between simplicial sets and topological spaces, I guess we would need the statement that the geometric realization of the singular simplicial set is homotopy equivalent to the given space

[Adam Topaz]

Oh yeah, I understand, I'm mostly thinking about the algebraic topology applications that Kevin asked for. And yes I agree that to fully model HoTT we would need some sort of infinity cats

[Mario Carneiro]

If we can fix on a single HoTT model of particular interest (like the one that says things about topological spaces), then we don't need as much of the higher category theory stuff

[Mario Carneiro]

especially since a full HoTT model comparable to the thing lean 2 implements might actually be too big to fit in lean

[Mario Carneiro]

so you would be forced to do a shallow embedding / "interpretation" to some extent

[Adam Topaz]

I think the simplicial set model (if I recall correctly, Voevodsky constructed this?) Is the natural one.

[Mario Carneiro]

I agree, but my impression was that this is a little too combinatorial, it doesn't really talk about continuous spaces in the same sense as in topology

[Adam Topaz]

And to obtain results about actual spaces, there's a Quillen equivalence with Top

[Mario Carneiro]

I wonder what that quillen equivalence looks like if you take out the categories from the statement and make them implicit

[Adam Topaz]

(Ping @Jakob Scholbach who might be interested in this too)

[Mario Carneiro]

In the best case, if we can build a (possibly implicit) HoTT model / interpretation in lean together with this quillen equivalence to deduce plain topological statements, we can get a custom tactic mode to work in the model and then we can do HoTT in mathlib the "right" way

[Floris van Doorn]

The first HoTT proof of computing pi_4(S^3) was given by Guillaume Brunerie. Note that he has not formalized his proof, he only gave a paper proof (and technically, there is still a hole in his proof, namely that the smash product forms a 1-coherent symmetric monoidal category - Definition 4.1.1 in his thesis).

Cubical type theory should in principle be able to prove that $\pi_4(S^3)=\Z/2\Z$ by (roughly) refl. However, so far this proof has only given (the equivalent of) the memory consumption exceeded error. Once you want to compute with everything you've proven, you have to not only give a correct proof, but also one that results in an efficient program, and that turns out to be hard.

[Kevin Buzzard]

But can we give a mathematical proof using the topological model that the Brunerie constant Is 2 for the topological 3-sphere and then deduce it's true for simplicial ("HoTT") spheres using a comparison theorem

[Mario Carneiro]

true, but then what would be the point of the HoTT side of the theorem?

[Mario Carneiro]

that's just proving the theorem directly

[Kevin Buzzard]

Can we define homotopy groups of spheres in the sense of Joseph Myers?

[Joseph Myers]

metric.sphere is defined for any metric space, with any centre and radius, so you can use that in either euclidean_space ℝ (fin n) or the abstract Euclidean affine space [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] to define your set of points (and thus topological subspace). (We also have the smooth manifold structure for a sphere, see geometry.manifold.instances.sphere.) We don't yet have bundled spheres for Euclidean geometry, but those aren't relevant here (they'd be more relevant for talking explicitly about power of a point, tangency, poles and polars, etc.).

[Reid Barton]

I would guess $\pi_4(S^3) = \mathbb{Z}/2$ was probably first proved by Pontryagin, though I don't think he used the pdf file format specifically.