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

• CompactOpen is the compact-open topology on C(α, β). It is declared as an instance.
• ContinuousMap.coev is the coevaluation map β → C(α, β × α). It is always continuous.
• ContinuousMap.curry is the currying map C(α × β, γ) → C(α, C(β, γ)). This map always exists and it is continuous as long as α × β is locally compact.
• ContinuousMap.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 ContinuousMap.CompactOpen.gen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (u : Set β) : Set C(α, β)

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

Equations

• ContinuousMap.CompactOpen.gen s u = {f | ↑f '' s ⊆ u}

@[simp]

theorem ContinuousMap.gen_empty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (u : Set β) : ContinuousMap.CompactOpen.gen ∅ u = Set.univ

@[simp]

theorem ContinuousMap.gen_univ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) : ContinuousMap.CompactOpen.gen s Set.univ = Set.univ

@[simp]

theorem ContinuousMap.gen_inter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (u : Set β) (v : Set β) : ContinuousMap.CompactOpen.gen s (u ∩ v) = ContinuousMap.CompactOpen.gen s u ∩ ContinuousMap.CompactOpen.gen s v

@[simp]

theorem ContinuousMap.gen_union {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (t : Set α) (u : Set β) : ContinuousMap.CompactOpen.gen (s ∪ t) u = ContinuousMap.CompactOpen.gen s u ∩ ContinuousMap.CompactOpen.gen t u

theorem ContinuousMap.gen_empty_right {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (h : Set.Nonempty s) : ContinuousMap.CompactOpen.gen s ∅ = ∅

instance ContinuousMap.compactOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : TopologicalSpace C(α, β)

Equations

• ContinuousMap.compactOpen = TopologicalSpace.generateFrom {m | ∃ s x u x, m = ContinuousMap.CompactOpen.gen s u}

theorem ContinuousMap.compactOpen_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : ContinuousMap.compactOpen = TopologicalSpace.generateFrom (Set.image2 ContinuousMap.CompactOpen.gen {s | IsCompact s} {t | IsOpen t})

Definition of ContinuousMap.compactOpen in terms of Set.image2.

theorem ContinuousMap.isOpen_gen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (hs : IsCompact s) {u : Set β} (hu : IsOpen u) : IsOpen (ContinuousMap.CompactOpen.gen s u)

theorem ContinuousMap.continuous_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (g : C(β, γ)) : Continuous (ContinuousMap.comp g)

C(α, -) is a functor.

theorem ContinuousMap.inducing_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (g : C(β, γ)) (hg : Inducing ↑g) : Inducing (ContinuousMap.comp g)

If g : C(β, γ) is a topology inducing map, then the composition ContinuousMap.comp g : C(α, β) → C(α, γ) is a topology inducing map too.

theorem ContinuousMap.embedding_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (g : C(β, γ)) (hg : Embedding ↑g) : Embedding (ContinuousMap.comp g)

If g : C(β, γ) is a topological embedding, then the composition ContinuousMap.comp g : C(α, β) → C(α, γ) is an embedding too.

theorem ContinuousMap.continuous_comp_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(α, β)) : Continuous fun g => ContinuousMap.comp g f

C(-, γ) is a functor.

theorem ContinuousMap.continuous_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [LocallyCompactSpace β] : Continuous fun x => ContinuousMap.comp x.snd 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.

theorem ContinuousMap.continuous.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {X : Type u_4} [TopologicalSpace X] [LocallyCompactSpace β] {f : X → C(α, β)} {g : X → C(β, γ)} (hf : Continuous f) (hg : Continuous g) : Continuous fun x => ContinuousMap.comp (g x) (f x)

theorem ContinuousMap.continuous_eval' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace α] : Continuous fun p => ↑p.fst p.snd

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

See also ContinuousMap.continuous_eval

theorem ContinuousMap.continuous_eval_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (a : α) : Continuous fun f => ↑f a

Evaluation of a continuous map f at a point a is continuous in f.

Porting note: merged continuous_eval_const with continuous_eval_const' removing unneeded assumptions.

theorem ContinuousMap.continuous_coe {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : Continuous FunLike.coe

Coercion from C(α, β) with compact-open topology to α → β with pointwise convergence topology is a continuous map.

Porting note: merged continuous_coe with continuous_coe' removing unneeded assumptions.

instance ContinuousMap.instT0SpaceContinuousMapCompactOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T0Space β] : T0Space C(α, β)

Equations

• @ContinuousMap.instT0SpaceContinuousMapCompactOpen = @ContinuousMap.instT0SpaceContinuousMapCompactOpen.proof_1

instance ContinuousMap.instT1SpaceContinuousMapCompactOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T1Space β] : T1Space C(α, β)

Equations

• @ContinuousMap.instT1SpaceContinuousMapCompactOpen = @ContinuousMap.instT1SpaceContinuousMapCompactOpen.proof_1

instance ContinuousMap.instT2SpaceContinuousMapCompactOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] : T2Space C(α, β)

Equations

• @ContinuousMap.instT2SpaceContinuousMapCompactOpen = @ContinuousMap.instT2SpaceContinuousMapCompactOpen.proof_1

theorem ContinuousMap.compactOpen_le_induced {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) : ContinuousMap.compactOpen ≤ TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen

theorem ContinuousMap.compactOpen_eq_sInf_induced {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : ContinuousMap.compactOpen = ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen

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 ContinuousMap.continuous_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) : Continuous fun F => ContinuousMap.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 ContinuousMap.nhds_compactOpen_eq_sInf_nhds_induced {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : nhds f = ⨅ (s : Set α) (_ : IsCompact s), Filter.comap (ContinuousMap.restrict s) (nhds (ContinuousMap.restrict s f))

theorem ContinuousMap.tendsto_compactOpen_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Type u_4} {l : Filter ι} {F : ι → C(α, β)} {f : C(α, β)} (hFf : Filter.Tendsto F l (nhds f)) (s : Set α) : Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (nhds (ContinuousMap.restrict s f))

theorem ContinuousMap.tendsto_compactOpen_iff_forall {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Type u_4} {l : Filter ι} (F : ι → C(α, β)) (f : C(α, β)) : Filter.Tendsto F l (nhds f) ↔ ∀ (s : Set α), IsCompact s → Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (nhds (ContinuousMap.restrict s f))

theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [WeaklyLocallyCompactSpace α] [T2Space β] {ι : Type u_4} {l : Filter ι} [Filter.NeBot l] (F : ι → C(α, β)) : (∃ f, Filter.Tendsto F l (nhds f)) ↔ ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => ContinuousMap.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 α.

def ContinuousMap.coev (α : Type u_1) (β : Type u_2) [TopologicalSpace α] [TopologicalSpace β] (b : β) : C(α, β × α)

The coevaluation map β → C(α, β × α) sending a point x : β to the continuous function on α sending y to (x, y).

Equations

• ContinuousMap.coev α β b = ContinuousMap.mk (Prod.mk b)

theorem ContinuousMap.image_coev {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {y : β} (s : Set α) : ↑(ContinuousMap.coev α β y) '' s = {y} ×ˢ s

theorem ContinuousMap.continuous_coev {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : Continuous (ContinuousMap.coev α β)

def ContinuousMap.curry' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(α × β, γ)) (a : α) : C(β, γ)

Auxiliary definition, see ContinuousMap.curry and Homeomorph.curry.

Equations

• ContinuousMap.curry' f a = ContinuousMap.mk (Function.curry (↑f) a)

theorem ContinuousMap.continuous_curry' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(α × β, γ)) : Continuous (ContinuousMap.curry' f)

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

theorem ContinuousMap.continuous_of_continuous_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α → C(β, γ)) (h : Continuous (Function.uncurry fun x y => ↑(f x) y)) : Continuous f

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

def ContinuousMap.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (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

• ContinuousMap.curry f = ContinuousMap.mk (ContinuousMap.curry' f)

@[simp]

theorem ContinuousMap.curry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : C(α × β, γ)) (a : α) (b : β) : ↑(↑(ContinuousMap.curry f) a) b = ↑f (a, b)

theorem ContinuousMap.continuous_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [LocallyCompactSpace (α × β)] : Continuous ContinuousMap.curry

The currying process is a continuous map between function spaces.

theorem ContinuousMap.continuous_uncurry_of_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [LocallyCompactSpace β] (f : C(α, C(β, γ))) : Continuous (Function.uncurry fun x y => ↑(↑f x) y)

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

@[simp]

theorem ContinuousMap.uncurry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [LocallyCompactSpace β] (f : C(α, C(β, γ))) : ∀ (a : α × β), ↑(ContinuousMap.uncurry f) a = Function.uncurry (fun x y => ↑(↑f x) y) a

def ContinuousMap.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [LocallyCompactSpace β] (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

• ContinuousMap.uncurry f = ContinuousMap.mk (Function.uncurry fun x y => ↑(↑f x) y)

theorem ContinuousMap.continuous_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [LocallyCompactSpace α] [LocallyCompactSpace β] : Continuous ContinuousMap.uncurry

The uncurrying process is a continuous map between function spaces.

def ContinuousMap.const' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : C(β, C(α, β))

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

Equations

• ContinuousMap.const' = ContinuousMap.curry ContinuousMap.fst

@[simp]

theorem ContinuousMap.coe_const' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : ↑ContinuousMap.const' = ContinuousMap.const α

theorem ContinuousMap.continuous_const' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] : Continuous (ContinuousMap.const α)

def Homeomorph.curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [LocallyCompactSpace α] [LocallyCompactSpace β] : C(α × β, γ) ≃ₜ C(α, C(β, γ))

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

Equations

• One or more equations did not get rendered due to their size.

def Homeomorph.continuousMapOfUnique {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Unique α] : β ≃ₜ C(α, β)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Homeomorph.continuousMapOfUnique_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Unique α] (b : β) (a : α) : ↑(↑Homeomorph.continuousMapOfUnique b) a = b

@[simp]

theorem Homeomorph.continuousMapOfUnique_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Unique α] (f : C(α, β)) : ↑(Homeomorph.symm Homeomorph.continuousMapOfUnique) f = ↑f default

theorem QuotientMap.continuous_lift_prod_left {X₀ : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X₀] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] {f : X₀ → X} (hf : QuotientMap f) {g : X × Y → Z} (hg : Continuous fun p => g (f p.fst, p.snd)) : Continuous g

theorem QuotientMap.continuous_lift_prod_right {X₀ : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X₀] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] {f : X₀ → X} (hf : QuotientMap f) {g : Y × X → Z} (hg : Continuous fun p => g (p.fst, f p.snd)) : Continuous g