Maps from generated spaces

A topological space Y is generated by a family of spaces X (Mathlib's IsGeneratedBy X Y) when its topology is coinduced by all continuous maps from the spaces X i. An empty space has only one topology, so it is generated by every family (TauCeti.instIsGeneratedByOfIsEmpty). In particular every empty space is delta-generated.

A continuous map from a generated space lifts uniquely through the generated-topology counit on its target (ContinuousMap.toGeneratedBy). The source's generation hypothesis is retained explicitly, as required for parameter families into a refined mapping space.

instance TauCeti.instIsGeneratedByOfIsEmpty {ι : Type u_1} (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (Y : Type u_3) [TopologicalSpace Y] [IsEmpty Y] : Topology.IsGeneratedBy X Y

An empty space is generated by any family of spaces: it has only one topology.

def Topology.WithGeneratedByTopology.counit {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → TopologicalSpace (G i)] (X : Type u_3) [TopologicalSpace X] : C(WithGeneratedByTopology G X, X)

The continuous counit from the generated refinement to the original space.

@[simp]

theorem Topology.WithGeneratedByTopology.counit_apply {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → TopologicalSpace (G i)] {X : Type u_3} [TopologicalSpace X] (x : WithGeneratedByTopology G X) : (counit G X) x = equiv x

@[simp]

theorem GeneratedByTopCat.adjCounit_app_hom {ι : Type u_1} (G : ι → Type u_2) [(i : ι) → TopologicalSpace (G i)] (X : TopCat) : TopCat.Hom.hom (adjCounit.app X) = Topology.WithGeneratedByTopology.counit G ↑X

The underlying continuous map of the categorical counit is the generated-topology counit.

def ContinuousMap.toGeneratedBy {ι : Type u_1} {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (G : ι → Type u_5) [(i : ι) → TopologicalSpace (G i)] [Topology.IsGeneratedBy G X] : C(X, Topology.WithGeneratedByTopology G Y)

Lift a continuous map from a generated source to the generated refinement of its target.

@[simp]

theorem ContinuousMap.toGeneratedBy_apply {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → TopologicalSpace (G i)] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [Topology.IsGeneratedBy G X] (f : C(X, Y)) (x : X) : (f.toGeneratedBy G) x = Topology.WithGeneratedByTopology.equiv.symm (f x)

@[simp]

theorem ContinuousMap.equiv_comp_toGeneratedBy {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → TopologicalSpace (G i)] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [Topology.IsGeneratedBy G X] (f : C(X, Y)) : (Topology.WithGeneratedByTopology.counit G Y).comp (f.toGeneratedBy G) = f

Composing the lifted map with the counit recovers the original map.

@[simp]

theorem ContinuousMap.toGeneratedBy_equiv_comp {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → TopologicalSpace (G i)] {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [Topology.IsGeneratedBy G X] (f : C(X, Topology.WithGeneratedByTopology G Y)) : ((Topology.WithGeneratedByTopology.counit G Y).comp f).toGeneratedBy G = f

A map to the generated refinement is recovered by lifting its composite with the counit.