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 #
compact_openis the compact-open topology onC(α, β). It is declared as an instance.continuous_map.coevis the coevaluation mapβ → C(α, β × α). It is always continuous.continuous_map.curryis the currying mapC(α × β, γ) → C(α, C(β, γ)). This map always exists and it is continuous as long asα × βis locally compact.continuous_map.uncurryis the uncurrying mapC(α, C(β, γ)) → C(α × β, γ). For this map to exist, we needβto be locally compact. Ifαis also locally compact, then this map is continuous.homeomorph.currycombines the currying and uncurrying operations into a homeomorphismC(α × β, γ) ≃ₜ C(α, C(β, γ)). This homeomorphism exists ifαandβare locally compact.
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 β) :
A generating set for the compact-open topology (when s is compact and u is open).
@[simp]
theorem
continuous_map.gen_empty
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(u : set β) :
@[simp]
theorem
continuous_map.gen_univ
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : set α) :
@[simp]
theorem
continuous_map.gen_inter
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : set α)
(u v : set β) :
@[simp]
theorem
continuous_map.gen_union
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s t : set α)
(u : set β) :
@[protected, instance]
def
continuous_map.compact_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
Equations
- continuous_map.compact_open = topological_space.generate_from {m : set C(α, β) | ∃ (s : set α) (hs : is_compact s) (u : set β) (hu : is_open u), m = continuous_map.compact_open.gen s u}
@[protected]
theorem
continuous_map.is_open_gen
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{s : set α}
(hs : is_compact s)
{u : set β}
(hu : is_open u) :
theorem
continuous_map.continuous_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(g : C(β, γ)) :
C(α, -) is a functor.
theorem
continuous_map.continuous_eval'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[locally_compact_space α] :
The evaluation map C(α, β) × α → β is continuous if α is locally compact.
See also continuous_map.continuous_eval
theorem
continuous_map.continuous_eval_const'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[locally_compact_space α]
(a : α) :
continuous (λ (f : C(α, β)), ⇑f a)
See also continuous_map.continuous_eval_const
theorem
continuous_map.continuous_coe'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[locally_compact_space α] :
See also continuous_map.continuous_coe
@[protected, instance]
def
continuous_map.t2_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[t2_space β] :
theorem
continuous_map.compact_open_le_induced
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : set α) :
theorem
continuous_map.compact_open_eq_Inf_induced
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
continuous_map.compact_open = ⨅ (s : set α) (hs : is_compact s), topological_space.induced (continuous_map.restrict s) continuous_map.compact_open
The compact-open topology on C(α, β) is equal to the infimum of the compact-open topologies
on C(s, β) for s a compact subset of α. The key point of the proof is that the union of the
compact subsets of α is equal to the union of compact subsets of the compact subsets of α.
theorem
continuous_map.continuous_restrict
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(s : set α) :
continuous (λ (F : C(α, β)), continuous_map.restrict s F)
For any subset s of α, the restriction of continuous functions to s is continuous as a
function from C(α, β) to C(s, β) with their respective compact-open topologies.
theorem
continuous_map.nhds_compact_open_eq_Inf_nhds_induced
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : C(α, β)) :
𝓝 f = ⨅ (s : set α) (hs : is_compact s), filter.comap (continuous_map.restrict s) (𝓝 (continuous_map.restrict s f))
theorem
continuous_map.tendsto_compact_open_restrict
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{ι : Type u_3}
{l : filter ι}
{F : ι → C(α, β)}
{f : C(α, β)}
(hFf : filter.tendsto F l (𝓝 f))
(s : set α) :
filter.tendsto (λ (i : ι), continuous_map.restrict s (F i)) l (𝓝 (continuous_map.restrict s f))
theorem
continuous_map.tendsto_compact_open_iff_forall
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{ι : Type u_3}
{l : filter ι}
(F : ι → C(α, β))
(f : C(α, β)) :
filter.tendsto F l (𝓝 f) ↔ ∀ (s : set α), is_compact s → filter.tendsto (λ (i : ι), continuous_map.restrict s (F i)) l (𝓝 (continuous_map.restrict s f))
theorem
continuous_map.exists_tendsto_compact_open_iff_forall
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[locally_compact_space α]
[t2_space α]
[t2_space β]
{ι : Type u_3}
{l : filter ι}
[l.ne_bot]
(F : ι → C(α, β)) :
(∃ (f : C(α, β)), filter.tendsto F l (𝓝 f)) ↔ ∀ (s : set α), is_compact s → (∃ (f : C(↥s, β)), filter.tendsto (λ (i : ι), continuous_map.restrict s (F i)) l (𝓝 f))
A family F of functions in C(α, β) converges in the compact-open topology, if and only if
it converges in the compact-open topology on each compact subset of α.
def
continuous_map.coev
(α : Type u_1)
(β : Type u_2)
[topological_space α]
[topological_space β]
(b : β) :
The coevaluation map β → C(α, β × α) sending a point x : β to the continuous function
on α sending y to (x, y).
Equations
- continuous_map.coev α β b = {to_fun := prod.mk b, continuous_to_fun := _}
theorem
continuous_map.image_coev
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{y : β}
(s : set α) :
⇑(continuous_map.coev α β y) '' s = {y} ×ˢ 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 : α) :
Auxiliary definition, see continuous_map.curry and homeomorph.curry.
Equations
- f.curry' a = {to_fun := function.curry ⇑f a, continuous_to_fun := _}
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(α × β, γ)) :
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.
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.
@[simp]
theorem
continuous_map.curry_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
(f : C(α × β, γ))
(a : α)
(b : β) :
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(β, γ))) :
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
- f.uncurry = {to_fun := function.uncurry (λ (x : α) (y : β), ⇑(⇑f x) y), continuous_to_fun := _}
theorem
continuous_map.continuous_uncurry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
[locally_compact_space α]
[locally_compact_space β] :
The uncurrying process is a continuous map between function spaces.
def
continuous_map.const'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
The family of constant maps: β → C(α, β) as a continuous map.
Equations
- continuous_map.const' = {to_fun := prod.fst α, continuous_to_fun := _}.curry
@[simp]
theorem
continuous_map.coe_const'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
theorem
continuous_map.continuous_const'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
def
homeomorph.curry
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
[locally_compact_space α]
[locally_compact_space β] :
Currying as a homeomorphism between the function spaces C(α × β, γ) and C(α, C(β, γ)).
Equations
- homeomorph.curry = {to_equiv := {to_fun := continuous_map.curry _inst_3, inv_fun := continuous_map.uncurry _inst_5, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.continuous_map_of_unique
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[unique α] :
If α has a single element, then β is homeomorphic to C(α, β).
Equations
- homeomorph.continuous_map_of_unique = {to_equiv := {to_fun := continuous_map.const α _inst_2, inv_fun := λ (f : C(α, β)), ⇑f default, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.continuous_map_of_unique_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[unique α]
(b : β)
(a : α) :
@[simp]
theorem
homeomorph.continuous_map_of_unique_symm_apply
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[unique α]
(f : C(α, β)) :
theorem
quotient_map.continuous_lift_prod_left
{X₀ : Type u_1}
{X : Type u_2}
{Y : Type u_3}
{Z : Type u_4}
[topological_space X₀]
[topological_space X]
[topological_space Y]
[topological_space Z]
[locally_compact_space Y]
{f : X₀ → X}
(hf : quotient_map f)
{g : X × Y → Z}
(hg : continuous (λ (p : X₀ × Y), g (f p.fst, p.snd))) :
theorem
quotient_map.continuous_lift_prod_right
{X₀ : Type u_1}
{X : Type u_2}
{Y : Type u_3}
{Z : Type u_4}
[topological_space X₀]
[topological_space X]
[topological_space Y]
[topological_space Z]
[locally_compact_space Y]
{f : X₀ → X}
(hf : quotient_map f)
{g : Y × X → Z}
(hg : continuous (λ (p : Y × X₀), g (p.fst, f p.snd))) :