mathlib documentation

topology.compact_open

The compact-open topology #

In this file, we define the compact-open topology on the set of continuous maps between two topological spaces.

Main definitions #

Tags #

compact-open, curry, function space

def continuous_map.compact_open.gen {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set α) (u : set β) :
set C(α, β)
Equations
@[instance]
def continuous_map.compact_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
Equations
def continuous_map.induced {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} (hg : continuous g) (f : C(α, β)) :
C(α, γ)
Equations
theorem continuous_map.continuous_induced {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} (hg : continuous g) :

C(α, -) is a functor.

def continuous_map.ev (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] (p : C(α, β) × α) :
β
Equations
def continuous_map.coev (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] (b : β) :
C(α, β × α)
Equations
theorem continuous_map.image_coev {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {y : β} (s : set α) :
(continuous_map.coev α β y) '' s = {y}.prod s
theorem continuous_map.continuous_coev {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
def continuous_map.curry' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : C(α × β, γ)) (a : α) :
C(β, γ)

Auxiliary definition, see continuous_map.curry and homeomorph.curry.

Equations
theorem continuous_map.continuous_curry' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : C(α × β, γ)) :

If a map α × β → γ is continuous, then its curried form α → C(β, γ) is continuous.

theorem continuous_map.continuous_of_continuous_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : α → C(β, γ)) (h : continuous (function.uncurry (λ (x : α) (y : β), (f x) y))) :

To show continuity of a map α → C(β, γ), it suffices to show that its uncurried form α × β → γ is continuous.

def continuous_map.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (f : C(α × β, γ)) :
C(α, C(β, γ))

The curried form of a continuous map α × β → γ as a continuous map α → C(β, γ). If a × β is locally compact, this is continuous. If α and β are both locally compact, then this is a homeomorphism, see homeomorph.curry.

Equations
theorem continuous_map.continuous_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [locally_compact_space × β)] :

The currying process is a continuous map between function spaces.

theorem continuous_map.continuous_uncurry_of_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [locally_compact_space β] (f : C(α, C(β, γ))) :
continuous (function.uncurry (λ (x : α) (y : β), (f x) y))

The uncurried form of a continuous map α → C(β, γ) is a continuous map α × β → γ.

def continuous_map.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [locally_compact_space β] (f : C(α, C(β, γ))) :
C(α × β, γ)

The uncurried form of a continuous map α → C(β, γ) as a continuous map α × β → γ (if β is locally compact). If α is also locally compact, then this is a homeomorphism between the two function spaces, see homeomorph.curry.

Equations

The uncurrying process is a continuous map between function spaces.

def homeomorph.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [locally_compact_space α] [locally_compact_space β] :
C(α × β, γ) ≃ₜ C(α, C(β, γ))

Currying as a homeomorphism between the function spaces C(α × β, γ) and C(α, C(β, γ)).

Equations
def homeomorph.continuous_map_of_unique {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [unique α] :
β ≃ₜ C(α, β)

If α has a single element, then β is homeomorphic to C(α, β).

Equations
@[simp]
theorem homeomorph.continuous_map_of_unique_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [unique α] (b : β) (a : α) :