## Stream: sphere eversion

### Topic: Constructing loops

#### Patrick Massot (Oct 08 2021 at 15:34):

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 (Oct 11 2021 at 12:34):

I'll take a look at this!

Awesome!

#### Floris van Doorn (Oct 11 2021 at 15:20):

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 (Oct 11 2021 at 16:10):

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 (Oct 11 2021 at 16:11):

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 (Oct 11 2021 at 19:14):

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 (Oct 11 2021 at 19:18):

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 (Oct 11 2021 at 19:20):

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 (Oct 11 2021 at 22:39):

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 (Oct 12 2021 at 11:30):

@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 (Oct 12 2021 at 11:37): Your formulation looks fine. #### Patrick Massot (Oct 12 2021 at 11:42): 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 (Oct 12 2021 at 11:45): 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 (Oct 12 2021 at 11:47): Ok, that would rather be continuous_on_filter then. #### Patrick Massot (Oct 12 2021 at 11:47): Except that in this case it wouldn't apply. #### Patrick Massot (Oct 12 2021 at 11:47): Because the conclusion uses a more complicated set built from a neighborhood. #### Floris van Doorn (Oct 12 2021 at 11:48): I expect you can take the product with some pure filters. But yeah, it's wouldn't buy much. #### Patrick Massot (Oct 12 2021 at 12:02): 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 (Oct 22 2021 at 15:07): I just finished the proof of Lemma 1.13, satisfied_or_refund. #### Oliver Nash (Oct 22 2021 at 15:08): Oh wow, that's awesome! #### Kevin Buzzard (Oct 22 2021 at 15:10): That's a fine name for a lemma I must say #### Patrick Massot (Oct 22 2021 at 16:23): Amazing! #### Patrick Massot (Oct 22 2021 at 18:31): Don't hesitate to update the TeX code if you want to add details to the informal proof. #### Floris van Doorn (Dec 06 2021 at 14:37): 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 (Dec 06 2021 at 14:40): Hopefully you should be able to use @Oliver Nash recent effort to link this to determinant and use continuity of determinants. #### Oliver Nash (Dec 06 2021 at 14:41): Yes, this is very easy from what I have. #### Oliver Nash (Dec 06 2021 at 14:42): 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 (Dec 06 2021 at 14:45): Nice, what is this paper about? #### Oliver Nash (Dec 06 2021 at 14:46): I waffle on about Lie algebras in Mathlib. #### Oliver Nash (Dec 06 2021 at 14:46): I was delighted that it was accepted for CPP which was very pleasing. #### Johan Commelin (Dec 06 2021 at 14:59): I would love to see the preprint #### Floris van Doorn (Dec 06 2021 at 14:59): Good luck with the camera-ready version of your CPP paper! #### Oliver Nash (Dec 06 2021 at 14:59): 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 (Dec 06 2021 at 14:59): @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 (Dec 06 2021 at 15:00): needs significant tidy up --- I'll keep going. #### Oliver Nash (Dec 06 2021 at 15:00): but hopefully gives the idea #### Floris van Doorn (Dec 06 2021 at 15:01): 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 (Dec 06 2021 at 15:01): Yep, we're close. #### Oliver Nash (Dec 06 2021 at 15:09): @Floris van Doorn I edited the snippet and the above is now sorry-free (though still a mess). #### Oliver Nash (Dec 06 2021 at 15:23): 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 (Dec 06 2021 at 15:24): 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 (Dec 06 2021 at 15:39): I love how work on this project magically happen while I'm talking to undergrad students. #### Sebastien Gouezel (Dec 06 2021 at 15:45): 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 (Dec 06 2021 at 15:47): You can of course, make this complaint, especially since I was thinking the same thing as I wrote the above. #### Oliver Nash (Dec 06 2021 at 15:47): I'll make sure the version that lands in Mathlib is stated with appropriate assumptions. #### Oliver Nash (Dec 06 2021 at 15:48): I was not aware of docs#is_open_set_of_linear_independent --- this is useful. #### Sebastien Gouezel (Dec 06 2021 at 15:49): 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 (Dec 06 2021 at 15:52): Understood. #### Floris van Doorn (Dec 06 2021 at 17:00): 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 (Dec 06 2021 at 17:10): 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 (Dec 06 2021 at 17:27):

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

#### Patrick Massot (Mar 01 2022 at 20:33):

@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 (Mar 02 2022 at 10:41):

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

Last updated: Dec 20 2023 at 11:08 UTC