# 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} [] (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} [] [] [] [] {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} [] (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} [] (y : Y) :
IsSeparatedMap fun (x : X) => y
theorem T2Space.isSeparatedMap {X : Type u_1} {Y : Sort u_2} [] [] (f : XY) :
theorem Function.Injective.isSeparatedMap {X : Type u_1} {Y : Sort u_2} [] {f : XY} (inj : ) :
theorem isSeparatedMap_iff_disjoint_nhds {X : Type u_1} {Y : Sort u_2} [] {f : XY} :
∀ (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} [] {f : XY} :
∀ (x₁ x₂ : X), f x₁ = f x₂x₁ x₂∃ s₁ ∈ nhds x₁, ∃ s₂ ∈ nhds x₂, Disjoint s₁ s₂
theorem isSeparatedMap_iff_isClosed_diagonal {X : Type u_1} {Y : Sort u_2} [] {f : XY} :
theorem isSeparatedMap_iff_closedEmbedding {X : Type u_1} {Y : Sort u_2} [] {f : XY} :
theorem isSeparatedMap_iff_isClosedMap {X : Type u_1} {Y : Sort u_2} [] {f : XY} :
theorem IsSeparatedMap.pullback {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [] [] {f : XY} (sep : ) (g : AY) :
IsSeparatedMap Function.Pullback.snd
theorem IsSeparatedMap.comp_left {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [] {f : XY} (sep : ) {g : YA} (inj : ) :
theorem IsSeparatedMap.comp_right {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [] [] {f : XY} (sep : ) {g : AX} (cont : ) (inj : ) :
def IsLocallyInjective {X : Type u_1} {Y : Type u_2} [] (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 Function.Injective.IsLocallyInjective {X : Type u_1} {Y : Type u_2} [] {f : XY} (inj : ) :
theorem isLocallyInjective_iff_nhds {X : Type u_1} {Y : Type u_2} [] {f : XY} :
∀ (x : X), ∃ U ∈ nhds x,
theorem isLocallyInjective_iff_isOpen_diagonal {X : Type u_1} {Y : Type u_2} [] {f : XY} :
theorem IsLocallyInjective_iff_openEmbedding {X : Type u_1} {Y : Type u_2} [] {f : XY} :
theorem isLocallyInjective_iff_isOpenMap {X : Type u_1} {Y : Type u_2} [] {f : XY} :
theorem discreteTopology_iff_locallyInjective {X : Type u_1} {Y : Type u_2} [] (y : Y) :
IsLocallyInjective fun (x : X) => y
theorem IsLocallyInjective.comp_left {X : Type u_1} {Y : Type u_2} {A : Type u_3} [] {f : XY} (hf : ) {g : YA} (hg : ) :
theorem IsLocallyInjective.comp_right {X : Type u_1} {Y : Type u_2} {A : Type u_3} [] [] {f : XY} (hf : ) {g : AX} (cont : ) (hg : ) :
theorem IsSeparatedMap.isClosed_eqLocus {X : Type u_3} {Y : Type u_2} {A : Type u_1} [] [] {f : XY} (sep : ) {g₁ : AX} {g₂ : AX} (h₁ : ) (h₂ : ) (he : f g₁ = f g₂) :
IsClosed {a : A | g₁ a = g₂ a}
theorem IsLocallyInjective.isOpen_eqLocus {X : Type u_3} {Y : Type u_2} {A : Type u_1} [] [] {f : XY} (inj : ) {g₁ : AX} {g₂ : AX} (h₁ : ) (h₂ : ) (he : f g₁ = f g₂) :
IsOpen {a : A | g₁ a = g₂ a}
theorem IsSeparatedMap.eq_of_comp_eq {X : Type u_3} {E : Type u_1} {A : Type u_2} [] [] {p : EX} (sep : ) (inj : ) {g₁ : AE} {g₂ : AE} (h₁ : ) (h₂ : ) (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_3} {E : Type u_1} {A : Type u_2} [] [] {p : EX} (sep : ) (inj : ) {s : Set A} (hs : ) {g₁ : AE} {g₂ : AE} (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_3} {E : Type u_1} {A : Type u_2} [] [] {p : EX} (sep : ) (inj : ) {g : AE} (cont : ) (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_3} {E : Type u_1} {A : Type u_2} [] [] {p : EX} (sep : ) (inj : ) {s : Set A} (hs : ) {g : AE} (cont : ) (he : as, a's, p (g a) = p (g a')) {a : A} {a' : A} (ha : a s) (ha' : a' s) :
g a = g a'