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 : X → Y) : Embedding (toPullbackDiag f)

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 : X → Y) : Prop

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

• IsSeparatedMap f = ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ (s₁ : Set X) (s₂ : Set X), IsOpen s₁ ∧ IsOpen s₂ ∧ x₁ ∈ s₁ ∧ x₂ ∈ s₂ ∧ Disjoint s₁ s₂

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 : X → Y) : IsSeparatedMap f

theorem Function.Injective.isSeparatedMap {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] {f : X → Y} (inj : Function.Injective f) : IsSeparatedMap f

theorem isSeparatedMap_iff_disjoint_nhds {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] {f : X → Y} : 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 : X → Y} : IsSeparatedMap f ↔ ∀ (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} [TopologicalSpace X] {f : X → Y} : IsSeparatedMap f ↔ IsClosed (Function.pullbackDiagonal f)

theorem isSeparatedMap_iff_closedEmbedding {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] {f : X → Y} : IsSeparatedMap f ↔ ClosedEmbedding (toPullbackDiag f)

theorem isSeparatedMap_iff_isClosedMap {X : Type u_1} {Y : Sort u_2} [TopologicalSpace X] {f : X → Y} : IsSeparatedMap f ↔ IsClosedMap (toPullbackDiag f)

theorem IsSeparatedMap.pullback {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : X → Y} (sep : IsSeparatedMap f) (g : A → Y) : IsSeparatedMap Function.Pullback.snd

theorem IsSeparatedMap.comp_left {X : Type u_2} {Y : Sort u_3} [TopologicalSpace X] {A : Sort u_1} {f : X → Y} (sep : IsSeparatedMap f) {g : Y → A} (inj : Function.Injective g) : IsSeparatedMap (g ∘ f)

theorem IsSeparatedMap.comp_right {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : X → Y} (sep : IsSeparatedMap f) {g : A → X} (cont : Continuous g) (inj : Function.Injective g) : IsSeparatedMap (f ∘ g)

def IsLocallyInjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : X → Y) : Prop

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

Equations

• IsLocallyInjective f = ∀ (x : X), ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ Set.InjOn f U

theorem Function.Injective.IsLocallyInjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} (inj : Function.Injective f) : IsLocallyInjective f

theorem isLocallyInjective_iff_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} : IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ nhds x, Set.InjOn f U

theorem isLocallyInjective_iff_isOpen_diagonal {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} : IsLocallyInjective f ↔ IsOpen (Function.pullbackDiagonal f)

theorem IsLocallyInjective_iff_openEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} : IsLocallyInjective f ↔ OpenEmbedding (toPullbackDiag f)

theorem isLocallyInjective_iff_isOpenMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {f : X → Y} : IsLocallyInjective f ↔ IsOpenMap (toPullbackDiag f)

theorem discreteTopology_iff_locallyInjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (y : Y) : DiscreteTopology X ↔ IsLocallyInjective fun (x : X) => y

theorem IsLocallyInjective.comp_left {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] {A : Type u_1} {f : X → Y} (hf : IsLocallyInjective f) {g : Y → A} (hg : Function.Injective g) : IsLocallyInjective (g ∘ f)

theorem IsLocallyInjective.comp_right {X : Type u_1} {Y : Type u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : X → Y} (hf : IsLocallyInjective f) {g : A → X} (cont : Continuous g) (hg : Function.Injective g) : IsLocallyInjective (f ∘ g)

theorem IsSeparatedMap.isClosed_eqLocus {X : Type u_1} {Y : Sort u_2} {A : Type u_3} [TopologicalSpace X] [TopologicalSpace A] {f : X → Y} {g₁ : A → X} {g₂ : A → X} (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 : X → Y} {g₁ : A → X} {g₂ : A → X} (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 : E → X} {g₁ : A → E} {g₂ : A → E} (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 : E → X} {s : Set A} {g₁ : A → E} {g₂ : A → E} (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 : E → X} {g : A → E} (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 : E → X} {s : Set A} {g : A → E} (sep : IsSeparatedMap p) (inj : IsLocallyInjective p) (hs : IsPreconnected s) (cont : ContinuousOn g s) (he : ∀ a ∈ s, ∀ a' ∈ s, p (g a) = p (g a')) {a : A} {a' : A} (ha : a ∈ s) (ha' : a' ∈ s) : g a = g a'