isSeparatedMap_iff_isClosed_diagonal
theorem isSeparatedMap_iff_isClosed_diagonal :
∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] {f : X → Y},
IsSeparatedMap f ↔ IsClosed (Function.pullbackDiagonal f)
The theorem `isSeparatedMap_iff_isClosed_diagonal` states that for any function `f` from a topological space `X` to any type `Y`, `f` is a separated map if and only if the diagonal of the pullback of `f` is a closed set. In other words, a function `f` separates points via open neighborhoods if and only if the subset of the pullback of `f` where the first and second components are equal forms a closed set in the topological space.
More concisely: A function between topological spaces is separated if and only if the diagonal of its pullback is a closed set.
|
IsSeparatedMap.eq_of_comp_eq
theorem IsSeparatedMap.eq_of_comp_eq :
∀ {X : Type u_3} {E : Type u_1} {A : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace A]
{p : E → X},
IsSeparatedMap p →
IsLocallyInjective p →
∀ {g₁ g₂ : A → E} [inst_2 : PreconnectedSpace A],
Continuous g₁ → Continuous g₂ → p ∘ g₁ = p ∘ g₂ → ∀ (a : A), g₁ a = g₂ a → g₁ = g₂
The theorem `IsSeparatedMap.eq_of_comp_eq` states that for any locally injective separated map `p` from a topological space `E` to another space `X`, and given a connected space `A`, if there are two continuous functions `g₁, g₂` from `A` to `E` that both lift a map `f` from `A` to `X` (i.e., `f` is the composition of `p` with either `g₁` or `g₂`), then if `g₁` and `g₂` agree at any point in `A`, they must be equal everywhere on `A`. This is a kind of uniqueness statement for lifting problems in topology, asserting that there can't be two different solutions that agree at a point in a connected space.
More concisely: If `p: E -> X` is a locally injective separated map between topological spaces, `A` is a connected space, and `g₁, g₂: A -> E` are continuous functions lifting the same map `f: A -> X` from `A` to `X`, then `g₁ = g₂` on `A`.
|
isLocallyInjective_iff_isOpen_diagonal
theorem isLocallyInjective_iff_isOpen_diagonal :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
IsLocallyInjective f ↔ IsOpen (Function.pullbackDiagonal f)
This theorem states that for any topological space `X` and any type `Y`, and any function `f` from `X` to `Y`, the function `f` is locally injective if and only if the pullback of the diagonal of `Y` under the function `f` is an open set in the product topology on `X` x `X`. In other words, near every point in `X`, `f` doesn't send two different points to the same value (`f` is locally injective), if and only if the set of all pairs `(x, x')` in `X` x `X` such that `f(x) = f(x')` is an open set.
More concisely: A function from a topological space to another type is locally injective if and only if the pullback of the diagonal relation is an open subset in the product topology.
|
Continuous.mapPullback
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}
[inst : TopologicalSpace X₁] [inst_1 : TopologicalSpace X₂] [inst_2 : TopologicalSpace Z₁]
[inst_3 : TopologicalSpace Z₂] {f₁ : X₁ → Y₁} {g₁ : Z₁ → Y₁} {f₂ : X₂ → Y₂} {g₂ : Z₂ → Y₂} {mapX : X₁ → X₂},
Continuous mapX →
∀ {mapY : Y₁ → Y₂} {mapZ : Z₁ → Z₂},
Continuous mapZ →
∀ {commX : f₂ ∘ mapX = mapY ∘ f₁} {commZ : g₂ ∘ mapZ = mapY ∘ g₁},
Continuous (Function.mapPullback mapX mapY mapZ commX commZ)
This theorem states that for any continuous functions `mapX : X₁ → X₂` and `mapZ : Z₁ → Z₂`, and two commutative diagrams `f₂ ∘ mapX = mapY ∘ f₁` and `g₂ ∘ mapZ = mapY ∘ g₁` where `f₁ : X₁ → Y₁`, `g₁ : Z₁ → Y₁`, `f₂ : X₂ → Y₂`, `g₂ : Z₂ → Y₂` and `mapY : Y₁ → Y₂`, the function obtained by pulling back along `mapX`, `mapY`, and `mapZ` is also continuous. In other words, the pullback of continuous maps is still continuous under the given commutative conditions. Here, (`X₁`, `X₂`, `Y₁`, `Y₂`, `Z₁`, `Z₂`) are types equipped with topological space structures.
More concisely: Given continuous functions `mapX: X₁ -> X₂`, `mapZ: Z₁ -> Z₂`, and commutative diagrams `f₂ ∘ mapX = mapY ∘ f₁` and `g₂ ∘ mapZ = mapY ∘ g₁` with `f₁: X₁ -> Y₁`, `g₁: Z₁ -> Y₁`, `f₂: X₂ -> Y₂`, `g₂: Z₂ -> Y₂`, and `mapY: Y₁ -> Y₂` on topological spaces `X₁`, `X₂`, `Y₁`, `Y₂`, `Z₁`, and `Z₂`, the pullback function `(mapX ∘ mapY ∘ mapZ)` is continuous.
|
embedding_toPullbackDiag
theorem embedding_toPullbackDiag :
∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] (f : X → Y), Embedding (toPullbackDiag f)
The theorem `embedding_toPullbackDiag` states that for any types `X` and `Y`, where `X` is equipped with a topological space structure, and given any function `f : X → Y`, the function `toPullbackDiag f` (which maps each element `x` of `X` to the pullback of `f` over itself at `x`) is an embedding. In terms of topology, an embedding is a function that is both injective and continuous, and its image is a homeomorphic copy of its domain in the codomain. This theorem indicates that the "diagonal map" to the pullback (i.e., the pair `(x, x)`) preserves the topological structure.
More concisely: The function `toPullbackDiag : X → Set Y` defined as the pullback of a continuous function `f : X → Y` along the diagonal embedding of `X` is an embedding.
|