## Stream: Lean Together 2021

### Topic: the sphere (Heather's talk)

#### Johan Commelin (Jan 04 2021 at 15:23):

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 (Jan 04 2021 at 15:28):

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

#### Heather Macbeth (Jan 04 2021 at 15:29):

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

#### Kevin Buzzard (Jan 04 2021 at 15:29):

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 (Jan 04 2021 at 15:32):

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

#### Adam Topaz (Jan 04 2021 at 15:34):

HoTT's spheres are not manifolds, right?

#### Heather Macbeth (Jan 04 2021 at 15:35):

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

#### Heather Macbeth (Jan 04 2021 at 15:36):

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

#### Kevin Buzzard (Jan 04 2021 at 15:49):

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 (Jan 04 2021 at 15:53):

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 (Jan 04 2021 at 16:00):

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


#### Adam Topaz (Jan 04 2021 at 16:01):

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 (Jan 04 2021 at 16:03):

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 (Jan 04 2021 at 16:04):

In HoTT the homotopy levels start at -2.

#### Reid Barton (Jan 04 2021 at 16:07):

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 (Jan 06 2021 at 03:46):

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 (Jan 06 2021 at 03:46):

@Reid Barton @Johan Commelin

Last updated: May 08 2021 at 21:09 UTC