Constructing loops

Stream: sphere eversion

[Patrick Massot]

After the preliminaries of chapter 1 comes the first section which is specific to the project: Section 1.3 Constructing loops. It is the topic of this Lean file. The first lemma is proved. The next targets involve using the previous section (all definitions and statements should already be there) and gluing continuous functions using continuous cut-off functions. This can be tackled by anyone knowing, or wanting to learn, the basic topology part of mathlib (basic means no uniform space of nonarchimedean topological algebra).

[Floris van Doorn]

I'll take a look at this!

[Oliver Nash]

Awesome!

[Floris van Doorn]

I just pushed a partial proof for Lem 1.11 (local_loops).
I ran into 2 issues:

• In the Lean file Lem 1.9 is formulated using continuous_on and Lem 1.11 is formulated using continuous_at in the conclusion. continuous_on does not apply continuous_at for all points (only for the points in the interior). Since $\gamma^t$ is allowed to have garbage values if $t\not\in I$ I presume we want to use continuous_on (or continuous_within_at), right?
• I don't see the math proof that $\gamma_x\in \Omega_x$. Just checking: $\Omega$ being open over a neighborhood $U$ of $x_0$ just means that the slices $\Omega_x$ are open (in $F$) for $x\in U$, right? So in particular we don't know whether $(x_0,\beta(x_0))$ (or $(x_0,\gamma(s))$, with $\gamma$ as in the proof) lies in the interior of $\Omega$, right? I don't see what prevents the following problematic example:
  • $\Omega_{x_0}$ is all of $F$
  • $\Omega_x$ is a tiny open region for $x\ne x_0$
  • The $\gamma$ we get in the proof has a range that goes far outside the tiny open regions $\Omega_x$.

[Oliver Nash]

Nice work :-) I'll have to context switch to think properly about your remarks but if they're still unanswered this evening, I'll do so!

[Oliver Nash]

I spent a bit too long working on #9657 this morning so I'm now grovelling around with finite sets trying to close the sorrys in https://github.com/leanprover-community/sphere-eversion/pull/26.

[Patrick Massot]

Floris van Doorn said:

• In the Lean file Lem 1.9 is formulated using continuous_on and Lem 1.11 is formulated using continuous_at in the conclusion. continuous_on does not apply continuous_at for all points (only for the points in the interior). Since $\gamma^t$ is allowed to have garbage values if $t\not\in I$ I presume we want to use continuous_on (or continuous_within_at), right?

This is a typo, it should be continuous_on everywhere. In the real work everything is defined only on I, there is no garbage value anywhere.

[Patrick Massot]

Floris van Doorn said:

• I don't see the math proof that $\gamma_x\in \Omega_x$. Just checking: $\Omega$ being open over a neighborhood $U$ of $x_0$ just means that the slices $\Omega_x$ are open (in $F$) for $x\in U$, right?

No. "over" always refer to the projection of $\pi : E \times F \to E$ (because we always secretly think everything is a fiber bundle). So $\Omega$ over a neighborhood of $x$ mean $\Omega \cap \pi^{-1}(U)$ for some neighborhood $U$ of $x$.

[Patrick Massot]

Of course this kind of sloppy wording based on implicit habits is part of the motivation for formal maths. To me this was completely clear, just as things were completely clear for the author of those notes on adic spaces that drove me crazy during the perfectoid spaces project...

[Floris van Doorn]

Ah ok, so in Lemma 1.11 $\Omega \cap \pi^{-1}(U)$ is open for some open neighborhood $U$ of $x_0$? Part of the confusion was that the formalized statement of the lemma didn't state this. I'll fix it tomorrow.

[Floris van Doorn]

@Patrick Massot what do you think the best way to formulate Lemma 1.11 is?
I currently have

lemma local_loops
  {x₀ : E}
  (hΩ_op : ∃ U ∈ 𝓝 x₀, is_open (Ω ∩ prod.fst ⁻¹' U))
  (hΩ_conn : ∀ᶠ x in 𝓝 x₀, is_connected (prod.mk x ⁻¹' Ω))
  (hg : ∀ᶠ x in 𝓝 x₀, continuous_at g x) (hb : ∀ᶠ x in 𝓝 x₀, continuous_at b x)
  (hb_in : ∀ᶠ x in 𝓝 x₀, (x, b x) ∈ Ω)
  (hconv : ∀ᶠ x in 𝓝 x₀, g x ∈ convex_hull ℝ (prod.mk x ⁻¹' Ω)) :
∃ (γ : E → ℝ → loop F), (∃ (U ∈ 𝓝 x₀), continuous_on ↿γ (set.prod U $ set.prod I univ)) ∧
  ∀ᶠ x in 𝓝 x₀, ∀ (t ∈ I) s,
  (x, γ x t s) ∈ Ω ∧
  γ x 0 s = b x ∧
  (γ x 1).surrounds (g x)

Is there a better way to formulate hΩ_conn? (this works fine for the proof so far).
I'm not sure how to formulate the conclusion most easily. I'm wondering if we should have continuous_at_filter similar to docs#measurable_at_filter.

[Patrick Massot]

Your formulation looks fine.

[Patrick Massot]

About continuous_at_filter, do you want to replace ∀ᶠ x in 𝓝 x₀, continuous_at g x with continuous_at_filter g (𝓝 x₀)? It doesn't seem to buy you much.

[Floris van Doorn]

No, continuous_at_filter g (𝓝 x₀) would mean∃ U ∈ 𝓝 x₀, continuous_on g U, which should (slightly) simplify the continuity statement in the conclusion.

[Patrick Massot]

Ok, that would rather be continuous_on_filter then.

[Patrick Massot]

Except that in this case it wouldn't apply.

[Patrick Massot]

Because the conclusion uses a more complicated set built from a neighborhood.

[Floris van Doorn]

I expect you can take the product with some pure filters. But yeah, it's wouldn't buy much.

[Patrick Massot]

Maybe we should drop I from this statement. You can probably arrange all those assumptions to hold for every t and that could actually make the proof easier.

[Floris van Doorn]

I just finished the proof of Lemma 1.13, satisfied_or_refund.

[Oliver Nash]

Oh wow, that's awesome!

[Kevin Buzzard]

That's a fine name for a lemma I must say

[Patrick Massot]

Amazing!

[Patrick Massot]

Don't hesitate to update the TeX code if you want to add details to the informal proof.

[Floris van Doorn]

I have pushed a mostly finished proof of local_loops. It still depends on the following sorry'd lemma

lemma is_open_affine_independent {ι} : is_open {p : ι → F | affine_independent ℝ p}

Is this something that is easy to prove?

[Patrick Massot]

Hopefully you should be able to use @Oliver Nash recent effort to link this to determinant and use continuity of determinants.

[Oliver Nash]

Yes, this is very easy from what I have.

[Oliver Nash]

I'm back from holidays and busy preparing some "camera-ready" version of a paper but I'll see if I can fill that sorry for you quickly now.

[Patrick Massot]

Nice, what is this paper about?

[Oliver Nash]

I waffle on about Lie algebras in Mathlib.

[Oliver Nash]

I was delighted that it was accepted for CPP which was very pleasing.

[Johan Commelin]

I would love to see the preprint

[Floris van Doorn]

Good luck with the camera-ready version of your CPP paper!

[Oliver Nash]

I'll share a link once I have it. I have only tiny changes to make but I might as well avoid having multiple versions floating around.

[Oliver Nash]

@Floris van Doorn
I'm currently this far along with your question:

import topology.algebra.matrix
import analysis.normed_space.add_torsor_bases
import topology.algebra.ring

open set function finite_dimensional fintype
open_locale topological_space affine classical matrix
noncomputable theory

variables (ι k V P : Type*)
variables [fintype ι] [nondiscrete_normed_field k] [complete_space k]
variables [normed_group V] [metric_space P] [normed_add_torsor V P]
variables [normed_space k V] [finite_dimensional k V]

lemma is_open_affine_bases (h : card ι = finrank k V + 1) :
  is_open { v : ι → P | affine_independent k v ∧ affine_span k (range v) = ⊤ } :=
begin
  obtain ⟨b : affine_basis ι k P⟩ := affine_basis.exists_affine_basis_of_finite_dimensional h,
  simp_rw [← b.is_unit_to_matrix_iff, matrix.is_unit_iff_is_unit_det, is_unit_iff_ne_zero],
  let f := matrix.det ∘ b.to_matrix,
  have hb : continuous (b.to_matrix : (ι → P) → (matrix ι ι k)), { continuity, },
  have hf : continuous f, { exact (continuous_det).comp hb, },
  change is_open (f⁻¹' {0}ᶜ),
  apply hf.is_open_preimage,
  simp only [is_open_compl_iff],
  exact t1_space.t1 0,
end

[Oliver Nash]

needs significant tidy up --- I'll keep going.

[Oliver Nash]

but hopefully gives the idea

[Floris van Doorn]

It's great to hear that you have basically proven is_open_affine_independent. Then we can almost mark local_loops as done!

[Oliver Nash]

Yep, we're close.

[Oliver Nash]

@Floris van Doorn I edited the snippet and the above is now sorry-free (though still a mess).

[Oliver Nash]

OK I've just edited again and the conclusion is now exactly what you wanted, namely is_open { v : ι → P | affine_independent k v }.

[Oliver Nash]

I won't have time to polish this up for a day or two so feel free to PR it in my place if you so wish. Otherwise I'll come back to it (most likely on Wednesday).

[Patrick Massot]

I love how work on this project magically happen while I'm talking to undergrad students.

[Sebastien Gouezel]

Can I complain that this is not the right generality? You shouldn't need that the space is finite-dimensional, nor that the cardinality of iota is the dimension of the space. As we already have the general version for vector spaces (see docs#is_open_set_of_linear_independent), I hope the general affine version can be deduced easily from it. Of course, it can not use the determinant trick.

[Oliver Nash]

You can of course, make this complaint, especially since I was thinking the same thing as I wrote the above.

[Oliver Nash]

I'll make sure the version that lands in Mathlib is stated with appropriate assumptions.

[Oliver Nash]

I was not aware of docs#is_open_set_of_linear_independent --- this is useful.

[Sebastien Gouezel]

What I really mean is: if the affine version is easy to deduce from the linear version we already have, then please do it. Otherwise, don't bother and stay with the finite-dimensional version if it's enough for your needs. No need to overgeneralize if it would only slow you down.

[Oliver Nash]

Understood.

[Floris van Doorn]

I also missed docs#is_open_set_of_linear_independent when I was looking earlier. I think that the reduction is not that hard.

[Floris van Doorn]

I managed to do the reduction:

lemma is_open_affine_independent {𝕜 E ι : Type*} [nondiscrete_normed_field 𝕜]
  [normed_group E] [normed_space 𝕜 E] [complete_space 𝕜] [fintype ι] :
  is_open {p : ι → F | affine_independent ℝ p} :=
begin
  classical,
  cases is_empty_or_nonempty ι, { resetI, exact is_open_discrete _ },
  obtain ⟨i₀⟩ := h,
  simp_rw [affine_independent_iff_linear_independent_vsub ℝ _ i₀],
  let ι' := {x // x ≠ i₀},
  haveI : fintype ι' := subtype.fintype _,
  convert_to
    is_open ((λ (p : ι → F) (i : ι'), p i -ᵥ p i₀) ⁻¹' {p : ι' → F | linear_independent ℝ p}),
  refine is_open.preimage _ is_open_set_of_linear_independent,
  refine continuous_pi (λ i', continuous.vsub (continuous_apply i') $ continuous_apply i₀),
end

[Floris van Doorn]

local_loops is done! I double checked that the only axiom it used is the sorry in smooth_surrounding.

[Patrick Massot]

@Floris van Doorn I should have warned you that I modified the statement of exists_loop slightly (and haven't updated the blueprint yet). The new statement no longer assumes each $\Omega_x$ is connected. The new statement should save some work in total. Also, I don't understand why we still need a exists_loop' now that U is gone.

[Floris van Doorn]

Oh good point. Now that U is gone, I'll try to put my proof sketch in exists_loop.