feat: separated and locally injective maps (#7911)

A function from a topological space `X` to a type `Y` is a separated map if any two distinct points in `X` with the same image in `Y` can be separated by open neighborhoods. A constant function is a separated map if and only if `X` is a `T2Space`.

A function from a topological space `X` is locally injective if every point of `X` has a neighborhood on which `f` is injective. A constant function is locally injective if and only if `X` is discrete.

Given `f : X → Y` one can form the pullback $X \times_Y X$; the diagonal map $\Delta: X \to X \times_Y X$ is always an embedding. It is a closed embedding iff `f` is a separated map, iff the equal locus of any two continuous maps equalized by `f` is closed. It is an open embedding iff `f` is locally injective, iff any such equal locus is open. Therefore, if `f` is a locally injective separated map (e.g. a covering map), the equal locus of two continuous maps equalized by `f` is clopen, so if the two maps agree on a point, then they agree on the whole connected component. This is crucial to showing the uniqueness of path lifting and the uniqueness and continuity of homotopy lifting for covering spaces.

The analogue of separated maps and locally injective maps in algebraic geometry are separated morphisms and unramified morphisms, respectively.

Mathlib.lean

@@ -3539,6 +3539,7 @@ import Mathlib.Topology.Perfect
 import Mathlib.Topology.ProperMap
 import Mathlib.Topology.QuasiSeparated
 import Mathlib.Topology.Semicontinuous
+import Mathlib.Topology.SeparatedMap
 import Mathlib.Topology.Separation
 import Mathlib.Topology.Separation.NotNormal
 import Mathlib.Topology.Sequences

Mathlib/Data/Set/Prod.lean

@@ -554,6 +554,89 @@ theorem diag_image (s : Set α) : (fun x => (x, x)) '' s = diagonal α ∩ s ×
 
 end Diagonal
 
+end Set
+
+section Pullback
+
+open Set
+
+variable {X Y Z}
+
+/-- The fiber product $X \times_Y Z$. -/
+abbrev Function.Pullback (f : X → Y) (g : Z → Y) := {p : X × Z // f p.1 = g p.2}
+
+/-- The fiber product $X \times_Y X$. -/
+abbrev Function.PullbackSelf (f : X → Y) := f.Pullback f
+
+/-- The projection from the fiber product to the first factor. -/
+def Function.Pullback.fst {f : X → Y} {g : Z → Y} (p : f.Pullback g) : X := p.val.1
+
+/-- The projection from the fiber product to the second factor. -/
+def Function.Pullback.snd {f : X → Y} {g : Z → Y} (p : f.Pullback g) : Z := p.val.2
+
+open Function.Pullback in
+lemma Function.pullback_comm_sq (f : X → Y) (g : Z → Y) :
+    f ∘ @fst X Y Z f g = g ∘ @snd X Y Z f g := funext fun p ↦ p.2
+
+/-- The diagonal map $\Delta: X \to X \times_Y X$. -/
+def toPullbackDiag (f : X → Y) (x : X) : f.Pullback f := ⟨(x, x), rfl⟩
+
+/-- The diagonal $\Delta(X) \subseteq X \times_Y X$. -/
+def Function.pullbackDiagonal (f : X → Y) : Set (f.Pullback f) := {p | p.fst = p.snd}
+
+/-- Three functions between the three pairs of spaces $X_i, Y_i, Z_i$ that are compatible
+  induce a function $X_1 \times_{Y_1} Z_1 \to X_2 \times_{Y_2} Z_2$. -/
+def Function.mapPullback {X₁ X₂ Y₁ Y₂ Z₁ Z₂}
+    {f₁ : X₁ → Y₁} {g₁ : Z₁ → Y₁} {f₂ : X₂ → Y₂} {g₂ : Z₂ → Y₂}
+    (mapX : X₁ → X₂) (mapY : Y₁ → Y₂) (mapZ : Z₁ → Z₂)
+    (commX : f₂ ∘ mapX = mapY ∘ f₁) (commZ : g₂ ∘ mapZ = mapY ∘ g₁)
+    (p : f₁.Pullback g₁) : f₂.Pullback g₂ :=
+  ⟨(mapX p.fst, mapZ p.snd),
+    (congr_fun commX _).trans <| (congr_arg mapY p.2).trans <| congr_fun commZ.symm _⟩
+
+open Function.Pullback in
+/-- The projection $(X \times_Y Z) \times_Z (X \times_Y Z) \to X \times_Y X$. -/
+def Function.PullbackSelf.map_fst {f : X → Y} {g : Z → Y} :
+    (@snd X Y Z f g).PullbackSelf → f.PullbackSelf :=
+  mapPullback fst g fst (pullback_comm_sq f g) (pullback_comm_sq f g)
+
+open Function.Pullback in
+/-- The projection $(X \times_Y Z) \times_X (X \times_Y Z) \to Z \times_Y Z$. -/
+def Function.PullbackSelf.map_snd {f : X → Y} {g : Z → Y} :
+    (@fst X Y Z f g).PullbackSelf → g.PullbackSelf :=
+  mapPullback snd f snd (pullback_comm_sq f g).symm (pullback_comm_sq f g).symm
+
+open Function.PullbackSelf Function.Pullback
+theorem preimage_map_fst_pullbackDiagonal {f : X → Y} {g : Z → Y} :
+    @map_fst X Y Z f g ⁻¹' pullbackDiagonal f = pullbackDiagonal (@snd X Y Z f g) := by
+  ext ⟨⟨p₁, p₂⟩, he⟩
+  simp_rw [pullbackDiagonal, mem_setOf, Subtype.ext_iff, Prod.ext_iff]
+  exact (and_iff_left he).symm
+
+theorem Function.Injective.preimage_pullbackDiagonal {f : X → Y} {g : Z → X} (inj : g.Injective) :
+    mapPullback g id g (by rfl) (by rfl) ⁻¹' pullbackDiagonal f = pullbackDiagonal (f ∘ g) :=
+  ext fun _ ↦ inj.eq_iff
+
+theorem image_toPullbackDiag (f : X → Y) (s : Set X) :
+    toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s := by
+  ext x
+  constructor
+  · rintro ⟨x, hx, rfl⟩
+    exact ⟨rfl, hx, hx⟩
+  · obtain ⟨⟨x, y⟩, h⟩ := x
+    rintro ⟨rfl : x = y, h2x⟩
+    exact mem_image_of_mem _ h2x.1
+
+theorem range_toPullbackDiag (f : X → Y) : range (toPullbackDiag f) = pullbackDiagonal f := by
+  rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]
+
+theorem injective_toPullbackDiag (f : X → Y) : (toPullbackDiag f).Injective :=
+  fun _ _ h ↦ congr_arg Prod.fst (congr_arg Subtype.val h)
+
+end Pullback
+
+namespace Set
+
 section OffDiag
 
 variable {α : Type*} {s t : Set α} {x : α × α} {a : α}

Mathlib/Topology/Covering.lean

@@ -156,25 +156,55 @@ theorem mk (F : X → Type*) [∀ x, TopologicalSpace (F x)] [∀ x, DiscreteTop
     (IsCoveringMapOn.mk f Set.univ F (fun x _ => e x) fun x _ => h x)
 #align is_covering_map.mk IsCoveringMap.mk
 
-variable {f}
+variable {f} (hf : IsCoveringMap f)
 
-protected theorem continuous (hf : IsCoveringMap f) : Continuous f :=
+protected theorem continuous : Continuous f :=
   continuous_iff_continuousOn_univ.mpr hf.isCoveringMapOn.continuousOn
 #align is_covering_map.continuous IsCoveringMap.continuous
 
-protected theorem isLocallyHomeomorph (hf : IsCoveringMap f) : IsLocallyHomeomorph f :=
+protected theorem isLocallyHomeomorph : IsLocallyHomeomorph f :=
   isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ.mpr hf.isCoveringMapOn.isLocallyHomeomorphOn
 #align is_covering_map.is_locally_homeomorph IsCoveringMap.isLocallyHomeomorph
 
-protected theorem isOpenMap (hf : IsCoveringMap f) : IsOpenMap f :=
+protected theorem isOpenMap : IsOpenMap f :=
   hf.isLocallyHomeomorph.isOpenMap
 #align is_covering_map.is_open_map IsCoveringMap.isOpenMap
 
-protected theorem quotientMap (hf : IsCoveringMap f) (hf' : Function.Surjective f) :
-    QuotientMap f :=
+protected theorem quotientMap (hf' : Function.Surjective f) : QuotientMap f :=
   hf.isOpenMap.to_quotientMap hf.continuous hf'
 #align is_covering_map.quotient_map IsCoveringMap.quotientMap
 
+protected theorem isSeparatedMap : IsSeparatedMap f :=
+  fun e₁ e₂ he hne ↦ by
+    obtain ⟨_, t, he₁⟩ := hf (f e₁)
+    have he₂ := he₁; simp_rw [he] at he₂; rw [← t.mem_source] at he₁ he₂
+    refine ⟨t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₁).2}, t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₂).2},
+      ?_, ?_, ⟨he₁, rfl⟩, ⟨he₂, rfl⟩, Set.disjoint_left.mpr fun x h₁ h₂ ↦ hne (t.injOn he₁ he₂ ?_)⟩
+    iterate 2
+      exact t.continuous_toFun.preimage_open_of_open t.open_source
+        (continuous_snd.isOpen_preimage _ <| isOpen_discrete _)
+    refine Prod.ext ?_ (h₁.2.symm.trans h₂.2)
+    rwa [t.proj_toFun e₁ he₁, t.proj_toFun e₂ he₂]
+
+variable {A} [TopologicalSpace A] {s : Set A} (hs : IsPreconnected s) {g g₁ g₂ : A → E}
+
+theorem eq_of_comp_eq [PreconnectedSpace A] (h₁ : Continuous g₁) (h₂ : Continuous g₂)
+    (he : f ∘ g₁ = f ∘ g₂) (a : A) (ha : g₁ a = g₂ a) : g₁ = g₂ :=
+  hf.isSeparatedMap.eq_of_comp_eq hf.isLocallyHomeomorph.isLocallyInjective h₁ h₂ he a ha
+
+theorem eqOn_of_comp_eqOn (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s)
+    (he : s.EqOn (f ∘ g₁) (f ∘ g₂)) {a : A} (has : a ∈ s) (ha : g₁ a = g₂ a) : s.EqOn g₁ g₂ :=
+  hf.isSeparatedMap.eqOn_of_comp_eqOn hf.isLocallyHomeomorph.isLocallyInjective hs h₁ h₂ he has ha
+
+theorem const_of_comp [PreconnectedSpace A] (cont : Continuous g)
+    (he : ∀ a a', f (g a) = f (g a')) (a a') : g a = g a' :=
+  hf.isSeparatedMap.const_of_comp hf.isLocallyHomeomorph.isLocallyInjective cont he a a'
+
+theorem constOn_of_comp (cont : ContinuousOn g s)
+    (he : ∀ a ∈ s, ∀ a' ∈ s, f (g a) = f (g a'))
+    {a a'} (ha : a ∈ s) (ha' : a' ∈ s) : g a = g a' :=
+  hf.isSeparatedMap.constOn_of_comp hf.isLocallyHomeomorph.isLocallyInjective hs cont he ha ha'
+
 end IsCoveringMap
 
 variable {f}

Mathlib/Topology/IsLocallyHomeomorph.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 import Mathlib.Topology.LocalHomeomorph
+import Mathlib.Topology.SeparatedMap
 
 #align_import topology.is_locally_homeomorph from "leanprover-community/mathlib"@"e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b"
 
@@ -125,7 +126,7 @@ def IsLocallyHomeomorph :=
   ∀ x : X, ∃ e : LocalHomeomorph X Y, x ∈ e.source ∧ f = e
 #align is_locally_homeomorph IsLocallyHomeomorph
 
-theorem isLocallyHomeomorph_homeomorph (f : X ≃ₜ Y) : IsLocallyHomeomorph f :=
+theorem Homeomorph.isLocallyHomeomorph (f : X ≃ₜ Y) : IsLocallyHomeomorph f :=
   fun _ ↦ ⟨f.toLocalHomeomorph, trivial, rfl⟩
 
 variable {f s}
@@ -163,6 +164,9 @@ theorem mk (h : ∀ x : X, ∃ e : LocalHomeomorph X Y, x ∈ e.source ∧ ∀ y
 
 variable {g f}
 
+lemma isLocallyInjective (hf : IsLocallyHomeomorph f) : IsLocallyInjective f :=
+  fun x ↦ by obtain ⟨f, hx, rfl⟩ := hf x; exact ⟨f.source, f.open_source, hx, f.injOn⟩
+
 theorem of_comp (hgf : IsLocallyHomeomorph (g ∘ f)) (hg : IsLocallyHomeomorph g)
     (cont : Continuous f) : IsLocallyHomeomorph f :=
   isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ.mpr <|
@@ -196,7 +200,7 @@ theorem openEmbedding_of_comp (hf : IsLocallyHomeomorph g) (hgf : OpenEmbedding
   (hgf.isLocallyHomeomorph.of_comp hf cont).openEmbedding_of_injective hgf.inj.of_comp
 
 open TopologicalSpace in
-/-- Ranges of continuous local sections of a local homeomorphism form a basis of the total space. -/
+/-- Ranges of continuous local sections of a local homeomorphism form a basis of the source space.-/
 theorem isTopologicalBasis (hf : IsLocallyHomeomorph f) : IsTopologicalBasis
     {U : Set X | ∃ V : Set Y, IsOpen V ∧ ∃ s : C(V,X), f ∘ s = (↑) ∧ Set.range s = U} := by
   refine isTopologicalBasis_of_open_of_nhds ?_ fun x U hx hU ↦ ?_