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(X, Y). It is declared as an instance.
ContinuousMap.coev is the coevaluation map Y → C(X, Y × X). It is always continuous.
ContinuousMap.curry is the currying map C(X × Y, Z) → C(X, C(Y, Z)). This map always exists and it is continuous as long as X × Y is locally compact.
ContinuousMap.uncurry is the uncurrying map C(X, C(Y, Z)) → C(X × Y, Z). For this map to exist, we need Y to be locally compact. If X is also locally compact, then this map is continuous.
Homeomorph.curry combines the currying and uncurrying operations into a homeomorphism C(X × Y, Z) ≃ₜ C(X, C(Y, Z)). This homeomorphism exists if X and Y are locally compact.

Tags #

compact-open, curry, function space

def ContinuousMap.CompactOpen.gen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (u : Set Y) :

Set C(X, Y)

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

Equations

ContinuousMap.CompactOpen.gen s u = {f : C(X, Y) | ⇑f '' s ⊆ u}

Instances For

source

@[simp]

theorem ContinuousMap.gen_empty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (u : Set Y) :

ContinuousMap.CompactOpen.gen ∅ u = Set.univ

source

@[simp]

theorem ContinuousMap.gen_univ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) :

ContinuousMap.CompactOpen.gen s Set.univ = Set.univ

source

@[simp]

theorem ContinuousMap.gen_inter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (u : Set Y) (v : Set Y) :

ContinuousMap.CompactOpen.gen s (u ∩ v) = ContinuousMap.CompactOpen.gen s u ∩ ContinuousMap.CompactOpen.gen s v

source

@[simp]

theorem ContinuousMap.gen_union {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) (t : Set X) (u : Set Y) :

ContinuousMap.CompactOpen.gen (s ∪ t) u = ContinuousMap.CompactOpen.gen s u ∩ ContinuousMap.CompactOpen.gen t u

source

theorem ContinuousMap.gen_empty_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (h : Set.Nonempty s) :

ContinuousMap.CompactOpen.gen s ∅ = ∅

source

instance ContinuousMap.compactOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

TopologicalSpace C(X, Y)

Equations

ContinuousMap.compactOpen = TopologicalSpace.generateFrom {m : Set C(X, Y) | ∃ (s : Set X) (_ : IsCompact s) (u : Set Y) (_ : IsOpen u), m = ContinuousMap.CompactOpen.gen s u}

source

theorem ContinuousMap.compactOpen_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

ContinuousMap.compactOpen = TopologicalSpace.generateFrom (Set.image2 ContinuousMap.CompactOpen.gen {s : Set X | IsCompact s} {t : Set Y | IsOpen t})

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

source

theorem ContinuousMap.isOpen_gen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (hs : IsCompact s) {u : Set Y} (hu : IsOpen u) :

IsOpen (ContinuousMap.CompactOpen.gen s u)

source

theorem ContinuousMap.isOpen_setOf_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {K : Set X} (hK : IsCompact K) {U : Set Y} (hU : IsOpen U) :

IsOpen {f : C(X, Y) | Set.MapsTo (⇑f) K U}

source

theorem ContinuousMap.eventually_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {K : Set X} {U : Set Y} (hK : IsCompact K) (hU : IsOpen U) (h : Set.MapsTo (⇑f) K U) :

∀ᶠ (g : C(X, Y)) in nhds f, Set.MapsTo (⇑g) K U

source

theorem ContinuousMap.tendsto_nhds_compactOpen {Y : Type u_2} {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] {α : Type u_4} {l : Filter α} {f : α → C(Y, Z)} {g : C(Y, Z)} :

Filter.Tendsto f l (nhds g) ↔ ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → Set.MapsTo (⇑g) K U → ∀ᶠ (a : α) in l, Set.MapsTo (⇑(f a)) K U

source

theorem ContinuousMap.continuous_compactOpen {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → C(Y, Z)} :

Continuous f ↔ ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → IsOpen {x : X | Set.MapsTo (⇑(f x)) K U}

source

theorem ContinuousMap.continuous_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) :

Continuous (ContinuousMap.comp g)

C(X, -) is a functor.

source

theorem ContinuousMap.inducing_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (hg : Inducing ⇑g) :

Inducing (ContinuousMap.comp g)

If g : C(Y, Z) is a topology inducing map, then the composition ContinuousMap.comp g : C(X, Y) → C(X, Z) is a topology inducing map too.

source

theorem ContinuousMap.embedding_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (hg : Embedding ⇑g) :

Embedding (ContinuousMap.comp g)

If g : C(Y, Z) is a topological embedding, then the composition ContinuousMap.comp g : C(X, Y) → C(X, Z) is an embedding too.

source

theorem ContinuousMap.continuous_comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X, Y)) :

Continuous fun (g : C(Y, Z)) => ContinuousMap.comp g f

C(-, Z) is a functor.

source

theorem ContinuousMap.continuous_comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactPair Y Z] :

Continuous fun (x : C(X, Y) × C(Y, Z)) => ContinuousMap.comp x.2 x.1

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

source

theorem ContinuousMap.continuous.comp' {Y : Type u_2} {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] {X : Type u_4} [TopologicalSpace X] [LocallyCompactPair Y Z] {f : X → C(X, Y)} {g : X → C(Y, Z)} (hf : Continuous f) (hg : Continuous g) :

Continuous fun (x : X) => ContinuousMap.comp (g x) (f x)

source

theorem ContinuousMap.continuous_eval {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactPair X Y] :

Continuous fun (p : C(X, Y) × X) => p.1 p.2

The evaluation map C(X, Y) × X → Y is continuous if X, Y is a locally compact pair of spaces.

source

@[deprecated ContinuousMap.continuous_eval]

theorem ContinuousMap.continuous_eval' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactPair X Y] :

Continuous fun (p : C(X, Y) × X) => p.1 p.2

Alias of ContinuousMap.continuous_eval.

The evaluation map C(X, Y) × X → Y is continuous if X, Y is a locally compact pair of spaces.

source

theorem ContinuousMap.continuous_eval_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (x : X) :

Continuous fun (f : C(X, Y)) => f x

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

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

source

theorem ContinuousMap.continuous_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

Continuous FunLike.coe

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

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

source

theorem ContinuousMap.isClosed_setOf_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {t : Set Y} (ht : IsClosed t) (s : Set X) :

IsClosed {f : C(X, Y) | Set.MapsTo (⇑f) s t}

source

theorem ContinuousMap.isClopen_setOf_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {K : Set X} (hK : IsCompact K) {U : Set Y} (hU : IsClopen U) :

IsClopen {f : C(X, Y) | Set.MapsTo (⇑f) K U}

source

instance ContinuousMap.instT0SpaceContinuousMapCompactOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space Y] :

T0Space C(X, Y)

Equations

(_ : T0Space C(X, Y)) = (_ : T0Space C(X, Y))

source

instance ContinuousMap.instT1SpaceContinuousMapCompactOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] :

T1Space C(X, Y)

Equations

(_ : T1Space C(X, Y)) = (_ : T1Space C(X, Y))

source

instance ContinuousMap.instT2SpaceContinuousMapCompactOpen {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] :

T2Space C(X, Y)

Equations

(_ : T2Space C(X, Y)) = (_ : T2Space C(X, Y))

source

theorem ContinuousMap.compactOpen_le_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) :

ContinuousMap.compactOpen ≤ TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen

source

theorem ContinuousMap.compactOpen_eq_sInf_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

ContinuousMap.compactOpen = ⨅ (s : Set X), ⨅ (_ : IsCompact s), TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen

The compact-open topology on C(X, Y) is equal to the infimum of the compact-open topologies on C(s, Y) for s a compact subset of X. The key point of the proof is that the union of the compact subsets of X is equal to the union of compact subsets of the compact subsets of X.

source

theorem ContinuousMap.continuous_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set X) :

Continuous fun (F : C(X, Y)) => ContinuousMap.restrict s F

For any subset s of X, the restriction of continuous functions to s is continuous as a function from C(X, Y) to C(s, Y) with their respective compact-open topologies.

source

theorem ContinuousMap.nhds_compactOpen_eq_sInf_nhds_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :

nhds f = ⨅ (s : Set X), ⨅ (_ : IsCompact s), Filter.comap (ContinuousMap.restrict s) (nhds (ContinuousMap.restrict s f))

source

theorem ContinuousMap.tendsto_compactOpen_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {ι : Type u_4} {l : Filter ι} {F : ι → C(X, Y)} {f : C(X, Y)} (hFf : Filter.Tendsto F l (nhds f)) (s : Set X) :

Filter.Tendsto (fun (i : ι) => ContinuousMap.restrict s (F i)) l (nhds (ContinuousMap.restrict s f))

source

theorem ContinuousMap.tendsto_compactOpen_iff_forall {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {ι : Type u_4} {l : Filter ι} (F : ι → C(X, Y)) (f : C(X, Y)) :

Filter.Tendsto F l (nhds f) ↔ ∀ (s : Set X), IsCompact s → Filter.Tendsto (fun (i : ι) => ContinuousMap.restrict s (F i)) l (nhds (ContinuousMap.restrict s f))

source

theorem ContinuousMap.exists_tendsto_compactOpen_iff_forall {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace X] [T2Space Y] {ι : Type u_4} {l : Filter ι} [Filter.NeBot l] (F : ι → C(X, Y)) :

(∃ (f : C(X, Y)), Filter.Tendsto F l (nhds f)) ↔ ∀ (s : Set X), IsCompact s → ∃ (f : C(↑s, Y)), Filter.Tendsto (fun (i : ι) => ContinuousMap.restrict s (F i)) l (nhds f)

A family F of functions in C(X, Y) converges in the compact-open topology, if and only if it converges in the compact-open topology on each compact subset of X.

source

def ContinuousMap.coev (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] (y : Y) :

C(X, Y × X)

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

Equations

ContinuousMap.coev X Y y = ContinuousMap.mk (Prod.mk y)

Instances For

source

theorem ContinuousMap.image_coev {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {y : Y} (s : Set X) :

⇑(ContinuousMap.coev X Y y) '' s = {y} ×ˢ s

source

theorem ContinuousMap.continuous_coev {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

Continuous (ContinuousMap.coev X Y)

source

def ContinuousMap.curry' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X × Y, Z)) (x : X) :

C(Y, Z)

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

Equations

ContinuousMap.curry' f x = ContinuousMap.mk (Function.curry (⇑f) x)

Instances For

source

theorem ContinuousMap.continuous_curry' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X × Y, Z)) :

Continuous (ContinuousMap.curry' f)

If a map X × Y → Z is continuous, then its curried form X → C(Y, Z) is continuous.

source

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

Continuous f

To show continuity of a map X → C(Y, Z), it suffices to show that its uncurried form X × Y → Z is continuous.

source

def ContinuousMap.curry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X × Y, Z)) :

C(X, C(Y, Z))

The curried form of a continuous map X × Y → Z as a continuous map X → C(Y, Z). If X × Y is locally compact, this is continuous. If X and Y are both locally compact, then this is a homeomorphism, see Homeomorph.curry.

Equations

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

Instances For

source

@[simp]

theorem ContinuousMap.curry_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X × Y, Z)) (x : X) (y : Y) :

((ContinuousMap.curry f) x) y = f (x, y)

source

theorem ContinuousMap.continuous_curry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace (X × Y)] :

Continuous ContinuousMap.curry

The currying process is a continuous map between function spaces.

source

theorem ContinuousMap.continuous_uncurry_of_continuous {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :

Continuous (Function.uncurry fun (x : X) (y : Y) => (f x) y)

The uncurried form of a continuous map X → C(Y, Z) is a continuous map X × Y → Z.

source

@[simp]

theorem ContinuousMap.uncurry_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :

∀ (a : X × Y), (ContinuousMap.uncurry f) a = Function.uncurry (fun (x : X) (y : Y) => (f x) y) a

source

def ContinuousMap.uncurry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :

C(X × Y, Z)

The uncurried form of a continuous map X → C(Y, Z) as a continuous map X × Y → Z (if Y is locally compact). If X 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 : X) (y : Y) => (f x) y)

Instances For

source

theorem ContinuousMap.continuous_uncurry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace X] [LocallyCompactSpace Y] :

Continuous ContinuousMap.uncurry

The uncurrying process is a continuous map between function spaces.

source

def ContinuousMap.const' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

C(Y, C(X, Y))

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

Equations

ContinuousMap.const' = ContinuousMap.curry ContinuousMap.fst

Instances For

source

@[simp]

theorem ContinuousMap.coe_const' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

⇑ContinuousMap.const' = ContinuousMap.const X

source

theorem ContinuousMap.continuous_const' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

Continuous (ContinuousMap.const X)

source

def Homeomorph.curry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [LocallyCompactSpace X] [LocallyCompactSpace Y] :

C(X × Y, Z) ≃ₜ C(X, C(Y, Z))

Currying as a homeomorphism between the function spaces C(X × Y, Z) and C(X, C(Y, Z)).

Equations

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

Instances For

source

def Homeomorph.continuousMapOfUnique {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Unique X] :

Y ≃ₜ C(X, Y)

If X has a single element, then Y is homeomorphic to C(X, Y).

Equations

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

Instances For

source

@[simp]

theorem Homeomorph.continuousMapOfUnique_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Unique X] (y : Y) (x : X) :

(Homeomorph.continuousMapOfUnique y) x = y

source

@[simp]

theorem Homeomorph.continuousMapOfUnique_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [Unique X] (f : C(X, Y)) :

(Homeomorph.symm Homeomorph.continuousMapOfUnique) f = f default

source

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 : X₀ × Y) => g (f p.1, p.2)) :

Continuous g

source

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 : Y × X₀) => g (p.1, f p.2)) :

Continuous g