The topology that is generated by a family of topological spaces

Let X : ι → Type u be a family of topological spaces. Let Y be a topological space. We introduce a type synonym WithGeneratedByTopology X Y for Y. This type is endowed with the X-generated topology, which is coinduced by all continuous maps X i → Y. When the bijection WithGeneratedByTopology X Y ≃ Y is a homeomorphism, we say that Y is X-generated (typeclass IsGeneratedBy X Y).

TODO (@joelriou)

• Redefine compactly generated spaces and delta generated spaces using these definitions
• Define the category of X-generated spaces and show that it is coreflective in TopCat
• Show that under suitable assumptions, the category of X-generated spaces is a closed cartesian monoidal category.

References

• [Rainer M. Vogt, Convenient categories of topological spaces for homotopy theory][vogt-1971]
• [Martín Escardó, Jimmie Lawson and Alex Simpson, Comparing Cartesian closed categories of (core) compactly generated spaces][escardo-lawson-simpson-2004]

def TopologicalSpace.generatedBy {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] : TopologicalSpace Y

Given a family of topological spaces X i, the X-generated topology on a topological space Y is the topology that is coinduced by all continuous maps X i → Y.

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

Given a family of topological spaces X i, and a topological space Y, this is a type synonym for Y which we endow with the X-generated topology.

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

The obvious bijection WithGeneratedByTopology X Y ≃ Y, where the source is endowed with the X-generated topology. See continuous_equiv for the continuity of equiv. The inverse map equiv.symm is continuous iff Y is X-generated, see isGeneratedBy_iff.

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

theorem Topology.WithGeneratedByTopology.isOpen_iff {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {U : Set (WithGeneratedByTopology X Y)} : IsOpen U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen (⇑f ⁻¹' (⇑equiv.symm ⁻¹' U))

theorem Topology.WithGeneratedByTopology.isClosed_iff {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {U : Set (WithGeneratedByTopology X Y)} : IsClosed U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed (⇑f ⁻¹' (⇑equiv.symm ⁻¹' U))

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

theorem Topology.WithGeneratedByTopology.continuous_equiv {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] : Continuous ⇑equiv

theorem TopologicalSpace.generatedBy_le {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y} : generatedBy X ≤ tY

theorem TopologicalSpace.generatedBy_mono {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} {t₁ t₂ : TopologicalSpace Y} (h : t₁ ≤ t₂) : generatedBy X ≤ generatedBy X

class Topology.IsGeneratedBy {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [tY : TopologicalSpace Y] : Prop

Given a family of topological spaces X i, we say that a topological space is X-generated (IsGeneratedBy X Y) when the topology on Y is the X-generated topology, i.e. when the identity is a homeomorphism WithGeneratedByTopology X Y ≃ₜ Y (see IsGeneratedBy.homeomorph).

• continuous_equiv_symm : Continuous ⇑WithGeneratedByTopology.equiv.symm

theorem Topology.isGeneratedBy_iff {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [tY : TopologicalSpace Y] : IsGeneratedBy X Y ↔ Continuous ⇑WithGeneratedByTopology.equiv.symm

theorem Topology.IsGeneratedBy.le_generatedBy {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y} [IsGeneratedBy X Y] : tY ≤ TopologicalSpace.generatedBy X

theorem Topology.IsGeneratedBy.generatedBy_eq {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y} [IsGeneratedBy X Y] : TopologicalSpace.generatedBy X = tY

theorem Topology.IsGeneratedBy.iff_le_generatedBy {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y} : IsGeneratedBy X Y ↔ tY ≤ TopologicalSpace.generatedBy X

def Topology.IsGeneratedBy.homeomorph {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] [IsGeneratedBy X Y] : WithGeneratedByTopology X Y ≃ₜ Y

The homeomorphism WithGeneratedByTopology X Y ≃ₜ Y when Y is X-generated.

@[simp]

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

@[simp]

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

theorem Topology.IsGeneratedBy.isOpen_iff {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] [IsGeneratedBy X Y] {U : Set Y} : IsOpen U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen (⇑f ⁻¹' U)

theorem Topology.IsGeneratedBy.isClosed_iff {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] [IsGeneratedBy X Y] {U : Set Y} : IsClosed U ↔ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed (⇑f ⁻¹' U)

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

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

instance Topology.IsGeneratedBy.inst {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (i : ι) : IsGeneratedBy X (X i)

instance Topology.IsGeneratedBy.instWithGeneratedByTopology {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] : IsGeneratedBy X (WithGeneratedByTopology X Y)

instance Topology.IsGeneratedBy.instPUnit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : IsGeneratedBy X PUnit.{v + 1}

theorem Topology.IsGeneratedBy.coinduced {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {Z : Type v'} [IsGeneratedBy X Y] (f : Y → Z) : IsGeneratedBy X Z

Any topology coinduced by an X-generated topology is X-generated.

theorem Topology.IsGeneratedBy.iSup {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {κ : Sort u_2} {t : κ → TopologicalSpace Y} (h : ∀ (k : κ), IsGeneratedBy X Y) : IsGeneratedBy X Y

Suprema of X-generated topologies are X-generated.

theorem Topology.IsGeneratedBy.sup {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {t₁ t₂ : TopologicalSpace Y} (h₁ : IsGeneratedBy X Y) (h₂ : IsGeneratedBy X Y) : IsGeneratedBy X Y

Suprema of X-generated topologies are X-generated.

theorem Topology.IsQuotientMap.isGeneratedBy {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] {f : Y → Z} (hf : IsQuotientMap f) [IsGeneratedBy X Y] : IsGeneratedBy X Z

instance Quot.isGeneratedBy {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] [Topology.IsGeneratedBy X Y] {r : Y → Y → Prop} : Topology.IsGeneratedBy X (Quot r)

Quotients of X-generated spaces are X-generated.

instance Quotient.isGeneratedBy {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] [Topology.IsGeneratedBy X Y] {s : Setoid Y} : Topology.IsGeneratedBy X (Quotient s)

Quotients of X-generated spaces are X-generated.

instance Sum.isGeneratedBy {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y] {Z : Type v'} [TopologicalSpace Z] [Topology.IsGeneratedBy X Y] [Topology.IsGeneratedBy X Z] : Topology.IsGeneratedBy X (Y ⊕ Z)

Disjoint unions of X-generated spaces are X-generated.

instance Sigma.isGeneratedBy {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {κ : Type u_1} {Y : κ → Type u_2} [(k : κ) → TopologicalSpace (Y k)] [∀ (k : κ), Topology.IsGeneratedBy X (Y k)] : Topology.IsGeneratedBy X ((k : κ) × Y k)

Disjoint unions of X-generated spaces are X-generated.