ContMDiff and restriction to opens

Stream: Is there code for X?

[Christian Merten]

Does the following really not exist?

import Mathlib
open TopologicalSpace

variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
  {EM : Type*} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
  {HM : Type*} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {M : Type u} [TopologicalSpace M] [ChartedSpace HM M]
  {EN : Type*} [NormedAddCommGroup EN] [NormedSpace 𝕜 EN] {HN : Type*}
  [TopologicalSpace HN] (IN : ModelWithCorners 𝕜 EN HN)
  {N : Type u} [TopologicalSpace N] [ChartedSpace HN N] (n : WithTop ℕ∞)

lemma ContMDiff.subtypeVal_comp_iff (U : Opens N) (f : M → U) :
    ContMDiff IM IN n (Subtype.val ∘ f) ↔ ContMDiff IM IN n f := by
  sorry

This holds for any smooth embedding, see #28865 by Michael Rothgang, but I would be very surprised if mathlib does not have the case for open embeddings.
I don't know the manifold library at all, so it could well be that I missed it.
(There is docs#ContMDiff.of_comp_isOpenEmbedding, which is related but is also for composition on the source.)

[Christian Merten]

For completeness, here is a proof:

import Mathlib

open TopologicalSpace

variable {X Y Z : Type*} [TopologicalSpace X]
  [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z}

lemma Topology.IsEmbedding.continuousWithinAt_comp_iff (hg : Topology.IsEmbedding g) {s : Set X} {x : X} :
    ContinuousWithinAt (g ∘ f) s x ↔ ContinuousWithinAt f s x := by
  simp [ContinuousWithinAt, hg.tendsto_nhds_iff]

lemma Topology.IsEmbedding.continuousAt_comp_iff (hg : Topology.IsEmbedding g) (x : X) :
    ContinuousAt (g ∘ f) x ↔ ContinuousAt f x := by
  rw [← continuousWithinAt_univ, hg.continuousWithinAt_comp_iff, continuousWithinAt_univ]

variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
  {EM : Type*} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
  {HM : Type*} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {M : Type u} [TopologicalSpace M] [ChartedSpace HM M]
  {EN : Type*} [NormedAddCommGroup EN] [NormedSpace 𝕜 EN] {HN : Type*}
  [TopologicalSpace HN] (IN : ModelWithCorners 𝕜 EN HN)
  {N : Type u} [TopologicalSpace N] [ChartedSpace HN N] (n : WithTop ℕ∞)

lemma ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff
    {P : (HM → HN) → Set HM → HM → Prop} {U : Opens N} (f : M → U)
    (s : Set M) (x : M) :
    LiftPropWithinAt P (Subtype.val ∘ f) s x ↔ LiftPropWithinAt P f s x := by
  simp only [ChartedSpace.liftPropWithinAt_iff']
  congrm ?_ ∧ ?_
  · exact Topology.IsEmbedding.subtypeVal.continuousWithinAt_comp_iff
  · rfl

lemma ContMDiffWithinAt.subtypeVal_comp_iff (U : Opens N) (f : M → U) (s : Set M) (x : M) :
    ContMDiffWithinAt IM IN n (Subtype.val ∘ f) s x ↔ ContMDiffWithinAt IM IN n f s x :=
  ChartedSpace.liftPropWithinAt_subtypeVal_comp_iff ..

lemma ContMDiffAt.subtypeVal_comp_iff (U : Opens N) (f : M → U) (x : M) :
    ContMDiffAt IM IN n (Subtype.val ∘ f) x ↔ ContMDiffAt IM IN n f x := by
  rw [ContMDiffAt, ContMDiffAt, ContMDiffWithinAt.subtypeVal_comp_iff]

lemma ContMDiff.subtypeVal_comp_iff (U : Opens N) (f : M → U) :
    ContMDiff IM IN n (Subtype.val ∘ f) ↔ ContMDiff IM IN n f := by
  simp_rw [ContMDiff, ContMDiffAt.subtypeVal_comp_iff]

Are any of the other lemmas somewhere?

[Michael Rothgang]

I don't think the other lemmas exist yet.

[Michael Rothgang]

Medium-term, the proper way to prove this is by deducing it from #28865 and "Subtype.val is a smooth embedding". The second part should be doable already today.

[Michael Rothgang]

(I will get back to #28796, hopefully in a week or two.)

[Christian Merten]

Agreed, should we still have these lemmas for now? I could imagine that for import reasons, we might want to keep them anyway in a more basic file?

[Michael Rothgang]

I presume you need these basic lemmas for an application of yours?

[Michael Rothgang]

The topology lemmas for sure look innocuous to me, I'm in favour of having them.

[Christian Merten]

Michael Rothgang said:

I presume you need these basic lemmas for an application of yours?

Yes, but they are easy enough that I can include them in the PR for the actual thing I am doing.

[Michael Rothgang]

The manifold lemmas are short. If you have an application in mind which benefits from importing little manifold theory, I'm fine adding them (at least for now, perhaps with a comment that this is a special case of a more general fact).

[Michael Rothgang]

(I don't have a good feeling if depending on these immersion facts will create import tangles or not. But for 10 lines, I'm inclined not too worry too much.)

[Michael Rothgang]

I'll be happy to review that part of the PR. (I'm on holiday though, and will switch off my computer tomorrow. So there will be some latency on my part.)

[Christian Merten]

In fact the two topology lemmas are just in the wrong generality and exist as docs#Topology.IsInducing.continuousWithinAt_iff.

[Christian Merten]

They are now contained in #35661.