X-continuous maps

Given a family X i of topological spaces, we introduce a predicate ContinuousGeneratedBy X on maps g : Y ⟶ Z saying that g is X-continuous, i.e. for any continuous map f : X i → Y, the composition g ∘ f is continuous.

References

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

def Topology.ContinuousGeneratedBy {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] (g : Y → Z) : Prop

Given a family X i of topological space, this is a predicate on maps g : Y → Z between topological spaces saying that for any continuous map f : X i → Y, the composition g ∘ f is continuous. We say that g is X-continuous.

Equations

• Topology.ContinuousGeneratedBy X g = ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑f)

theorem Topology.continuousGeneratedBy_def {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] (g : Y → Z) : ContinuousGeneratedBy X g ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous (g ∘ ⇑f)

theorem Topology.continuousGeneratedBy_iff {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] (g : Y → Z) : ContinuousGeneratedBy X g ↔ Continuous (⇑WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑WithGeneratedByTopology.equiv)

def Topology.ContinuousGeneratedBy.continuousMap {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {g : Y → Z} (hg : ContinuousGeneratedBy X g) : C(WithGeneratedByTopology X Y, WithGeneratedByTopology X Z)

A X-continuous map g : Y → Z induces a continuous map between the types Y and Z equipped with the X-generated topology.

Equations

• hg.continuousMap = { toFun := ⇑Topology.WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑Topology.WithGeneratedByTopology.equiv, continuous_toFun := ⋯ }

@[simp]

theorem Topology.ContinuousGeneratedBy.continuousMap_coe {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {g : Y → Z} (hg : ContinuousGeneratedBy X g) : ⇑hg.continuousMap = ⇑WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑WithGeneratedByTopology.equiv

@[simp]

theorem Topology.ContinuousGeneratedBy.id {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] : ContinuousGeneratedBy X _root_.id

theorem Topology.ContinuousGeneratedBy.comp {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {g : Y → Z} (hg : ContinuousGeneratedBy X g) {T : Type u_1} [TopologicalSpace T] {f : T → Y} (hf : ContinuousGeneratedBy X f) : ContinuousGeneratedBy X (g ∘ f)

theorem Continuous.continuousGeneratedBy {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {g : Y → Z} (hg : Continuous g) : Topology.ContinuousGeneratedBy X g

structure Topology.ContinuousMapGeneratedBy {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [TopologicalSpace Y] (Z : Type v') [TopologicalSpace Z] : Type (max v v')

The (bundled) type of X-continuous maps Y → Z.

• toFun : Y → Z

  the underlying map of a X-continuous map

• prop : ContinuousGeneratedBy X self.toFun

theorem Topology.ContinuousMapGeneratedBy.ext {ι : Type t} {X : ι → Type u} {inst✝ : (i : ι) → TopologicalSpace (X i)} {Y : Type v} {inst✝¹ : TopologicalSpace Y} {Z : Type v'} {inst✝² : TopologicalSpace Z} {x y : ContinuousMapGeneratedBy X Y Z} (toFun : x.toFun = y.toFun) : x = y

theorem Topology.ContinuousMapGeneratedBy.ext_iff {ι : Type t} {X : ι → Type u} {inst✝ : (i : ι) → TopologicalSpace (X i)} {Y : Type v} {inst✝¹ : TopologicalSpace Y} {Z : Type v'} {inst✝² : TopologicalSpace Z} {x y : ContinuousMapGeneratedBy X Y Z} : x = y ↔ x.toFun = y.toFun

@[implicit_reducible]

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

Equations

• Topology.instFunLikeContinuousMapGeneratedBy = { coe := fun (f : Topology.ContinuousMapGeneratedBy X Y Z) => f.toFun, coe_injective' := ⋯ }

def Topology.ContinuousMapGeneratedBy.id {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] : ContinuousMapGeneratedBy X Y Y

The identity, as a X-continous map.

Equations

• Topology.ContinuousMapGeneratedBy.id = { toFun := id, prop := ⋯ }

@[simp]

theorem Topology.ContinuousMapGeneratedBy.id_toFun {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] (a : Y) : id a = _root_.id a

def Topology.ContinuousMapGeneratedBy.comp {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type u_1} [TopologicalSpace Z] {T : Type u_2} [TopologicalSpace T] (g : ContinuousMapGeneratedBy X Y Z) (f : ContinuousMapGeneratedBy X T Y) : ContinuousMapGeneratedBy X T Z

The composition of X-continuous maps.

Equations

• g.comp f = { toFun := g.toFun ∘ f.toFun, prop := ⋯ }

@[simp]

theorem Topology.ContinuousMapGeneratedBy.comp_toFun {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [TopologicalSpace Y] {Z : Type u_1} [TopologicalSpace Z] {T : Type u_2} [TopologicalSpace T] (g : ContinuousMapGeneratedBy X Y Z) (f : ContinuousMapGeneratedBy X T Y) (a✝ : T) : (g.comp f) a✝ = (g.toFun ∘ f.toFun) a✝

def Topology.WithGeneratedByTopology.equivSymmAsContinuousMapGeneratedBy {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [TopologicalSpace Y] : ContinuousMapGeneratedBy X Y (WithGeneratedByTopology X Y)

The identity WithGeneratedByTopology.equiv.symm : Y → WithGeneratedByTopology X Y as a X-continuous map.

Equations

• Topology.WithGeneratedByTopology.equivSymmAsContinuousMapGeneratedBy X Y = { toFun := ⇑Topology.WithGeneratedByTopology.equiv.symm, prop := ⋯ }

@[simp]

theorem Topology.WithGeneratedByTopology.equivSymmAsContinuousMapGeneratedBy_coe {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [TopologicalSpace Y] : ⇑(equivSymmAsContinuousMapGeneratedBy X Y) = ⇑equiv.symm

def Topology.WithGeneratedByTopology.equivAsContinuousMapGeneratedBy {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [TopologicalSpace Y] : ContinuousMapGeneratedBy X (WithGeneratedByTopology X Y) Y

The identity WithGeneratedByTopology.equiv : WithGeneratedByTopology X Y → Y as a X-continuous map.

Equations

• Topology.WithGeneratedByTopology.equivAsContinuousMapGeneratedBy X Y = { toFun := ⇑Topology.WithGeneratedByTopology.equiv, prop := ⋯ }

@[simp]

theorem Topology.WithGeneratedByTopology.equivAsContinuousMapGeneratedBy_coe {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [TopologicalSpace Y] : ⇑(equivAsContinuousMapGeneratedBy X Y) = ⇑equiv