The topological space of X-continuous maps

Let X i be a family of topological spaces. Let Z and T be topological spaces. In this file, we endow the type ContinuousMapGeneratedBy X Z T of X-continuous maps Z → T with the coarsest topology which makes the precomposition maps ContinuousMapGeneratedBy X Z T → C(X i, T) continuous for any continuous map X i → Z, where C(X i, T) is endowed with the compact-open topology.

If we assume that the spaces X i are locally compact and that the products X i × X j are X-generated, we obtain that the curryfication of maps induces a bijection between the type of X-continuous maps Y × Z → T and the type of X-continuous maps Z → ContinuousMapGeneratedBy X Y T for all topological spaces Y, Z and T.

References

• Martín Escardó, Jimmie Lawson and Alex Simpson, Comparing Cartesian closed categories of (core) compactly generated spaces

def Topology.ContinuousMapGeneratedBy.precomp {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] {i : ι} (f : C(X i, Z)) : ContinuousMapGeneratedBy X Z T → C(X i, T)

Given a continuous map f : X i → Z, this is the map ContinuousMapGeneratedBy X Z T → C(X i, T) given by the precomposition with f. This is used in order to define a topology on ContinuousMapGeneratedBy X Z T.

Equations

• Topology.ContinuousMapGeneratedBy.precomp f g = { toFun := g.toFun ∘ ⇑f, continuous_toFun := ⋯ }

@[simp]

theorem Topology.ContinuousMapGeneratedBy.precomp_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] {i : ι} (f : C(X i, Z)) (g : ContinuousMapGeneratedBy X Z T) : ⇑(precomp f g) = ⇑g ∘ ⇑f

@[implicit_reducible]

instance Topology.ContinuousMapGeneratedBy.instTopologicalSpace {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] : TopologicalSpace (ContinuousMapGeneratedBy X Z T)

Equations

• Topology.ContinuousMapGeneratedBy.instTopologicalSpace = ⨅ (i : ι), ⨅ (f : C(X i, Z)), TopologicalSpace.induced (Topology.ContinuousMapGeneratedBy.precomp f) inferInstance

theorem Topology.ContinuousMapGeneratedBy.continuous_iff {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] {A : Type u_1} [TopologicalSpace A] {φ : A → ContinuousMapGeneratedBy X Z T} : Continuous φ ↔ ∀ (i : ι) (f : C(X i, Z)), Continuous (precomp f ∘ φ)

theorem Topology.ContinuousMapGeneratedBy.continuous_precomp {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] {i : ι} (f : C(X i, Z)) : Continuous (precomp f)

theorem Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_iff_uncurry {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] [∀ (i : ι), LocallyCompactSpace (X i)] (g : Z → ContinuousMapGeneratedBy X Y T) : ContinuousGeneratedBy X g ↔ ∀ ⦃i₁ : ι⦄ (f₁ : C(X i₁, Z)) ⦃i₂ : ι⦄ (f₂ : C(X i₂, Y)), Continuous fun (x : X i₁ × X i₂) => match x with | (x₁, x₂) => (g (f₁ x₁)) (f₂ x₂)

theorem Topology.ContinuousMapGeneratedBy.continuousGeneratedBy_dom_prod_iff {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] [∀ (i j : ι), IsGeneratedBy X (X i × X j)] (g : Y × Z → T) : ContinuousGeneratedBy X g ↔ ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)), Continuous fun (x : X i₁ × X i₂) => match x with | (x₁, x₂) => g (f₂ x₂, f₁ x₁)

def Topology.ContinuousMapGeneratedBy.curryEquiv {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] [∀ (i : ι), LocallyCompactSpace (X i)] [∀ (i j : ι), IsGeneratedBy X (X i × X j)] : ContinuousMapGeneratedBy X (Y × Z) T ≃ ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)

The bijection between the type of X-continuous maps Y × Z → T and the type of X-continuous maps Z → ContinuousMapGeneratedBy X Y T.

Equations

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

@[simp]

theorem Topology.ContinuousMapGeneratedBy.curryEquiv_apply_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] [∀ (i : ι), LocallyCompactSpace (X i)] [∀ (i j : ι), IsGeneratedBy X (X i × X j)] (g : ContinuousMapGeneratedBy X (Y × Z) T) (y : Y) (z : Z) : ((curryEquiv g) z) y = g (y, z)

@[simp]

theorem Topology.ContinuousMapGeneratedBy.curryEquiv_symm_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] [∀ (i : ι), LocallyCompactSpace (X i)] [∀ (i j : ι), IsGeneratedBy X (X i × X j)] (g : ContinuousMapGeneratedBy X Z (ContinuousMapGeneratedBy X Y T)) (y : Y) (z : Z) : (curryEquiv.symm g) (y, z) = (g z) y

def Topology.ContinuousMapGeneratedBy.ev {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] [∀ (i : ι), LocallyCompactSpace (X i)] [∀ (i j : ι), IsGeneratedBy X (X i × X j)] : ContinuousMapGeneratedBy X (Y × ContinuousMapGeneratedBy X Y Z) Z

The evaluation Y × ContinuousMapGeneratedBy X Y Z → Z as a X-continuous map.

Equations

• Topology.ContinuousMapGeneratedBy.ev = Topology.ContinuousMapGeneratedBy.curryEquiv.symm Topology.ContinuousMapGeneratedBy.id

@[simp]

theorem Topology.ContinuousMapGeneratedBy.ev_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] [∀ (i : ι), LocallyCompactSpace (X i)] [∀ (i j : ι), IsGeneratedBy X (X i × X j)] (y : Y) (f : ContinuousMapGeneratedBy X Y Z) : ev (y, f) = f y

def Topology.ContinuousMapGeneratedBy.postcomp {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] [∀ (i : ι), LocallyCompactSpace (X i)] [∀ (i j : ι), IsGeneratedBy X (X i × X j)] (p : ContinuousMapGeneratedBy X Z T) : ContinuousMapGeneratedBy X (ContinuousMapGeneratedBy X Y Z) (ContinuousMapGeneratedBy X Y T)

Given a X-continuous map p : Z → T, this is the postcomposition with p ContinuousMapGeneratedBy X Y Z → ContinuousMapGeneratedBy X Y T as a X-continuous map.

Equations

• p.postcomp = Topology.ContinuousMapGeneratedBy.curryEquiv (p.comp Topology.ContinuousMapGeneratedBy.ev)

@[simp]

theorem Topology.ContinuousMapGeneratedBy.postcomp_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {T : Type v''} [TopologicalSpace T] [∀ (i : ι), LocallyCompactSpace (X i)] [∀ (i j : ι), IsGeneratedBy X (X i × X j)] (p : ContinuousMapGeneratedBy X Z T) (g : ContinuousMapGeneratedBy X Y Z) : p.postcomp g = p.comp g