Zulip Chat Archive

Stream: sphere eversion

Topic: Gromov's theorem

Floris van Doorn (Aug 25 2022 at 15:55):

I modified the statement of the h-principle so that it is relative and C^0-dense. Does this seem right?
In particular: do we want to be relative to a specified closed set in the domain M and a specified closed set in the parameter space P?

/-- An arbitrary distance on `J¹(M, M')`. -/
@[reducible] def some_dist : has_dist (one_jet_bundle I M I' M') :=
-- some garbage; obtained from metrizability

/-- A relation `R` satisfies the parametric relative C⁰-dense h-principle w.r.t. manifold `P`,
`C₁ ⊆ P`, `C₂ ⊆ M` and `ε : M → ℝ` if for every family of
formal solutions `𝓕₀` indexed by a manifold with boundary `P` that is holonomic near `C₁` and `C₂`,
there is a homotopy `𝓕` between `𝓕₀` and a holonomic solution,
in such a way that `𝓕` is constant near `C₁` and `C₂` and `ε`-close to `𝓕₀`.
Note: `ε`-closeness is measured using an arbitrary distance function obtained from the metrizability
of `J¹(M, M')`. Potentially we prefer to have this w.r.t. an arbitrary compatible metric.
def rel_mfld.satisfies_h_principle_with (R : rel_mfld I M I' M') (C₁ : set P) (C₂ : set M)
  (ε : M  ) : Prop :=
 𝓕₀ : family_formal_sol IP P R, -- given a family of formal solutions with parameters in `P`
(∀ᶠ s in 𝓝ˢ C₁, (𝓕₀ s).to_one_jet_sec.is_holonomic)  -- holonomic near `C₁` of parameter space
(∀ᶠ x in 𝓝ˢ C₂,  s, (𝓕₀ s).to_one_jet_sec.is_holonomic_at x)  -- and near set `C₂` of the domain
 𝓕 : family_formal_sol (𝓘(, ).prod IP) ( × P) R, -- then there is a homotopy of such families
  ( s, 𝓕 (0, s) = 𝓕₀ s)  -- that agrees on `t = 0`
  (∀ᶠ s in 𝓝ˢ C₁,  t : , 𝓕 (t, s) = 𝓕₀ s)  -- and agrees near `C₁`
  (∀ᶠ x in 𝓝ˢ C₂,  (t : ) (s : P), 𝓕 (t, s) x = 𝓕₀ s x)  -- and agrees near `C₂`
  ( s, (𝓕 (1, s)).to_one_jet_sec.is_holonomic)  -- is holonomic everywhere for `t = 1`.
  ( (t : ) (s : P) (x : M), @dist _ some_dist (𝓕 (t, s) x) (𝓕₀ s x)  ε x) -- and close to `𝓕₀`

/-- **Gromov's Theorem** -/
theorem rel_mfld.ample.satisfies_h_principle_with (hC₁ : is_closed C₁) (hC₂ : is_closed C₂)
  (hε_pos :  x, 0 < ε x) (hε_cont : continuous ε)
  (h1 : R.ample) (h2 : is_open R) :
  R.satisfies_h_principle_with IP C₁ C₂ ε :=

Oliver Nash (Aug 25 2022 at 16:49):

I think for our application we would require the parametric version to be relative only to a closed subset of the parameter space but this is really a question for Patrick. Also, isn't it just the base map of the section of the jet bundle that has to be C0C^0 close?

Patrick Massot (Aug 25 2022 at 17:27):

In the sphere eversion application of this theorem the homotopy is not relative to a subset in M. But there is a parameter space. And the way we get rid of parameters turns parameters into elements of M somehow, so we need need to have a result relative to a subset of M in the non-parametric case. So I don't think we can gain any simplification from removing C₂

Patrick Massot (Aug 25 2022 at 17:30):

Much more importantly, Oliver is right that only the base map stays C0C^0-close.

Patrick Massot (Aug 25 2022 at 17:37):

You need to keep in mind the important example of the Bullock-Reeves theorem. This states that given any map f:RR2f : \R \to \R^2, there is a map gg which is as close as you want to ff in C0C^0 topology and whose derivative satisfies t,g(t)>50 mph\forall t, \|g'(t) \| > 50 \text{ mph}. That's because the complement of the 50 mph50 \text{ mph} ball around the origin in ample in R2\R^2. But there is no hope you can guarantee gg' stays close to ff' if f\|f'\| was very small. Note that our proof also doesn't yield any control on the acceleration of gg, which is presumably why Bullock and Reeves don't use convex integration (but they actually also give up on C0C^0 control).

Patrick Massot (Aug 25 2022 at 17:40):

Floris, I also don't understand why you want to define the has_dist (one_jet_bundle I M I' M') instead of simply defining the dist function. I guess you want to be able to start the proof with a letI and then access all metric spaces lemmas but you could do both.

Patrick Massot (Aug 25 2022 at 17:41):

In order to make the statement readable, it would also be nice to define abbreviation getting rid of all .to_one_jet_sec (unless Kyle's new dot notation tweaks allows it without doing anything, which would be awesome).

Floris van Doorn (Aug 25 2022 at 18:34):

Oh yes, of course we only get the C0C^0-closeness on the base map. I'll correct it tomorrow.
In that case I could just make M' a metric space, to have it for an arbitrary compatible metric.
Patrick, I'm not sure what you mean by "instead of simply defining the dist function".

Patrick Massot (Aug 25 2022 at 19:26):

I mean replacing @dist _ some_dist (𝓕 (t, s) x) (𝓕₀ s x) with a def. That's not very important and indeed it is probably better to think of a better way of talking about a distance function on a metrizable space.

Floris van Doorn (Aug 26 2022 at 12:20):

With the corrected version, I made the change that the target space is a metric space, so we can talk about the distance, instead of having to define (and write API for) the distance on a metrizable space.

Oliver Nash (Aug 26 2022 at 14:24):

Thanks for the updated statements, they look good to me now. We can drop the hypothesis (hC₁ : is_closed C₁) from rel_mfld.ample.satisfies_h_principle though since C₁ is irrelevant, right?

Patrick Massot (Aug 26 2022 at 14:30):

Yes, this is a copy-paste mistake, there is no parameter in that lemma.

Patrick Massot (Aug 26 2022 at 14:32):

We have a much more serious issue. The metrizable stuff is backfiring, as I feared. When applying all this to sphere eversion the target manifold is a normed space that get two metric spaces instances: one from the norm and one imposed by the statement and coming from its manifold structure.

Patrick Massot (Aug 26 2022 at 14:40):

This isn't blocking since with a have a statement for Gromov's theorem assuming a distinguished metric has been fixed. But at some point we'll need a better way to handle this.

Floris van Doorn (Aug 26 2022 at 14:41):

I was expecting something like this, so I stated the main Gromov's theorem to use an arbitrary metric space instance

Last updated: Dec 20 2023 at 11:08 UTC