The category of X-generated spaces, as a localization

Let X i be a family of topological spaces. In this file, we introduce a property of morphisms morphismPropertyWithGeneratedByTopologyEquiv X in the category TopCat: it consists of the morphisms corresponding to the canonical continuous maps WithGeneratedByTopology X Z → Z for all topological spaces Z. We show that the functor TopCat.toContinuousGeneratedByCat X : TopCat ⥤ ContinuousGeneratedByCat X makes ContinuousGeneratedByCat X the localized category of TopCat with respect to this class of morphisms. Similarly, TopCat.toGeneratedByTopCat : TopCat ⥤ GeneratedByTopCat X is also a localization functor.

def TopCat.morphismPropertyWithGeneratedByTopologyEquiv {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.MorphismProperty TopCat

Given a family of topological spaces X, this is the family of morphisms in TopCat corresponding to the continuous maps WithGeneratedByTopology X Z → Z for all topological spaces Z.

Equations

• TopCat.morphismPropertyWithGeneratedByTopologyEquiv X = CategoryTheory.MorphismProperty.ofHoms GeneratedByTopCat.adjCounit.app

instance TopCat.instIsLocalizationContinuousGeneratedByCatToContinuousGeneratedByCatMorphismPropertyWithGeneratedByTopologyEquiv {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : (toContinuousGeneratedByCat X).IsLocalization (morphismPropertyWithGeneratedByTopologyEquiv X)

instance TopCat.instIsLocalizationGeneratedByTopCatToGeneratedByTopCatMorphismPropertyWithGeneratedByTopologyEquiv {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : toGeneratedByTopCat.IsLocalization (morphismPropertyWithGeneratedByTopologyEquiv X)