Mathlib.Topology.CompactOpen

ContinuousMap.compactOpen instance

: TopologicalSpace C(X, Y)

Full source

/-- The compact-open topology on the space of continuous maps `C(X, Y)`. -/
instance compactOpen : TopologicalSpace C(X, Y) :=
  .generateFrom <| image2 (fun K U ↦ {f | MapsTo f K U}) {K | IsCompact K} {U | IsOpen U}

Compact-Open Topology on Continuous Function Space

Informal description

The compact-open topology on the space of continuous maps $C(X, Y)$ is the topology generated by sets of the form $\{f \in C(X, Y) \mid f(K) \subseteq U\}$ where $K$ is a compact subset of $X$ and $U$ is an open subset of $Y$.

ContinuousMap.compactOpen_eq theorem

: @compactOpen X Y _ _ = .generateFrom (image2 (fun K U ↦ {f | MapsTo f K U}) {K | IsCompact K} {t | IsOpen t})

Full source

/-- Definition of `ContinuousMap.compactOpen`. -/
theorem compactOpen_eq : @compactOpen X Y _ _ =
    .generateFrom (image2 (fun K U ↦ {f | MapsTo f K U}) {K | IsCompact K} {t | IsOpen t}) :=
   rfl

Compact-Open Topology as Generated by Compact-Open Subsets

Informal description

The compact-open topology on the space of continuous maps $C(X, Y)$ is equal to the topology generated by the collection of all sets of the form $\{f \in C(X, Y) \mid f(K) \subseteq U\}$, where $K$ ranges over all compact subsets of $X$ and $U$ ranges over all open subsets of $Y$.

ContinuousMap.isOpen_setOf_mapsTo theorem

(hK : IsCompact K) (hU : IsOpen U) : IsOpen {f : C(X, Y) | MapsTo f K U}

Full source

theorem isOpen_setOf_mapsTo (hK : IsCompact K) (hU : IsOpen U) :
    IsOpen {f : C(X, Y) | MapsTo f K U} :=
  isOpen_generateFrom_of_mem <| mem_image2_of_mem hK hU

Openness of Maps-to Sets in Compact-Open Topology

Informal description

For any compact subset $K$ of $X$ and any open subset $U$ of $Y$, the set $\{f \in C(X, Y) \mid f(K) \subseteq U\}$ is open in the compact-open topology on $C(X, Y)$.

ContinuousMap.eventually_mapsTo theorem

{f : C(X, Y)} (hK : IsCompact K) (hU : IsOpen U) (h : MapsTo f K U) : ∀ᶠ g : C(X, Y) in 𝓝 f, MapsTo g K U

Full source

lemma eventually_mapsTo {f : C(X, Y)} (hK : IsCompact K) (hU : IsOpen U) (h : MapsTo f K U) :
    ∀ᶠ g : C(X, Y) in 𝓝 f, MapsTo g K U :=
  (isOpen_setOf_mapsTo hK hU).mem_nhds h

Neighborhood Condition for Maps in Compact-Open Topology: $f(K) \subseteq U$ implies $\forall^g \in \mathcal{N}(f), g(K) \subseteq U$

Informal description

Let $X$ and $Y$ be topological spaces, and let $C(X, Y)$ be the space of continuous maps from $X$ to $Y$ equipped with the compact-open topology. For any continuous map $f \in C(X, Y)$, if $K \subseteq X$ is compact, $U \subseteq Y$ is open, and $f(K) \subseteq U$, then there exists a neighborhood $\mathcal{N}(f)$ of $f$ in $C(X, Y)$ such that every $g \in \mathcal{N}(f)$ satisfies $g(K) \subseteq U$.

ContinuousMap.nhds_compactOpen theorem

 (f : C(X, Y)) :
  𝓝 f = ⨅ (K : Set X) (_ : IsCompact K) (U : Set Y) (_ : IsOpen U) (_ : MapsTo f K U), 𝓟 {g : C(X, Y) | MapsTo g K U}

Full source

lemma nhds_compactOpen (f : C(X, Y)) :
    𝓝 f = ⨅ (K : Set X) (_ : IsCompact K) (U : Set Y) (_ : IsOpen U) (_ : MapsTo f K U),
      𝓟 {g : C(X, Y) | MapsTo g K U} := by
  simp_rw [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
    ← image_prod, iInf_image, biInf_prod, mem_setOf_eq]

Neighborhood Filter Characterization in Compact-Open Topology

Informal description

For any continuous map $f \in C(X, Y)$, the neighborhood filter $\mathcal{N}(f)$ in the compact-open topology is given by: \[ \mathcal{N}(f) = \bigsqcap_{\substack{K \subseteq X \text{ compact} \\ U \subseteq Y \text{ open} \\ f(K) \subseteq U}} \mathcal{P}\{g \in C(X, Y) \mid g(K) \subseteq U\}, \] where the infimum is taken over all compact subsets $K$ of $X$ and open subsets $U$ of $Y$ such that $f$ maps $K$ into $U$.

ContinuousMap.tendsto_nhds_compactOpen theorem

 {l : Filter α} {f : α → C(Y, Z)} {g : C(Y, Z)} :
  Tendsto f l (𝓝 g) ↔ ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → ∀ᶠ a in l, MapsTo (f a) K U

Full source

lemma tendsto_nhds_compactOpen {l : Filter α} {f : α → C(Y, Z)} {g : C(Y, Z)} :
    TendstoTendsto f l (𝓝 g) ↔
      ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → ∀ᶠ a in l, MapsTo (f a) K U := by
  simp [nhds_compactOpen]

Characterization of Convergence in Compact-Open Topology: $f \to g$ iff $\forall K \text{ compact}, \forall U \text{ open}, g(K) \subseteq U \Rightarrow \forall^l a, f(a)(K) \subseteq U$

Informal description

Let $X$ and $Y$ be topological spaces, and let $C(Y, Z)$ be the space of continuous maps from $Y$ to $Z$ equipped with the compact-open topology. For any filter $l$ on a type $\alpha$, a function $f : \alpha \to C(Y, Z)$, and a continuous map $g \in C(Y, Z)$, the following are equivalent: 1. The function $f$ tends to $g$ along the filter $l$ in the compact-open topology. 2. For every compact subset $K \subseteq Y$ and every open subset $U \subseteq Z$ such that $g(K) \subseteq U$, the set $\{a \in \alpha \mid f(a)(K) \subseteq U\}$ is eventually in $l$.

ContinuousMap.continuous_compactOpen theorem

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

Full source

lemma continuous_compactOpen {f : X → C(Y, Z)} :
    ContinuousContinuous f ↔ ∀ K, IsCompact K → ∀ U, IsOpen U → IsOpen {x | MapsTo (f x) K U} :=
  continuous_generateFrom_iff.trans forall_mem_image2

Continuity Criterion for Functions into Compact-Open Function Space: $f$ continuous iff preimages of subbasic opens are open

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $C(Y, Z)$ be the space of continuous maps from $Y$ to $Z$ equipped with the compact-open topology. A function $f : X \to C(Y, Z)$ is continuous if and only if for every compact subset $K \subseteq Y$ and every open subset $U \subseteq Z$, the set $\{x \in X \mid f(x)(K) \subseteq U\}$ is open in $X$.

ContinuousMap.hasBasis_nhds theorem

 (f : C(X, Y)) :
  (𝓝 f).HasBasis (fun S : Set (Set X × Set Y) ↦ S.Finite ∧ ∀ K U, (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ MapsTo f K U)
    (⋂ KU ∈ ·, {g : C(X, Y) | MapsTo g KU.1 KU.2})

Full source

protected lemma hasBasis_nhds (f : C(X, Y)) :
    (𝓝 f).HasBasis
      (fun S : Set (SetSet X × Set Y) ↦
        S.Finite ∧ ∀ K U, (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ MapsTo f K U)
      (⋂ KU ∈ ·, {g : C(X, Y) | MapsTo g KU.1 KU.2}) := by
  refine ⟨fun s ↦ ?_⟩
  simp_rw [nhds_compactOpen, iInf_comm.{_, 0, _ + 1}, iInf_prod', iInf_and']
  simp [mem_biInf_principal, and_assoc]

Basis Characterization of Neighborhoods in Compact-Open Topology

Informal description

For any continuous map $f \in C(X, Y)$, the neighborhood filter $\mathcal{N}(f)$ in the compact-open topology has a basis consisting of sets of the form \[ \bigcap_{(K, U) \in S} \{g \in C(X, Y) \mid g(K) \subseteq U\}, \] where $S$ is a finite collection of pairs $(K, U)$ with $K$ a compact subset of $X$, $U$ an open subset of $Y$, and $f(K) \subseteq U$.

ContinuousMap.mem_nhds_iff theorem

 {f : C(X, Y)} {s : Set C(X, Y)} :
  s ∈ 𝓝 f ↔
    ∃ S : Set (Set X × Set Y),
      S.Finite ∧
        (∀ K U, (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ MapsTo f K U) ∧
          {g : C(X, Y) | ∀ K U, (K, U) ∈ S → MapsTo g K U} ⊆ s

Full source

protected lemma mem_nhds_iff {f : C(X, Y)} {s : Set C(X, Y)} :
    s ∈ 𝓝 fs ∈ 𝓝 f ↔ ∃ S : Set (Set X × Set Y), S.Finite ∧
      (∀ K U, (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ MapsTo f K U) ∧
      {g : C(X, Y) | ∀ K U, (K, U) ∈ S → MapsTo g K U} ⊆ s := by
  simp [f.hasBasis_nhds.mem_iff, ← setOf_forall, and_assoc]

Neighborhood Characterization in Compact-Open Topology

Informal description

For a continuous map $f \in C(X, Y)$ and a subset $s \subseteq C(X, Y)$, the set $s$ is a neighborhood of $f$ in the compact-open topology if and only if there exists a finite collection $S$ of pairs $(K, U)$, where $K$ is a compact subset of $X$ and $U$ is an open subset of $Y$ such that $f(K) \subseteq U$, and the set $\{g \in C(X, Y) \mid \forall (K, U) \in S, g(K) \subseteq U\}$ is contained in $s$.

ContinuousMap.continuous_postcomp theorem

(g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z))

Full source

/-- `C(X, ·)` is a functor. -/
theorem continuous_postcomp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X, Y) → C(X, Z)) :=
  continuous_compactOpen.2 fun _K hK _U hU ↦ isOpen_setOf_mapsTo hK (hU.preimage g.2)

Continuity of Postcomposition in Compact-Open Topology

Informal description

For any continuous map $g : Y \to Z$, the postcomposition map $g_* : C(X, Y) \to C(X, Z)$ defined by $g_*(f) = g \circ f$ is continuous with respect to the compact-open topologies on $C(X, Y)$ and $C(X, Z)$.

ContinuousMap.isInducing_postcomp theorem

(g : C(Y, Z)) (hg : IsInducing g) : IsInducing (g.comp : C(X, Y) → C(X, Z))

Full source

/-- 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. -/
theorem isInducing_postcomp (g : C(Y, Z)) (hg : IsInducing g) :
    IsInducing (g.comp : C(X, Y) → C(X, Z)) where
  eq_induced := by
    simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, hg.setOf_isOpen,
      image2_image_right, MapsTo, mem_preimage, preimage_setOf_eq, comp_apply]

Induced Topology Preservation under Post-Composition in Function Spaces

Informal description

Let $X$, $Y$, and $Z$ be topological spaces. If $g \colon Y \to Z$ is a continuous map that induces the topology on $Z$ (i.e., the topology on $Z$ is the coarsest such that $g$ is continuous), then the composition map $g \circ \_ \colon C(X, Y) \to C(X, Z)$ also induces the topology on $C(X, Z)$ (i.e., the compact-open topology on $C(X, Z)$ is the coarsest such that $g \circ \_$ is continuous).

ContinuousMap.isEmbedding_postcomp theorem

(g : C(Y, Z)) (hg : IsEmbedding g) : IsEmbedding (g.comp : C(X, Y) → C(X, Z))

Full source

/-- 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. -/
theorem isEmbedding_postcomp (g : C(Y, Z)) (hg : IsEmbedding g) :
    IsEmbedding (g.comp : C(X, Y) → C(X, Z)) :=
  ⟨isInducing_postcomp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩

Embedding Property of Postcomposition in Compact-Open Topology

Informal description

Let $X$, $Y$, and $Z$ be topological spaces. If $g \colon Y \to Z$ is a topological embedding (i.e., a continuous injective map that is a homeomorphism onto its image), then the composition map $g \circ \_ \colon C(X, Y) \to C(X, Z)$ is also a topological embedding with respect to the compact-open topologies on $C(X, Y)$ and $C(X, Z)$.

ContinuousMap.continuous_precomp theorem

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

Full source

/-- `C(·, Z)` is a functor. -/
@[continuity, fun_prop]
theorem continuous_precomp (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) :=
  continuous_compactOpen.2 fun K hK U hU ↦ by
    simpa only [mapsTo_image_iff] using isOpen_setOf_mapsTo (hK.image f.2) hU

Continuity of Precomposition in Compact-Open Topology

Informal description

For any continuous map $f \in C(X, Y)$, the precomposition map $g \mapsto g \circ f$ from $C(Y, Z)$ to $C(X, Z)$ is continuous with respect to the compact-open topologies on both function spaces.

ContinuousMap.compRightContinuousMap definition

(f : C(X, Y)) : C(C(Y, Z), C(X, Z))

Full source

/-- Precomposition by a continuous map is itself a continuous map between spaces of continuous maps.
-/
@[simps apply]
def compRightContinuousMap (f : C(X, Y)) :
    C(C(Y, Z), C(X, Z)) where
  toFun g := g.comp f

Continuous precomposition map

Informal description

Given a continuous map $f \in C(X, Y)$, the function that maps each $g \in C(Y, Z)$ to its composition $g \circ f \in C(X, Z)$ is itself a continuous map between the function spaces equipped with the compact-open topology.

Homeomorph.arrowCongr definition

(φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) : C(X, Y) ≃ₜ C(Z, T)

Full source

/-- Any pair of homeomorphisms `X ≃ₜ Z` and `Y ≃ₜ T` gives rise to a homeomorphism
`C(X, Y) ≃ₜ C(Z, T)`. -/
protected def _root_.Homeomorph.arrowCongr (φ : X ≃ₜ Z) (ψ : Y ≃ₜ T) :
    C(X, Y)C(X, Y) ≃ₜ C(Z, T) where
  toFun f := .comp ψ <| f.comp φ.symm
  invFun f := .comp ψ.symm <| f.comp φ
  left_inv f := ext fun _ ↦ ψ.left_inv (f _) |>.trans <| congrArg f <| φ.left_inv _
  right_inv f := ext fun _ ↦ ψ.right_inv (f _) |>.trans <| congrArg f <| φ.right_inv _
  continuous_toFun := continuous_postcomp _ |>.comp <| continuous_precomp _
  continuous_invFun := continuous_postcomp _ |>.comp <| continuous_precomp _

Homeomorphism of function spaces induced by homeomorphisms of domains and codomains

Informal description

Given homeomorphisms $\varphi : X \simeq Z$ and $\psi : Y \simeq T$, there is an induced homeomorphism between the spaces of continuous maps $C(X, Y) \simeq C(Z, T)$. The forward map sends $f \in C(X, Y)$ to $\psi \circ f \circ \varphi^{-1} \in C(Z, T)$, and the inverse map sends $g \in C(Z, T)$ to $\psi^{-1} \circ g \circ \varphi \in C(X, Y)$. Both maps are continuous with respect to the compact-open topology.

ContinuousMap.continuous_comp' theorem

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

Full source

/-- 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*. -/
theorem continuous_comp' : Continuous fun x : C(X, Y)C(X, Y) × C(Y, Z) => x.2.comp x.1 := by
  simp_rw [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen]
  intro ⟨f, g⟩ K hK U hU (hKU : MapsTo (g ∘ f) K U)
  obtain ⟨L, hKL, hLc, hLU⟩ : ∃ L ∈ 𝓝ˢ (f '' K), IsCompact L ∧ MapsTo g L U :=
    exists_mem_nhdsSet_isCompact_mapsTo g.continuous (hK.image f.continuous) hU
      (mapsTo_image_iff.2 hKU)
  rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo'] at hKL
  exact ((eventually_mapsTo hK isOpen_interior hKL).prod_nhds
    (eventually_mapsTo hLc hU hLU)).mono fun ⟨f', g'⟩ ⟨hf', hg'⟩ ↦
      hg'.comp <| hf'.mono_right interior_subset

Continuity of Composition in Compact-Open Topology

Informal description

Let $X$, $Y$, and $Z$ be topological spaces with $Y$ locally compact. The composition map $C(X, Y) \times C(Y, Z) \to C(X, Z)$, defined by $(f, g) \mapsto g \circ f$, is continuous when the function spaces are equipped with the compact-open topology.

Filter.Tendsto.compCM theorem

 {α : Type*} {l : Filter α} {g : α → C(Y, Z)} {g₀ : C(Y, Z)} {f : α → C(X, Y)} {f₀ : C(X, Y)} (hg : Tendsto g l (𝓝 g₀))
  (hf : Tendsto f l (𝓝 f₀)) : Tendsto (fun a ↦ (g a).comp (f a)) l (𝓝 (g₀.comp f₀))

Full source

lemma _root_.Filter.Tendsto.compCM {α : Type*} {l : Filter α} {g : α → C(Y, Z)} {g₀ : C(Y, Z)}
    {f : α → C(X, Y)} {f₀ : C(X, Y)} (hg : Tendsto g l (𝓝 g₀)) (hf : Tendsto f l (𝓝 f₀)) :
    Tendsto (fun a ↦ (g a).comp (f a)) l (𝓝 (g₀.comp f₀)) :=
  (continuous_comp'.tendsto (f₀, g₀)).comp (hf.prodMk_nhds hg)

Limit of Compositions of Continuous Maps in Compact-Open Topology

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $\alpha$ be a type. Given a filter $l$ on $\alpha$, two families of continuous maps $g : \alpha \to C(Y, Z)$ and $f : \alpha \to C(X, Y)$, and their respective limit points $g_0 \in C(Y, Z)$ and $f_0 \in C(X, Y)$, if $g$ tends to $g_0$ along $l$ and $f$ tends to $f_0$ along $l$, then the family of composed maps $(g \circ f)(a) := g(a) \circ f(a)$ tends to $g_0 \circ f_0$ along $l$.

ContinuousAt.compCM theorem

(hg : ContinuousAt g a) (hf : ContinuousAt f a) : ContinuousAt (fun x ↦ (g x).comp (f x)) a

Full source

nonrec lemma _root_.ContinuousAt.compCM (hg : ContinuousAt g a) (hf : ContinuousAt f a) :
    ContinuousAt (fun x ↦ (g x).comp (f x)) a :=
  hg.compCM hf

Continuity of Composition at a Point in Compact-Open Topology

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $g$ and $f$ be functions such that $g$ is continuous at a point $a$ in $Y$ and $f$ is continuous at $a$ in $X$. Then the composition function $x \mapsto g(x) \circ f(x)$ is continuous at $a$.

ContinuousWithinAt.compCM theorem

(hg : ContinuousWithinAt g s a) (hf : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x ↦ (g x).comp (f x)) s a

Full source

nonrec lemma _root_.ContinuousWithinAt.compCM (hg : ContinuousWithinAt g s a)
    (hf : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x ↦ (g x).comp (f x)) s a :=
  hg.compCM hf

Continuity Within a Set of Pointwise Composition in Compact-Open Topology

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $g : X \to C(Y, Z)$ and $f : X \to C(Y, Z)$ be functions. If $g$ is continuous within a set $s$ at a point $a \in X$ and $f$ is continuous within $s$ at $a$, then the function $x \mapsto g(x) \circ f(x)$ is continuous within $s$ at $a$, where $C(Y, Z)$ is equipped with the compact-open topology.

ContinuousOn.compCM theorem

(hg : ContinuousOn g s) (hf : ContinuousOn f s) : ContinuousOn (fun x ↦ (g x).comp (f x)) s

Full source

lemma _root_.ContinuousOn.compCM (hg : ContinuousOn g s) (hf : ContinuousOn f s) :
    ContinuousOn (fun x ↦ (g x).comp (f x)) s := fun a ha ↦
  (hg a ha).compCM (hf a ha)

Continuity of Pointwise Composition on a Subset in Compact-Open Topology

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $g : X \to C(Y, Z)$ and $f : X \to C(Y, Z)$ be functions. If $g$ and $f$ are continuous on a subset $s \subseteq X$, then the function $x \mapsto g(x) \circ f(x)$ is continuous on $s$, where $C(Y, Z)$ is equipped with the compact-open topology.

Continuous.compCM theorem

(hg : Continuous g) (hf : Continuous f) : Continuous fun x => (g x).comp (f x)

Full source

lemma _root_.Continuous.compCM (hg : Continuous g) (hf : Continuous f) :
    Continuous fun x => (g x).comp (f x) :=
  continuous_comp'.comp (hf.prodMk hg)

Continuity of Pointwise Composition in Compact-Open Topology

Informal description

Let $X$, $Y$, and $Z$ be topological spaces, and let $f : X \to C(Y, Z)$ and $g : X \to C(Y, Z)$ be continuous functions. Then the function $x \mapsto g(x) \circ f(x)$ is continuous from $X$ to $C(Y, Z)$, where $C(Y, Z)$ is equipped with the compact-open topology.

ContinuousMap.instContinuousEvalOfLocallyCompactPair instance

[LocallyCompactPair X Y] : ContinuousEval C(X, Y) X Y

Full source

/-- The evaluation map `C(X, Y) × X → Y` is continuous
if `X, Y` is a locally compact pair of spaces. -/
instance [LocallyCompactPair X Y] : ContinuousEval C(X, Y) X Y where
  continuous_eval := by
    simp_rw [continuous_iff_continuousAt, ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]
    rintro ⟨f, x⟩ U ⟨hx : f x ∈ U, hU : IsOpen U⟩
    rcases exists_mem_nhds_isCompact_mapsTo f.continuous (hU.mem_nhds hx) with ⟨K, hxK, hK, hKU⟩
    filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2

Continuity of Evaluation Map for Locally Compact Pairs

Informal description

For topological spaces $X$ and $Y$ forming a locally compact pair, the evaluation map $C(X, Y) \times X \to Y$ defined by $(f, x) \mapsto f(x)$ is continuous when $C(X, Y)$ is equipped with the compact-open topology.

ContinuousMap.instContinuousEvalConst instance

: ContinuousEvalConst C(X, Y) X Y

Full source

instance : ContinuousEvalConst C(X, Y) X Y where
  continuous_eval_const x :=
    continuous_def.2 fun U hU ↦ by simpa using isOpen_setOf_mapsTo isCompact_singleton hU

Continuous Evaluation at Points for Continuous Function Spaces

Informal description

The space of continuous maps $C(X, Y)$ is equipped with a canonical structure of continuous evaluation at any point, meaning that for any fixed $x \in X$, the evaluation map $C(X, Y) \to Y$ given by $f \mapsto f(x)$ is continuous.

ContinuousMap.isClosed_setOf_mapsTo theorem

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

Full source

lemma isClosed_setOf_mapsTo {t : Set Y} (ht : IsClosed t) (s : Set X) :
    IsClosed {f : C(X, Y) | MapsTo f s t} :=
  ht.setOf_mapsTo fun _ _ ↦ continuous_eval_const _

Closedness of Continuous Maps Preserving Subset Inclusion in Compact-Open Topology

Informal description

For any closed subset $t$ of $Y$ and any subset $s$ of $X$, the set of continuous maps $f \in C(X, Y)$ such that $f$ maps $s$ into $t$ is closed in the compact-open topology on $C(X, Y)$.

ContinuousMap.isClopen_setOf_mapsTo theorem

(hK : IsCompact K) (hU : IsClopen U) : IsClopen {f : C(X, Y) | MapsTo f K U}

Full source

lemma isClopen_setOf_mapsTo (hK : IsCompact K) (hU : IsClopen U) :
    IsClopen {f : C(X, Y) | MapsTo f K U} :=
  ⟨isClosed_setOf_mapsTo hU.isClosed K, isOpen_setOf_mapsTo hK hU.isOpen⟩

Clopenness of Maps-to Sets for Clopen Targets in Compact-Open Topology

Informal description

Let $X$ and $Y$ be topological spaces, $K$ a compact subset of $X$, and $U$ a clopen (both closed and open) subset of $Y$. Then the set $\{f \in C(X, Y) \mid f(K) \subseteq U\}$ is clopen in the compact-open topology on $C(X, Y)$.

ContinuousMap.specializes_coe theorem

{f g : C(X, Y)} : ⇑f ⤳ ⇑g ↔ f ⤳ g

Full source

@[norm_cast]
lemma specializes_coe {f g : C(X, Y)} : ⇑f ⤳ ⇑g⇑f ⤳ ⇑g ↔ f ⤳ g := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coeFun⟩
  suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
    simpa [specializes_iff_pure, nhds_compactOpen]
  exact fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)

Specialization in Compact-Open Topology is Equivalent to Pointwise Specialization

Informal description

For any two continuous maps $f, g \in C(X, Y)$, the function $f$ specializes to $g$ pointwise (i.e., $f(x) \rightsquigarrow g(x)$ for all $x \in X$) if and only if $f$ specializes to $g$ in the compact-open topology on $C(X, Y)$.

ContinuousMap.inseparable_coe theorem

{f g : C(X, Y)} : Inseparable (f : X → Y) g ↔ Inseparable f g

Full source

@[norm_cast]
lemma inseparable_coe {f g : C(X, Y)} : InseparableInseparable (f : X → Y) g ↔ Inseparable f g := by
  simp only [inseparable_iff_specializes_and, specializes_coe]

Inseparability of Continuous Maps in Compact-Open Topology vs. Pointwise Inseparability

Informal description

For any two continuous maps $f, g \in C(X, Y)$, the functions $f$ and $g$ are inseparable (in the function space $X \to Y$) if and only if the continuous maps $f$ and $g$ are inseparable in the compact-open topology on $C(X, Y)$.

ContinuousMap.instT0Space instance

[T0Space Y] : T0Space C(X, Y)

Full source

instance [T0Space Y] : T0Space C(X, Y) :=
  t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun

T₀ Property of Continuous Function Spaces with Compact-Open Topology

Informal description

For any topological spaces $X$ and $Y$, if $Y$ is a T₀ space, then the space of continuous maps $C(X, Y)$ equipped with the compact-open topology is also a T₀ space.

ContinuousMap.instR0Space instance

[R0Space Y] : R0Space C(X, Y)

Full source

instance [R0Space Y] : R0Space C(X, Y) where
  specializes_symmetric f g h := by
    rw [← specializes_coe] at h ⊢
    exact h.symm

Compact-Open Topology Preserves R₀ Property

Informal description

For any topological spaces $X$ and $Y$, if $Y$ is an R₀ space, then the space of continuous maps $C(X, Y)$ equipped with the compact-open topology is also an R₀ space.

ContinuousMap.instT1Space instance

[T1Space Y] : T1Space C(X, Y)

Full source

instance [T1Space Y] : T1Space C(X, Y) :=
  t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun

Compact-Open Topology Preserves T₁ Property

Informal description

For any topological spaces $X$ and $Y$, if $Y$ is a T₁ space, then the space of continuous maps $C(X, Y)$ equipped with the compact-open topology is also a T₁ space.

ContinuousMap.instR1Space instance

[R1Space Y] : R1Space C(X, Y)

Full source

instance [R1Space Y] : R1Space C(X, Y) :=
  .of_continuous_specializes_imp continuous_coeFun fun _ _ ↦ specializes_coe.1

Compact-Open Topology Preserves Preregularity

Informal description

For any topological spaces $X$ and $Y$, if $Y$ is an R₁ (preregular) space, then the space of continuous maps $C(X, Y)$ equipped with the compact-open topology is also an R₁ space.

ContinuousMap.instT2Space instance

[T2Space Y] : T2Space C(X, Y)

Full source

instance [T2Space Y] : T2Space C(X, Y) := inferInstance

Compact-Open Topology Preserves Hausdorff Property

Informal description

For any topological spaces $X$ and $Y$, if $Y$ is a Hausdorff (T₂) space, then the space of continuous maps $C(X, Y)$ equipped with the compact-open topology is also a Hausdorff space.

ContinuousMap.instRegularSpace instance

[RegularSpace Y] : RegularSpace C(X, Y)

Full source

instance [RegularSpace Y] : RegularSpace C(X, Y) :=
  .of_lift'_closure_le fun f ↦ by
    rw [← tendsto_id', tendsto_nhds_compactOpen]
    intro K hK U hU hf
    rcases (hK.image f.continuous).exists_isOpen_closure_subset (hU.mem_nhdsSet.2 hf.image_subset)
      with ⟨V, hVo, hKV, hVU⟩
    filter_upwards [mem_lift' (eventually_mapsTo hK hVo (mapsTo'.2 hKV))] with g hg
    refine ((isClosed_setOf_mapsTo isClosed_closure K).closure_subset ?_).mono_right hVU
    exact closure_mono (fun _ h ↦ h.mono_right subset_closure) hg

Regularity of Continuous Function Space in Compact-Open Topology

Informal description

For any topological spaces $X$ and $Y$, if $Y$ is a regular space, then the space of continuous maps $C(X, Y)$ equipped with the compact-open topology is also a regular space.

ContinuousMap.instT3Space instance

[T3Space Y] : T3Space C(X, Y)

Full source

instance [T3Space Y] : T3Space C(X, Y) := inferInstance

T₃ Property of Continuous Function Spaces with Compact-Open Topology

Informal description

For any topological spaces $X$ and $Y$, if $Y$ is a T₃ space, then the space of continuous maps $C(X, Y)$ equipped with the compact-open topology is also a T₃ space.

ContinuousMap.continuous_restrict theorem

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

Full source

/-- 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. -/
theorem continuous_restrict (s : Set X) : Continuous fun F : C(X, Y) => F.restrict s :=
  continuous_precomp <| restrict s <| .id X

Continuity of Function Restriction in Compact-Open Topology

Informal description

For any subset $s$ of a topological space $X$, the restriction map $F \mapsto F|_s$ from the space of continuous functions $C(X, Y)$ to $C(s, Y)$ is continuous, where both function spaces are equipped with the compact-open topology.

ContinuousMap.compactOpen_le_induced theorem

 (s : Set X) : (ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) ≤ .induced (restrict s) ContinuousMap.compactOpen

Full source

theorem compactOpen_le_induced (s : Set X) :
    (ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) ≤
      .induced (restrict s) ContinuousMap.compactOpen :=
  (continuous_restrict s).le_induced

Compact-Open Topology is Finer than Induced Topology via Restriction

Informal description

For any subset $s$ of a topological space $X$, the compact-open topology on the space of continuous maps $C(X, Y)$ is finer than the topology induced by the restriction map $F \mapsto F|_s$ from $C(X, Y)$ to $C(s, Y)$, where both spaces are equipped with the compact-open topology. In other words, the compact-open topology on $C(X, Y)$ is at least as fine as the topology obtained by pulling back the compact-open topology on $C(s, Y)$ via the restriction map.

ContinuousMap.compactOpen_eq_iInf_induced theorem

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

Full source

/-- 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 for every compact set `K`,
the universal set `Set.univ : Set K` is a compact set as well. -/
theorem compactOpen_eq_iInf_induced :
    (ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) =
      ⨅ (K : Set X) (_ : IsCompact K), .induced (.restrict K) ContinuousMap.compactOpen := by
  refine le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_
  refine le_generateFrom <| forall_mem_image2.2 fun K (hK : IsCompact K) U hU ↦ ?_
  refine TopologicalSpace.le_def.1 (iInf₂_le K hK) _ ?_
  convert isOpen_induced (isOpen_setOf_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)
  simp [mapsTo_univ_iff, Subtype.forall, MapsTo]

Compact-Open Topology as Infimum of Induced Topologies via Restrictions to Compact Subsets

Informal description

The compact-open topology on the space of continuous maps $C(X, Y)$ coincides with the infimum of the topologies induced by the restriction maps $F \mapsto F|_K$ for all compact subsets $K \subseteq X$, where each $C(K, Y)$ is equipped with the compact-open topology.

ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced theorem

(f : C(X, Y)) : 𝓝 f = ⨅ (s) (_ : IsCompact s), (𝓝 (f.restrict s)).comap (ContinuousMap.restrict s)

Full source

theorem nhds_compactOpen_eq_iInf_nhds_induced (f : C(X, Y)) :
    𝓝 f = ⨅ (s) (_ : IsCompact s), (𝓝 (f.restrict s)).comap (ContinuousMap.restrict s) := by
  rw [compactOpen_eq_iInf_induced]
  simp only [nhds_iInf, nhds_induced]

Neighborhood Filter Characterization in Compact-Open Topology via Restrictions to Compact Subsets

Informal description

For any continuous map $f \in C(X, Y)$, the neighborhood filter of $f$ in the compact-open topology on $C(X, Y)$ is equal to the infimum over all compact subsets $s \subseteq X$ of the preimage under the restriction map of the neighborhood filter of $f|_s$ in the compact-open topology on $C(s, Y)$. In symbols: \[ \mathcal{N}_{\text{compact-open}}(f) = \bigsqcap_{\substack{s \subseteq X \\ \text{compact}}} (\text{restrict}_s)^{-1}(\mathcal{N}_{\text{compact-open}}(f|_s)) \]

ContinuousMap.tendsto_compactOpen_restrict theorem

 {ι : Type*} {l : Filter ι} {F : ι → C(X, Y)} {f : C(X, Y)} (hFf : Filter.Tendsto F l (𝓝 f)) (s : Set X) :
  Tendsto (fun i => (F i).restrict s) l (𝓝 (f.restrict s))

Full source

theorem tendsto_compactOpen_restrict {ι : Type*} {l : Filter ι} {F : ι → C(X, Y)} {f : C(X, Y)}
    (hFf : Filter.Tendsto F l (𝓝 f)) (s : Set X) :
    Tendsto (fun i => (F i).restrict s) l (𝓝 (f.restrict s)) :=
  (continuous_restrict s).continuousAt.tendsto.comp hFf

Continuity of Restriction in Compact-Open Topology

Informal description

Let $X$ and $Y$ be topological spaces, $\iota$ a type, and $l$ a filter on $\iota$. Given a family of continuous maps $F \colon \iota \to C(X, Y)$ and a continuous map $f \in C(X, Y)$ such that $F$ tends to $f$ in the compact-open topology, then for any subset $s \subseteq X$, the restricted family $(F_i|_s)_{i \in \iota}$ tends to $f|_s$ in the compact-open topology on $C(s, Y)$.

ContinuousMap.tendsto_compactOpen_iff_forall theorem

 {ι : Type*} {l : Filter ι} (F : ι → C(X, Y)) (f : C(X, Y)) :
  Tendsto F l (𝓝 f) ↔ ∀ K, IsCompact K → Tendsto (fun i => (F i).restrict K) l (𝓝 (f.restrict K))

Full source

theorem tendsto_compactOpen_iff_forall {ι : Type*} {l : Filter ι} (F : ι → C(X, Y)) (f : C(X, Y)) :
    TendstoTendsto F l (𝓝 f) ↔
      ∀ K, IsCompact K → Tendsto (fun i => (F i).restrict K) l (𝓝 (f.restrict K)) := by
  rw [compactOpen_eq_iInf_induced]
  simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp_def]

Characterization of Convergence in Compact-Open Topology via Restrictions to Compact Subsets

Informal description

Let $X$ and $Y$ be topological spaces, $\iota$ a type, and $l$ a filter on $\iota$. For a family of continuous maps $F \colon \iota \to C(X, Y)$ and a continuous map $f \in C(X, Y)$, the following are equivalent: 1. $F$ converges to $f$ in the compact-open topology on $C(X, Y)$. 2. For every compact subset $K \subseteq X$, the restricted family $(F_i|_K)_{i \in \iota}$ converges to $f|_K$ in the compact-open topology on $C(K, Y)$.

ContinuousMap.exists_tendsto_compactOpen_iff_forall theorem

 [WeaklyLocallyCompactSpace X] [T2Space Y] {ι : Type*} {l : Filter ι} [Filter.NeBot l] (F : ι → C(X, Y)) :
  (∃ f, Filter.Tendsto F l (𝓝 f)) ↔ ∀ s : Set X, IsCompact s → ∃ f, Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 f)

Full source

/-- 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`. -/
theorem exists_tendsto_compactOpen_iff_forall [WeaklyLocallyCompactSpace X] [T2Space Y]
    {ι : Type*} {l : Filter ι} [Filter.NeBot l] (F : ι → C(X, Y)) :
    (∃ f, Filter.Tendsto F l (𝓝 f)) ↔
      ∀ s : Set X, IsCompact s → ∃ f, Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 f) := by
  constructor
  · rintro ⟨f, hf⟩ s _
    exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
  · intro h
    choose f hf using h
    -- By uniqueness of limits in a `T2Space`, since `fun i ↦ F i x` tends to both `f s₁ hs₁ x` and
    -- `f s₂ hs₂ x`, we have `f s₁ hs₁ x = f s₂ hs₂ x`
    have h :
      ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
        f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ := by
      rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
      haveI := isCompact_iff_compactSpace.mp hs₁
      haveI := isCompact_iff_compactSpace.mp hs₂
      have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
      have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
      exact tendsto_nhds_unique h₁ h₂
    -- So glue the `f s hs` together and prove that this glued function `f₀` is a limit on each
    -- compact set `s`
    refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩
    rw [tendsto_compactOpen_iff_forall]
    intro s hs
    rw [liftCover_restrict']
    exact hf s hs

Existence of Limit in Compact-Open Topology via Compact Restrictions

Informal description

Let $X$ be a weakly locally compact space and $Y$ a Hausdorff space. For any type $\iota$, a non-trivial filter $l$ on $\iota$, and a family of continuous maps $F \colon \iota \to C(X, Y)$, the following are equivalent: 1. There exists a continuous map $f \in C(X, Y)$ such that $F$ converges to $f$ in the compact-open topology. 2. For every compact subset $s \subseteq X$, there exists a continuous map $f_s \in C(s, Y)$ such that the restricted family $(F_i|_s)_{i \in \iota}$ converges to $f_s$ in the compact-open topology on $C(s, Y)$.

ContinuousMap.coev definition

(b : Y) : C(X, Y × X)

Full source

/-- The coevaluation map `Y → C(X, Y × X)` sending a point `x : Y` to the continuous function
on `X` sending `y` to `(x, y)`. -/
@[simps -fullyApplied]
def coev (b : Y) : C(X, Y × X) :=
  { toFun := Prod.mk b }

Coevaluation map $ Y \to C(X, Y \times X) $

Informal description

The coevaluation map $ \text{coev} \colon Y \to C(X, Y \times X) $ sends a point $ y \in Y $ to the continuous function $ X \to Y \times X $ defined by $ x \mapsto (y, x) $.

ContinuousMap.image_coev theorem

{y : Y} (s : Set X) : coev X Y y '' s = { y } ×ˢ s

Full source

theorem image_coev {y : Y} (s : Set X) : coevcoev X Y y '' s = {y} ×ˢ s := by simp [singleton_prod]

Image of Coevaluation Map Equals Cartesian Product with Singleton

Informal description

For any point $y \in Y$ and any subset $s \subseteq X$, the image of $s$ under the coevaluation map $\text{coev}(y) \colon X \to Y \times X$ is equal to the Cartesian product $\{y\} \times s$.

ContinuousMap.continuous_coev theorem

: Continuous (coev X Y)

Full source

/-- The coevaluation map `Y → C(X, Y × X)` is continuous (always). -/
theorem continuous_coev : Continuous (coev X Y) := by
  have : ∀ {a K U}, MapsToMapsTo (coev X Y a) K U ↔ {a} ×ˢ K ⊆ U := by simp [singleton_prod, mapsTo']
  simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen, this]
  intro x K hK U hU hKU
  rcases generalized_tube_lemma isCompact_singleton hK hU hKU with ⟨V, W, hV, -, hxV, hKW, hVWU⟩
  filter_upwards [hV.mem_nhds (hxV rfl)] with a ha
  exact (prod_mono (singleton_subset_iff.mpr ha) hKW).trans hVWU

Continuity of the Coevaluation Map in Compact-Open Topology

Informal description

The coevaluation map $\text{coev} \colon Y \to C(X, Y \times X)$, defined by $y \mapsto (x \mapsto (y, x))$, is continuous when $C(X, Y \times X)$ is equipped with the compact-open topology.

ContinuousMap.curry definition

(f : C(X × Y, Z)) : C(X, C(Y, Z))

Full source

/-- 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`. -/
def curry (f : C(X × Y, Z)) : C(X, C(Y, Z)) where
  toFun a := ⟨Function.curry f a, f.continuous.comp <| by fun_prop⟩
  continuous_toFun := (continuous_postcomp f).comp continuous_coev

Currying of continuous maps

Informal description

The currying operation takes a continuous map $f \colon X \times Y \to Z$ and returns a continuous map $X \to C(Y, Z)$, where $C(Y, Z)$ is equipped with the compact-open topology. For each $a \in X$, the resulting map sends $a$ to the continuous function $f(a, \cdot) \colon Y \to Z$.

ContinuousMap.curry_apply theorem

(f : C(X × Y, Z)) (a : X) (b : Y) : f.curry a b = f (a, b)

Full source

@[simp]
theorem curry_apply (f : C(X × Y, Z)) (a : X) (b : Y) : f.curry a b = f (a, b) :=
  rfl

Evaluation of Curried Continuous Function: $\text{curry}(f)(a)(b) = f(a, b)$

Informal description

For any continuous map $f \colon X \times Y \to Z$, the curried function $\text{curry}(f) \colon X \to C(Y, Z)$ satisfies $\text{curry}(f)(a)(b) = f(a, b)$ for all $a \in X$ and $b \in Y$.

ContinuousMap.continuous_of_continuous_uncurry theorem

(f : X → C(Y, Z)) (h : Continuous (Function.uncurry fun x y => f x y)) : Continuous f

Full source

/-- To show continuity of a map `α → C(β, γ)`, it suffices to show that its uncurried form
    `α × β → γ` is continuous. -/
theorem continuous_of_continuous_uncurry (f : X → C(Y, Z))
    (h : Continuous (Function.uncurry fun x y => f x y)) : Continuous f :=
  (curry ⟨_, h⟩).2

Continuity via Uncurrying: $f$ is continuous if its uncurried form is continuous

Informal description

Let $X$, $Y$, and $Z$ be topological spaces. Given a map $f \colon X \to C(Y, Z)$, if the uncurried map $\tilde{f} \colon X \times Y \to Z$ defined by $\tilde{f}(x,y) = f(x)(y)$ is continuous, then $f$ is continuous when $C(Y, Z)$ is equipped with the compact-open topology.

ContinuousMap.continuous_curry theorem

[LocallyCompactSpace (X × Y)] : Continuous (curry : C(X × Y, Z) → C(X, C(Y, Z)))

Full source

/-- The currying process is a continuous map between function spaces. -/
theorem continuous_curry [LocallyCompactSpace (X × Y)] :
    Continuous (curry : C(X × Y, Z) → C(X, C(Y, Z))) := by
  apply continuous_of_continuous_uncurry
  apply continuous_of_continuous_uncurry
  rw [← (Homeomorph.prodAssoc _ _ _).symm.comp_continuous_iff']
  exact continuous_eval

Continuity of Currying for Locally Compact Product Spaces

Informal description

If the product space $X \times Y$ is locally compact, then the currying map $\text{curry} \colon C(X \times Y, Z) \to C(X, C(Y, Z))$ is continuous, where both function spaces are equipped with the compact-open topology.

ContinuousMap.continuous_uncurry_of_continuous theorem

[LocallyCompactSpace Y] (f : C(X, C(Y, Z))) : Continuous (Function.uncurry fun x y => f x y)

Full source

/-- The uncurried form of a continuous map `X → C(Y, Z)` is a continuous map `X × Y → Z`. -/
theorem continuous_uncurry_of_continuous [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) :
    Continuous (Function.uncurry fun x y => f x y) :=
  continuous_eval.comp <| f.continuous.prodMap continuous_id

Continuity of Uncurried Map for Locally Compact $Y$

Informal description

Let $X$, $Y$, and $Z$ be topological spaces with $Y$ locally compact. For any continuous map $f \colon X \to C(Y, Z)$ (where $C(Y, Z)$ is equipped with the compact-open topology), the uncurried map $\tilde{f} \colon X \times Y \to Z$ defined by $\tilde{f}(x,y) = f(x)(y)$ is continuous.

ContinuousMap.uncurry definition

[LocallyCompactSpace Y] (f : C(X, C(Y, Z))) : C(X × Y, Z)

Full source

/-- 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`. -/
@[simps]
def uncurry [LocallyCompactSpace Y] (f : C(X, C(Y, Z))) : C(X × Y, Z) :=
  ⟨_, continuous_uncurry_of_continuous f⟩

Uncurrying of continuous maps for locally compact spaces

Informal description

Given topological spaces $X$, $Y$, and $Z$ with $Y$ locally compact, the uncurrying operation transforms a continuous map $f \colon X \to C(Y, Z)$ (where $C(Y, Z)$ has the compact-open topology) into a continuous map $\tilde{f} \colon X \times Y \to Z$ defined by $\tilde{f}(x,y) = f(x)(y)$. This operation is continuous when $X$ is also locally compact.

ContinuousMap.continuous_uncurry theorem

[LocallyCompactSpace X] [LocallyCompactSpace Y] : Continuous (uncurry : C(X, C(Y, Z)) → C(X × Y, Z))

Full source

/-- The uncurrying process is a continuous map between function spaces. -/
theorem continuous_uncurry [LocallyCompactSpace X] [LocallyCompactSpace Y] :
    Continuous (uncurry : C(X, C(Y, Z)) → C(X × Y, Z)) := by
  apply continuous_of_continuous_uncurry
  rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
  dsimp [Function.comp_def]
  exact (continuous_fst.fst.eval continuous_fst.snd).eval continuous_snd

Continuity of Uncurrying for Locally Compact Spaces

Informal description

Let $X$, $Y$, and $Z$ be topological spaces where both $X$ and $Y$ are locally compact. Then the uncurrying map $C(X, C(Y, Z)) \to C(X \times Y, Z)$, which sends a continuous map $f$ to its uncurried form $\tilde{f}(x,y) = f(x)(y)$, is continuous when both function spaces are equipped with their compact-open topologies.

ContinuousMap.const' definition

: C(Y, C(X, Y))

Full source

/-- The family of constant maps: `Y → C(X, Y)` as a continuous map. -/
def const' : C(Y, C(X, Y)) :=
  curry ContinuousMap.fst

Constant map function

Informal description

The constant map function that sends each element $y \in Y$ to the constant map in $C(X, Y)$ that takes every $x \in X$ to $y$. This is represented as a continuous map from $Y$ to $C(X, Y)$, where $C(X, Y)$ is equipped with the compact-open topology.

ContinuousMap.coe_const' theorem

: (const' : Y → C(X, Y)) = const X

Full source

@[simp]
theorem coe_const' : (const' : Y → C(X, Y)) = const X :=
  rfl

Equality of Constant Map Functions: `const' = const X`

Informal description

The function `const' : Y → C(X, Y)` is equal to the constant map function `const X : Y → C(X, Y)`, where `const X y` is the constant map in `C(X, Y)` that sends every `x ∈ X` to `y ∈ Y`.

ContinuousMap.continuous_const' theorem

: Continuous (const X : Y → C(X, Y))

Full source

theorem continuous_const' : Continuous (const X : Y → C(X, Y)) :=
  const'.continuous

Continuity of the Constant Map Function into Compact-Open Topology

Informal description

The constant map function $\text{const}_X : Y \to C(X, Y)$, which sends each $y \in Y$ to the constant map in $C(X, Y)$ with value $y$, is continuous when $C(X, Y)$ is equipped with the compact-open topology.

Homeomorph.curry definition

[LocallyCompactSpace X] [LocallyCompactSpace Y] : C(X × Y, Z) ≃ₜ C(X, C(Y, Z))

Full source

/-- Currying as a homeomorphism between the function spaces `C(X × Y, Z)` and `C(X, C(Y, Z))`. -/
def curry [LocallyCompactSpace X] [LocallyCompactSpace Y] : C(X × Y, Z)C(X × Y, Z) ≃ₜ C(X, C(Y, Z)) :=
  ⟨⟨ContinuousMap.curry, uncurry, by intro; ext; rfl, by intro; ext; rfl⟩,
    continuous_curry, continuous_uncurry⟩

Currying homeomorphism for continuous maps on locally compact spaces

Informal description

Given locally compact topological spaces $X$ and $Y$, and any topological space $Z$, there exists a homeomorphism between the spaces of continuous maps $C(X \times Y, Z)$ and $C(X, C(Y, Z))$. This homeomorphism is given by the currying operation $f \mapsto (x \mapsto (y \mapsto f(x,y)))$ and its inverse uncurrying operation.

Homeomorph.continuousMapOfUnique definition

[Unique X] : Y ≃ₜ C(X, Y)

Full source

/-- If `X` has a single element, then `Y` is homeomorphic to `C(X, Y)`. -/
def continuousMapOfUnique [Unique X] : Y ≃ₜ C(X, Y) where
  toFun := const X
  invFun f := f default
  left_inv _ := rfl
  right_inv f := by
    ext x
    rw [Unique.eq_default x]
    rfl
  continuous_toFun := continuous_const'
  continuous_invFun := continuous_eval_const _

Homeomorphism between $Y$ and $C(X, Y)$ when $X$ is a singleton

Informal description

When the topological space $X$ has a unique element, there is a homeomorphism between $Y$ and the space of continuous maps $C(X, Y)$. The homeomorphism maps each $y \in Y$ to the constant function in $C(X, Y)$ with value $y$, and its inverse maps each $f \in C(X, Y)$ to $f(\text{default})$, where $\text{default}$ is the unique element of $X$.

Homeomorph.continuousMapOfUnique_apply theorem

[Unique X] (y : Y) (x : X) : continuousMapOfUnique y x = y

Full source

@[simp]
theorem continuousMapOfUnique_apply [Unique X] (y : Y) (x : X) : continuousMapOfUnique y x = y :=
  rfl

Evaluation of Homeomorphism between $Y$ and $C(X, Y)$ at Unique Point

Informal description

For a topological space $X$ with a unique element and any topological space $Y$, the homeomorphism $\text{continuousMapOfUnique}$ from $Y$ to $C(X, Y)$ satisfies $\text{continuousMapOfUnique}(y)(x) = y$ for all $y \in Y$ and $x \in X$.

Homeomorph.continuousMapOfUnique_symm_apply theorem

[Unique X] (f : C(X, Y)) : continuousMapOfUnique.symm f = f default

Full source

@[simp]
theorem continuousMapOfUnique_symm_apply [Unique X] (f : C(X, Y)) :
    continuousMapOfUnique.symm f = f default :=
  rfl

Inverse of Homeomorphism between $Y$ and $C(X, Y)$ Evaluates at Default Point

Informal description

For a topological space $X$ with a unique element and any topological space $Y$, the inverse of the homeomorphism $Y \cong C(X, Y)$ maps a continuous function $f \in C(X, Y)$ to its evaluation at the unique element of $X$, i.e., $f(\text{default})$.

Topology.IsQuotientMap.continuous_lift_prod_left theorem

(hf : IsQuotientMap f) {g : X × Y → Z} (hg : Continuous fun p : X₀ × Y => g (f p.1, p.2)) : Continuous g

Full source

theorem Topology.IsQuotientMap.continuous_lift_prod_left (hf : IsQuotientMap f) {g : X × Y → Z}
    (hg : Continuous fun p : X₀ × Y => g (f p.1, p.2)) : Continuous g := by
  let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩
  have h : ∀ x : X, Continuous fun y => g (x, y) := by
    intro x
    obtain ⟨x₀, rfl⟩ := hf.surjective x
    exact (Gf x₀).continuous
  let G : X → C(Y, Z) := fun x => ⟨_, h x⟩
  have : Continuous G := by
    rw [hf.continuous_iff]
    exact Gf.continuous
  exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩

Continuity of Lifted Product Map via Left Quotient Map

Informal description

Let $f \colon X_0 \to X$ be a quotient map between topological spaces. For any continuous map $g \colon X \times Y \to Z$, if the composition $(p \in X_0 \times Y) \mapsto g(f(p_1), p_2)$ is continuous, then $g$ itself is continuous.

Topology.IsQuotientMap.continuous_lift_prod_right theorem

(hf : IsQuotientMap f) {g : Y × X → Z} (hg : Continuous fun p : Y × X₀ => g (p.1, f p.2)) : Continuous g

Full source

theorem Topology.IsQuotientMap.continuous_lift_prod_right (hf : IsQuotientMap f) {g : Y × X → Z}
    (hg : Continuous fun p : Y × X₀ => g (p.1, f p.2)) : Continuous g := by
  have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) :=
    hg.comp continuous_swap
  have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this
  exact (hf.continuous_lift_prod_left this).comp continuous_swap

Continuity of Lifted Product Map via Right Quotient Map

Informal description

Let $f \colon X_0 \to X$ be a quotient map between topological spaces. For any continuous map $g \colon Y \times X \to Z$, if the composition $(p \in Y \times X_0) \mapsto g(p_1, f(p_2))$ is continuous, then $g$ itself is continuous.

Mathlib.Topology.CompactOpen

Main definitions

Tags