Documentation

Mathlib.Topology.SeparatedMap

Separated maps and locally injective maps out of a topological space. #

This module introduces a pair of dual notions IsSeparatedMap and IsLocallyInjective.

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 we 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 coequalized 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, the equal locus of two continuous maps coequalized by f is clopen, so if the two maps agree on a point, then they agree on the whole connected component.

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

Reference #

https://stacks.math.columbia.edu/tag/0CY0

theorem embedding_toPullbackDiag {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] (f : XY) :
theorem Continuous.mapPullback {X₁ : Type u_1} {X₂ : Type u_2} {Y₁ : Sort u_3} {Y₂ : Sort u_4} {Z₁ : Type u_5} {Z₂ : Type u_6} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Z₁] [TopologicalSpace Z₂] {f₁ : X₁Y₁} {g₁ : Z₁Y₁} {f₂ : X₂Y₂} {g₂ : Z₂Y₂} {mapX : X₁X₂} (contX : Continuous mapX) {mapY : Y₁Y₂} {mapZ : Z₁Z₂} (contZ : Continuous mapZ) {commX : f₂ mapX = mapY f₁} {commZ : g₂ mapZ = mapY g₁} :
Continuous (Function.mapPullback mapX mapY mapZ commX commZ)
def IsSeparatedMap {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] (f : XY) :

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.

Equations
Instances For
    theorem t2space_iff_isSeparatedMap {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] (y : Y) :
    T2Space X IsSeparatedMap fun (x : X) => y
    theorem T2Space.isSeparatedMap {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] [T2Space X] (f : XY) :
    theorem Function.Injective.isSeparatedMap {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] {f : XY} (inj : Function.Injective f) :
    theorem isSeparatedMap_iff_disjoint_nhds {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] {f : XY} :
    IsSeparatedMap f ∀ (x₁ x₂ : X), f x₁ = f x₂x₁ x₂Disjoint (nhds x₁) (nhds x₂)
    theorem isSeparatedMap_iff_nhds {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] {f : XY} :
    IsSeparatedMap f ∀ (x₁ x₂ : X), f x₁ = f x₂x₁ x₂s₁nhds x₁, s₂nhds x₂, Disjoint s₁ s₂
    theorem IsSeparatedMap.pullback {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : XY} (sep : IsSeparatedMap f) (g : AY) :
    IsSeparatedMap Function.Pullback.snd
    theorem IsSeparatedMap.comp_left {X : Type u_2} {Y : Sort u_3} [TopologicalSpace X] {A : Sort u_1} {f : XY} (sep : IsSeparatedMap f) {g : YA} (inj : Function.Injective g) :
    theorem IsSeparatedMap.comp_right {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : XY} (sep : IsSeparatedMap f) {g : AX} (cont : Continuous g) (inj : Function.Injective g) :
    def IsLocallyInjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : XY) :

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

    Equations
    Instances For
      theorem isLocallyInjective_iff_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : XY} :
      IsLocallyInjective f ∀ (x : X), Unhds x, Set.InjOn f U
      theorem IsLocallyInjective.comp_left {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] {A : Type u_1} {f : XY} (hf : IsLocallyInjective f) {g : YA} (hg : Function.Injective g) :
      theorem IsLocallyInjective.comp_right {X : Type u_1} {Y : Type u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : XY} (hf : IsLocallyInjective f) {g : AX} (cont : Continuous g) (hg : Function.Injective g) :
      theorem IsSeparatedMap.isClosed_eqLocus {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : XY} {g₁ : AX} {g₂ : AX} (h₁ : Continuous g₁) (h₂ : Continuous g₂) (sep : IsSeparatedMap f) (he : f g₁ = f g₂) :
      IsClosed {a : A | g₁ a = g₂ a}
      theorem IsLocallyInjective.isOpen_eqLocus {X : Type u_1} {Y : Type u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : XY} {g₁ : AX} {g₂ : AX} (h₁ : Continuous g₁) (h₂ : Continuous g₂) (inj : IsLocallyInjective f) (he : f g₁ = f g₂) :
      IsOpen {a : A | g₁ a = g₂ a}
      theorem IsSeparatedMap.eq_of_comp_eq {X : Type u_1} {E : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace A] {p : EX} {g₁ : AE} {g₂ : AE} (sep : IsSeparatedMap p) (inj : IsLocallyInjective p) [PreconnectedSpace A] (h₁ : Continuous g₁) (h₂ : Continuous g₂) (he : p g₁ = p g₂) (a : A) (ha : g₁ a = g₂ a) :
      g₁ = g₂

      If p is a locally injective separated map, and A is a connected space, then two lifts g₁, g₂ : A → E of a map f : A → X are equal if they agree at one point.

      theorem IsSeparatedMap.eqOn_of_comp_eqOn {X : Type u_1} {E : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace A] {p : EX} {s : Set A} {g₁ : AE} {g₂ : AE} (sep : IsSeparatedMap p) (inj : IsLocallyInjective p) (hs : IsPreconnected s) (h₁ : ContinuousOn g₁ s) (h₂ : ContinuousOn g₂ s) (he : Set.EqOn (p g₁) (p g₂) s) {a : A} (has : a s) (ha : g₁ a = g₂ a) :
      Set.EqOn g₁ g₂ s
      theorem IsSeparatedMap.const_of_comp {X : Type u_1} {E : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace A] {p : EX} {g : AE} (sep : IsSeparatedMap p) (inj : IsLocallyInjective p) [PreconnectedSpace A] (cont : Continuous g) (he : ∀ (a a' : A), p (g a) = p (g a')) (a : A) (a' : A) :
      g a = g a'
      theorem IsSeparatedMap.constOn_of_comp {X : Type u_1} {E : Type u_2} {A : Type u_3} [TopologicalSpace E] [TopologicalSpace A] {p : EX} {s : Set A} {g : AE} (sep : IsSeparatedMap p) (inj : IsLocallyInjective p) (hs : IsPreconnected s) (cont : ContinuousOn g s) (he : as, a's, p (g a) = p (g a')) {a : A} {a' : A} (ha : a s) (ha' : a' s) :
      g a = g a'