The compact-open topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

compact_open is the compact-open topology on C(α, β). It is declared as an instance.
continuous_map.coev is the coevaluation map β → C(α, β × α). It is always continuous.
continuous_map.curry is the currying map C(α × β, γ) → C(α, C(β, γ)). This map always exists and it is continuous as long as α × β is locally compact.
continuous_map.uncurry is the uncurrying map C(α, C(β, γ)) → C(α × β, γ). For this map to exist, we need β to be locally compact. If α is also locally compact, then this map is continuous.
homeomorph.curry combines the currying and uncurrying operations into a homeomorphism C(α × β, γ) ≃ₜ 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 β) :

set C(α, β)

A generating set for the compact-open topology (when s is compact and u is open).

Equations

continuous_map.compact_open.gen s u = {f : C(α, β) | ⇑f '' s ⊆ u}

source

@[simp]

theorem continuous_map.gen_empty {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (u : set β) :

continuous_map.compact_open.gen ∅ u = set.univ

source

@[simp]

theorem continuous_map.gen_univ {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set α) :

continuous_map.compact_open.gen s set.univ = set.univ

source

@[simp]

theorem continuous_map.gen_inter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set α) (u v : set β) :

continuous_map.compact_open.gen s (u ∩ v) = continuous_map.compact_open.gen s u ∩ continuous_map.compact_open.gen s v

source

@[simp]

theorem continuous_map.gen_union {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s t : set α) (u : set β) :

continuous_map.compact_open.gen (s ∪ t) u = continuous_map.compact_open.gen s u ∩ continuous_map.compact_open.gen t u

source

theorem continuous_map.gen_empty_right {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} (h : s.nonempty) :

continuous_map.compact_open.gen s ∅ = ∅

source

@[protected, instance]

def continuous_map.compact_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

topological_space C(α, β)

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}

source

@[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) :

is_open (continuous_map.compact_open.gen s u)

source

theorem continuous_map.continuous_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] (g : C(β, γ)) :

continuous g.comp

C(α, -) is a functor.

source

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

continuous (λ (g : C(β, γ)), g.comp f)

C(-, γ) is a functor.

source

theorem continuous_map.continuous_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] [locally_compact_space β] :

continuous (λ (x : C(α, β) × C(β, γ)), x.snd.comp x.fst)

Composition is a continuous map from C(α, β) × C(β, γ) to C(α, γ), provided that β is locally compact. This is Prop. 9 of Chap. X, §3, №. 4 of Bourbaki's Topologie Générale.

source

theorem continuous_map.continuous.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {X : Type u_4} [topological_space X] [locally_compact_space β] {f : X → C(α, β)} {g : X → C(β, γ)} (hf : continuous f) (hg : continuous g) :

continuous (λ (x : X), (g x).comp (f x))

source

theorem continuous_map.continuous_eval' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [locally_compact_space α] :

continuous (λ (p : C(α, β) × α), ⇑(p.fst) p.snd)

The evaluation map C(α, β) × α → β is continuous if α is locally compact.

source

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)

source

theorem continuous_map.continuous_coe' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [locally_compact_space α] :

continuous coe_fn

source

@[protected, instance]

def continuous_map.t2_space {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [t2_space β] :

t2_space C(α, β)

source

theorem continuous_map.compact_open_le_induced {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (s : set α) :

continuous_map.compact_open ≤ topological_space.induced (continuous_map.restrict s) continuous_map.compact_open

source

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 α.

source

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.

source

theorem continuous_map.nhds_compact_open_eq_Inf_nhds_induced {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : C(α, β)) :

nhds f = ⨅ (s : set α) (hs : is_compact s), filter.comap (continuous_map.restrict s) (nhds (continuous_map.restrict s f))

source

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 (nhds f)) (s : set α) :

filter.tendsto (λ (i : ι), continuous_map.restrict s (F i)) l (nhds (continuous_map.restrict s f))

source

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 (nhds f) ↔ ∀ (s : set α), is_compact s → filter.tendsto (λ (i : ι), continuous_map.restrict s (F i)) l (nhds (continuous_map.restrict s f))

source

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 (nhds f)) ↔ ∀ (s : set α), is_compact s → (∃ (f : C(↥s, β)), filter.tendsto (λ (i : ι), continuous_map.restrict s (F i)) l (nhds 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 α.

source

def continuous_map.coev (α : Type u_1) (β : Type u_2) [topological_space α] [topological_space β] (b : β) :

C(α, β × α)

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 := _}

source

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

source

theorem continuous_map.continuous_coev {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

continuous (continuous_map.coev α β)

source

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

f.curry' a = {to_fun := function.curry ⇑f a, continuous_to_fun := _}

source

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

continuous f.curry'

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

source

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))) :

continuous f

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

source

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

f.curry = {to_fun := f.curry', continuous_to_fun := _}

source

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

continuous continuous_map.curry

The currying process is a continuous map between function spaces.

source

@[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 : β) :

⇑(⇑(f.curry) a) b = ⇑f (a, b)

source

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 α × β → γ.

source

@[simp]

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

⇑(f.uncurry) ᾰ = function.uncurry (λ (x : α) (y : β), ⇑(⇑f x) y) ᾰ

source

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

f.uncurry = {to_fun := function.uncurry (λ (x : α) (y : β), ⇑(⇑f x) y), continuous_to_fun := _}

source

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 β] :

continuous continuous_map.uncurry

The uncurrying process is a continuous map between function spaces.

source

def continuous_map.const' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

C(β, C(α, β))

The family of constant maps: β → C(α, β) as a continuous map.

Equations

continuous_map.const' = {to_fun := prod.fst α, continuous_to_fun := _}.curry

source

@[simp]

theorem continuous_map.coe_const' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

⇑continuous_map.const' = continuous_map.const α

source

theorem continuous_map.continuous_const' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

continuous (continuous_map.const α)

source

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

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 := _}

source

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

homeomorph.continuous_map_of_unique = {to_equiv := {to_fun := continuous_map.const α _inst_2, inv_fun := λ (f : C(α, β)), ⇑f inhabited.default, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

source

@[simp]

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

⇑(⇑homeomorph.continuous_map_of_unique b) a = b

source

@[simp]

theorem homeomorph.continuous_map_of_unique_symm_apply {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [unique α] (f : C(α, β)) :

⇑(homeomorph.continuous_map_of_unique.symm) f = ⇑f inhabited.default

source

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))) :

continuous g

source

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))) :

continuous g