English
Let X,Y be topological spaces, f:X→Y continuous, and U_i an open cover of Range f with associated spaces V_i and continuous iV_i: V_i → X such that each f ∘ iV_i is an embedding and f^{-1}(U_i) ⊆ Range(iV_i) for all i. Then f is an embedding.
Русский
Пусть X,Y — топологические пространства, f: X→Y непрерывно, а покрытие Range f состоит из открытых U_i; существует семейство V_i и непрерывных iV_i: V_i → X такие, что каждый f ∘ iV_i является вложением и f^{-1}(U_i) ⊆ Range(iV_i) для всех i. Тогда f является вложением.
LaTeX
$$$\text{Suppose }\{U_i\}_{i},\{V_i\}_{i},\{iV_i: V_i \to X\}\text{ satisfy the stated conditions; then } \operatorname{IsEmbedding}(f).$$$
Lean4
/-- Given a continuous map `f : X → Y` between topological spaces.
Suppose we have an open cover `U i` of the range of `f`, and a family of continuous maps `V i → X`
whose images are a cover of `X` that is coarser than the pullback of `U` under `f`.
To check that `f` is an embedding it suffices to check that `V i → Y` is an embedding for all `i`.
-/
-- TODO : the lemma name does not match the content (there is no hypothesis `iSup_eq_top`!)
theorem isEmbedding_of_iSup_eq_top_of_preimage_subset_range {X Y} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y)
(h : Continuous f) {ι : Type*} (U : ι → Opens Y) (hU : Set.range f ⊆ (iSup U :)) (V : ι → Type*)
[∀ i, TopologicalSpace (V i)] (iV : ∀ i, V i → X) (hiV : ∀ i, Continuous (iV i))
(hV : ∀ i, f ⁻¹' U i ⊆ Set.range (iV i)) (hV' : ∀ i, IsEmbedding (f ∘ iV i)) : IsEmbedding f :=
by
wlog hU' : iSup U = ⊤
· let f₀ : X → Set.range f := fun x ↦ ⟨f x, ⟨x, rfl⟩⟩
suffices IsEmbedding f₀ from IsEmbedding.subtypeVal.comp this
have hU'' : (⨆ i, (U i).comap ⟨Subtype.val, continuous_subtype_val⟩ : Opens (Set.range f)) = ⊤ :=
by
rw [← top_le_iff]
simpa [Set.range_subset_iff, SetLike.le_def] using hU
refine this _ ?_ _ ?_ V iV hiV ?_ ?_ hU''
· fun_prop
· rw [hU'']; simp
· exact hV
· exact fun i ↦ IsEmbedding.of_comp (by fun_prop) continuous_subtype_val (hV' i)
rw [(IsOpenCover.mk hU').isEmbedding_iff_restrictPreimage h]
intro i
let f' := (Subtype.val ∘ (f ⁻¹' U i).restrictPreimage (iV i))
have : IsEmbedding f' := IsEmbedding.subtypeVal.comp ((IsEmbedding.of_comp (hiV i) h (hV' _)).restrictPreimage _)
have hf' : Set.range f' = f ⁻¹' U i := by simpa [f', Set.range_comp, Set.range_restrictPreimage] using hV i
let e := this.toHomeomorph.trans (Homeomorph.setCongr hf')
refine IsEmbedding.of_comp (by fun_prop) continuous_subtype_val ?_
convert ((hV' i).comp IsEmbedding.subtypeVal).comp e.symm.isEmbedding
ext x
obtain ⟨x, rfl⟩ := e.surjective x
simp
rfl
