the sphere (Heather's talk)

Stream: Lean Together 2021

[Johan Commelin]

if you want to prove that rotations are smooth... I guess this becomes easier if you know that the sphere is a submanifold, right?

[Heather Macbeth]

Actually, I don't think the "submanifold" definition is needed for this!

[Heather Macbeth]

We already know from the construction that the inclusion map from the sphere into $\mathbb{R}^{n+1}$ is smooth.

[Kevin Buzzard]

Heather I think what your work gives is huge evidence that the manifold library is solid. This is great!

The reason I mentioned Grassmannians was for the following very silly one. We can now say "Lean has spheres!" but of course the HoTT people can reply "HoTT has spheres and furthermore they're defined in 3 lines and not 1200". Of course the difference is that a HoTT sphere is synthetic and yours are analytic, but people who are only paying a superficial interest won't be able to tell the difference. My understanding is that it is not known how to make Grassmannians synthetically -- we "don't know the generators and relations" in some sense -- so it would be something to tell someone who says "HoTT has spheres".

[Heather Macbeth]

Of course, Lean has "had spheres" for a long time. docs#metric.sphere

[Adam Topaz]

HoTT's spheres are not manifolds, right?

[Heather Macbeth]

I think, also, that Lean could be made to "have Grassmannians" in the same way, using docs#quotient.topological_space

[Heather Macbeth]

This would be a nice algebra exercise, the geometry exercise comes when you want to put a manifold structure on the Grassmannian.

[Kevin Buzzard]

Yes, HoTT's sphere are simplicial, if you like. They're inductive types, because the model in HoTT is that a type is a top space up to homotopy, whereas the model in Lean is that a type is a set.

[Kevin Buzzard]

So the claim in the HoTT systems that you can compute e.g. homotopy groups of spheres is a computation of a combinatorial nature. These results are kind of like the poster child of HoTT but what I've always been uncomfortable about is that as far as I can see they can't compute homotopy groups of things which they can't build synthetically, and my understanding it is that it's an unsolved problem as to how to do Grassmannians synthetically (or even if it can be done?)

[Kevin Buzzard]

Fixpoint Sphere (n : trunc_index)
  := match n return Type with
       | -2 ⇒ Empty
       | -1 ⇒ Empty
       | n'.+1 ⇒ Susp (Sphere n')
     end.

[Adam Topaz]

I guess it "can" be done, since it's finitely triangulizable (right?). the question is how. and whether there is an obvious simplicial model.

[Kenny Lau]

Kevin Buzzard said:

Fixpoint Sphere (n : trunc_index)
  := match n return Type with
       | -2 ⇒ Empty
       | -1 ⇒ Empty
       | n'.+1 ⇒ Susp (Sphere n')
     end.

Thanks, I was worried about what the $(-2)$-dimensional sphere is.

[Adam Topaz]

In HoTT the homotopy levels start at -2.

[Reid Barton]

Adam Topaz said:

I guess it "can" be done, since it's finitely triangulizable (right?). the question is how. and whether there is an obvious simplicial model.

For fixed $n$ and $k$ it can be done, but not(?) uniformly

[Heather Macbeth]

Inspired by sphere eversion, I checked the smoothness of the antipodal map:

lemma times_cont_mdiff_neg_sphere :
  times_cont_mdiff (𝓡 (findim ℝ E - 1)) (𝓡 (findim ℝ E - 1)) ⊤ (λ x : sphere (0:E) 1, -x) :=
(times_cont_diff_neg.times_cont_mdiff.comp times_cont_mdiff_coe_sphere).cod_restrict_sphere _

Exercise: rotations :)

[Heather Macbeth]

@Reid Barton @Johan Commelin