continuous on image of embedding

Stream: Is there code for X?

[Junyan Xu]

Is there a simpler proof than

import Mathlib.Topology.Homeomorph.Lemmas

namespace Topology.IsEmbedding

variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
  (s : Set X) {i : X → Y} (emb : IsEmbedding i) (f : Y → Z)

include emb

noncomputable def homeomorphImage : s ≃ₜ i '' s :=
  (emb.comp .subtypeVal).toHomeomorph.trans <| .setCongr <| by simp [Set.range_comp]

theorem continuousOn_image_iff :
    ContinuousOn f (i '' s) ↔ ContinuousOn (f ∘ i) s := by
  refine ⟨(·.image_comp_continuous emb.continuous), fun h ↦ ?_⟩
  rw [continuousOn_iff_continuous_restrict] at h ⊢
  rwa [← (emb.homeomorphImage s).comp_continuous_iff']

end Topology.IsEmbedding

?

[Aaron Liu]

This already looks pretty short, I think you can probably weaken IsEmbedding i to IsInducing i in continuousOn_image_iff

[Junyan Xu]

You are right!

import Mathlib.Topology.Homeomorph.Lemmas

namespace Topology.IsInducing

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

theorem continuous_iff_of_surjective (ind : IsInducing i) (surj : Function.Surjective i) :
    Continuous (f ∘ i) ↔ Continuous f := by
  refine ⟨fun h ↦ ⟨fun U hU ↦ ?_⟩, (·.comp ind.continuous)⟩
  have ⟨V, hV, (eq : _ = i ⁻¹' (f ⁻¹' U))⟩ := ind.isOpen_iff.mp (hU.preimage h)
  rwa [← surj.preimage_injective eq]

theorem continuousOn_image_iff {s : Set X} (ind : IsInducing i) :
    ContinuousOn f (i '' s) ↔ ContinuousOn (f ∘ i) s := by
  simp_rw [continuousOn_iff_continuous_restrict]
  exact (((ind.comp .subtypeVal).codRestrict (s := i '' s)
    fun x ↦ ⟨x, x.2, rfl⟩).continuous_iff_of_surjective <| by
    rintro ⟨_, x, hx, rfl⟩; exact ⟨⟨x, hx⟩, rfl⟩).symm

end Topology.IsInducing

[Aaron Liu]

Here's what I came up with

import Mathlib.Topology.Homeomorph.Lemmas

theorem TopologicalSpace.induced_le_induced_iff_of_surjective {X Y : Type*}
    {t₁ t₂ : TopologicalSpace Y} {f : X → Y}
    (hf : f.Surjective) : t₁.induced f ≤ t₂.induced f ↔ t₁ ≤ t₂ := by
  refine ⟨fun h => ?_, induced_mono⟩ -- should `induced_mono` be namespaced?
  rw [TopologicalSpace.le_def] at h ⊢
  intro s
  simpa [isOpen_induced_iff, hf.preimage_injective.eq_iff] using h (f ⁻¹' s)

theorem Topology.IsInducing.continuousOn_image_iff {X Y Z : Type*}
    [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    (s : Set X) {i : X → Y} (hi : IsInducing i) (f : Y → Z) :
    ContinuousOn f (i '' s) ↔ ContinuousOn (f ∘ i) s := by
  refine ⟨(·.image_comp_continuous hi.continuous), fun h ↦ ?_⟩
  simp_rw [continuousOn_iff_continuous_restrict, continuous_iff_le_induced,
    Set.restrict_eq, instTopologicalSpaceSubtype] at h ⊢
  rw [hi.eq_induced, induced_compose, Function.comp_assoc, ← Set.imageFactorization_eq] at h
  simp_rw [← induced_compose] at h ⊢
  rwa [TopologicalSpace.induced_le_induced_iff_of_surjective (Set.surjective_onto_image)] at h

[Andrew Yang]

The right lean proof (for IsEmbedding) is probably

theorem continuousOn_image_iff :
    ContinuousOn f (i '' s) ↔ ContinuousOn (f ∘ i) s := by
  simp [ContinuousOn, ContinuousWithinAt, ← emb.map_nhdsWithin_eq]

And it is probably possible to extend this to inducing.

[Aaron Liu]

import Mathlib.Topology.Homeomorph.Lemmas

namespace Topology.IsInducing

theorem map_nhdsWithin_eq {α β : Type*}
    [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsInducing f)
    (s : Set α) (x : α) : Filter.map f (𝓝[s] x) = 𝓝[f '' s] f x := by
  apply le_antisymm
  · rw [nhdsWithin, nhdsWithin]
    apply Filter.map_inf_le.trans
    apply inf_le_inf
    · exact hf.continuous.tendsto x
    · rw [Filter.map_principal]
  · intro U hU
    rw [Filter.mem_map] at hU
    rw [mem_nhdsWithin_iff_eventually] at hU ⊢
    rw [hf.nhds_eq_comap, Filter.eventually_comap] at hU
    filter_upwards [hU] with b hb ⟨a, ha, hab⟩
    subst hab
    exact hb a rfl ha

[Aaron Liu]

You don't need an embedding

[Junyan Xu]

Very nice! The proof of Topology.IsEmbedding.map_nhdsWithin_eq doesn't generalize (requires injectivity) so I was wondering whether this is true ...

[Michael Rothgang]

Would you like to PR this?

[Junyan Xu]

(deleted)

[Junyan Xu]

If the task falls on me I'd PR it with the file Trivialization.lean here which uses it ((Topology.IsInducing.subtypeVal.prodMap .id).continuousOn_image_iff.2).

[Junyan Xu]

Okay, I decided to make a separate PR #25041

[Junyan Xu]

and make the trivialization PR #25042 depend on it. It includes restriction/extension of Trivialization and composition with Homeomorph, which was required to restrict/extend/compose covering maps, but may no longer be needed after the definition changes in #24983. It should be useful in other situations nonetheless.