Zulip Chat Archive

Stream: Lean Together 2021

Topic: the sphere (Heather's talk)


view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Jan 04 2021 at 15:28):

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

view this post on Zulip Heather Macbeth (Jan 04 2021 at 15:29):

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

view this post on Zulip 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".

view this post on Zulip Heather Macbeth (Jan 04 2021 at 15:32):

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

view this post on Zulip Adam Topaz (Jan 04 2021 at 15:34):

HoTT's spheres are not manifolds, right?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)(-2)-dimensional sphere is.

view this post on Zulip Adam Topaz (Jan 04 2021 at 16:04):

In HoTT the homotopy levels start at -2.

view this post on Zulip Reid Barton (Jan 04 2021 at 16:07):

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 nn and kk it can be done, but not(?) uniformly

view this post on Zulip 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 :)

view this post on Zulip Heather Macbeth (Jan 06 2021 at 03:46):

@Reid Barton @Johan Commelin


Last updated: May 08 2021 at 21:09 UTC