Further restriction of an embedding is an embedding

Stream: Is there code for X?

[Michael Rothgang]

MWE:

import Mathlib
lemma foo {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : X → Y} {g : Y → Z} {s : Set X} {t : Set Y}
    (hf : IsEmbedding (s.restrict f)) (hg : IsEmbedding (t.restrict g)) :
    IsEmbedding ((s ∩ f ⁻¹' t).restrict (g ∘ f)) := sorry

This seems easy, but I'm easily running into DTT hell. I'm sure this question has been asked before, can somebody help me?
I started with this: so far, clear enough:

import Mathlib
lemma foo {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : X → Y} {g : Y → Z} {s : Set X} {t : Set Y}
    (hf : IsEmbedding (s.restrict f)) (hg : IsEmbedding (t.restrict g)) :
    IsEmbedding ((s ∩ f ⁻¹' t).restrict (g ∘ f)) := by
  have hm : MapsTo f (s ∩ f⁻¹' t) t := by intro x ⟨_hxs, hxt⟩; simp_all
  have hf' : IsEmbedding (hm.restrict f) := by sorry -- this should be known!
  exact hg.comp hf'

The sorry hf' is surely known, right? Loogle-ing for Topology.IsEmbedding, "restrict" yields docs#Topology.IsEmbedding.restrictPreimage, which seems exactly like what I want... except now I'm stuck in DTT hell!

import Mathlib
lemma foo {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : X → Y} {g : Y → Z} {s : Set X} {t : Set Y}
    (hf : IsEmbedding (s.restrict f)) (hg : IsEmbedding (t.restrict g)) :
    IsEmbedding ((s ∩ f ⁻¹' t).restrict (g ∘ f)) := by
  have hm : MapsTo f (s ∩ f⁻¹' t) t := by intro x ⟨_hxs, hxt⟩; simp_all

  have hf'' := Topology.IsEmbedding.restrictPreimage t hf
  have : s.restrict f ⁻¹' t = s ∩ f ⁻¹' t := by ext; constructor <;> simp +contextual
  -- This does not typecheck; need a map between the subtypes of (s.restrict f ⁻¹' t) and
  -- (s ∩ f ⁻¹' t) and show it's an embedding.
  -- have : (s ∩ f ⁻¹' t).restrict (g ∘ f) = (t.restrict g) ∘ (t.restrictPreimage (s.restrict f)) := by
  --   sorry
  -- Subtype.map does not quite work: what's the trick here?
  let s₁ := s.restrict f ⁻¹' t; let s₂ := s ∩ f ⁻¹' t
  have : (∀ a ∈ s₁, ↑a ∈ s₂) := sorry
  let φ := Subtype.map (p := fun x ↦ x ∈ s₁) (q := fun x ↦ x ∈ s₂) Subtype.val this
  have : IsEmbedding φ := sorry -- give inverse; use Continuous.subtype_mk in both directions
  -- application type mismatch...
  -- let rhs := (t.restrict g) ∘ φ ∘ (t.restrictPreimage (s.restrict f))

  have hf' : IsEmbedding (hm.restrict f) := by
    sorry -- if not for the above, `hf''` would do it.
  exact hg.comp hf'--hf''

[Aaron Liu]

We can add Topology.IsEmbedding.restrict

[Aaron Liu]

I'll take a look once I'm back at a keyboard

[Michael Rothgang]

Ok, here's a more elegant idea: can one construct an embedding from the subtype s ∩ f ⁻¹' t to s? With that, I can finish the proof.

[Michael Rothgang]

The idea is to avoid working with subtypes (for reasons such as above), and use docs#Topology.IsEmbedding.of_comp_iff and docs#Topology.IsEmbedding.subtypeVal.

[Michael Rothgang]

And the answer to my question above is yes: use Subtype.map again. :working_on_it:

[Michael Rothgang]

Here's the complete proof:

import Mathlib
lemma IsEmbedding.subtype_map_of_subset {X : Type*} [TopologicalSpace X]
    {s t : Set X} (hst : s ⊆ t) : IsEmbedding (Subtype.map id hst) := by
  have := IsEmbedding.subtypeVal (p := t)
  rw [← IsEmbedding.of_comp_iff (IsEmbedding.subtypeVal (p := t))]
  exact IsEmbedding.subtypeVal (p := s)

lemma foo {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : X → Y} {g : Y → Z} {s : Set X} {t : Set Y}
    (hf : IsEmbedding (s.restrict f)) (hg : IsEmbedding (t.restrict g)) :
    IsEmbedding ((s ∩ f ⁻¹' t).restrict (g ∘ f)) := by
  have hm : MapsTo f (s ∩ f⁻¹' t) t := by intro x ⟨_hxs, hxt⟩; simp_all
  have : s ∩ f⁻¹' t ⊆ s := inter_subset_left
  have hf' : IsEmbedding (hm.restrict f) :=
    (hf.comp (IsEmbedding.subtype_map_of_subset this)).codRestrict t _
  exact hg.comp hf'

[Aaron Liu]

oh you did it

[Aaron Liu]

but maybe don't use Subtype.map?

[Ben Eltschig]

that first lemma seems very similar to docs#Topology.IsEmbedding.inclusion

[Aaron Liu]

ah yes docs#Set.inclusion

[Aaron Liu]

do use that instead of Subtype.map

[Michael Rothgang]

That's much nicer, thanks!

[Michael Rothgang]

Updated code

import Mathlib
open Topology Set

lemma Topology.IsEmbedding.restrict_subset {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    {f : X → Y} {g : Y → Z} {s : Set X} {t : Set Y}
    (hf : IsEmbedding (s.restrict f)) (hg : IsEmbedding (t.restrict g)) :
    IsEmbedding ((s ∩ f ⁻¹' t).restrict (g ∘ f)) := by
  have hm : MapsTo f (s ∩ f⁻¹' t) t := by intro x ⟨_hxs, hxt⟩; simp_all
  have : s ∩ f⁻¹' t ⊆ s := inter_subset_left
  have hf' : IsEmbedding (hm.restrict f) :=
    (hf.comp (IsEmbedding.inclusion this)).codRestrict t _
  exact hg.comp hf'