The category of X-generated spaces

Let X i be a family of topological spaces. In this file, we define the category GeneratedByTopCat X of X-generated spaces: this is defined as a full subcategory of TopCat.

We also introduce an equivalent category ContinuousGeneratedByCat X whose objects are all topological spaces, but morphisms from Y to Z identify to the type ContinuousMapGeneratedBy X Y Z of X-continuous maps from Y to Z. While GeneratedByTopCat X is defined as a full subcategory of TopCat, ContinuousGeneratedByCat X should be thought of as a localization of the category TopCat. This alternative point of view from the article by Martín Escardó, Jimmie Lawson and Alex Simpson shall allow a very nice construction of a cartesian monoidal closed structure on GeneratedByTopCat X under suitable assumptions (TODO @joelriou).

References

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

@[reducible, inline]

abbrev TopCat.generatedBy {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.ObjectProperty TopCat

The property of objects of TopCat which is satisfied by X-generated spaces.

Equations

• TopCat.generatedBy X Y = Topology.IsGeneratedBy X ↑Y

theorem TopCat.generatedBy_def {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : TopCat) : generatedBy X Y ↔ Topology.IsGeneratedBy X ↑Y

@[reducible, inline]

abbrev GeneratedByTopCat {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : Type (v + 1)

The full subcategory of TopCat consisting of X-generated spaces.

Equations

• GeneratedByTopCat X = (TopCat.generatedBy X).FullSubcategory

@[reducible, inline]

abbrev GeneratedByTopCat.toTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor (GeneratedByTopCat X) TopCat

The inclusion functor GeneratedByTopCat X ⥤ TopCat.

Equations

• GeneratedByTopCat.toTopCat = (TopCat.generatedBy X).ι

instance GeneratedByTopCat.instIsGeneratedByCarrierObjTopCatToTopCat {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : GeneratedByTopCat X) : Topology.IsGeneratedBy X ↑(toTopCat.obj Y)

@[reducible, inline]

abbrev GeneratedByTopCat.fullyFaithfulToTopCat {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : toTopCat.FullyFaithful

The inclusion functor toTopCat : GeneratedByTopCat X ⥤ TopCat is fully faithful.

Equations

• GeneratedByTopCat.fullyFaithfulToTopCat X = (TopCat.generatedBy X).fullyFaithfulι

@[reducible, inline]

abbrev GeneratedByTopCat.of {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [TopologicalSpace Y] [Topology.IsGeneratedBy X Y] : GeneratedByTopCat X

Constructor for objects in the category of X-generated spaces.

Equations

• GeneratedByTopCat.of Y = { obj := TopCat.of Y, property := inst✝ }

@[implicit_reducible]

instance GeneratedByTopCat.instCoeSortType {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : CoeSort (GeneratedByTopCat X) (Type v)

Equations

• GeneratedByTopCat.instCoeSortType X = { coe := fun (Y : GeneratedByTopCat X) => ↑Y.obj }

instance GeneratedByTopCat.instIsGeneratedByCarrierObjTopCatGeneratedBy {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : GeneratedByTopCat X) : Topology.IsGeneratedBy X ↑Y.obj

structure ContinuousGeneratedByCat {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : Type (v + 1)

Let X i be a family of topological spaces. This is the type of objects in a category ContinuousGeneratedByCat X where:

• objects are topological spaces;
• morphisms are X-continuous maps.

• of :: (
• carrier : Type v

  The underlying type of an object in ContinuousGeneratedByCat X.

• str : TopologicalSpace ↑self
• )

@[implicit_reducible]

instance ContinuousGeneratedByCat.instCoeSortType {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CoeSort (ContinuousGeneratedByCat X) (Type v)

Equations

• ContinuousGeneratedByCat.instCoeSortType = { coe := ContinuousGeneratedByCat.carrier }

theorem ContinuousGeneratedByCat.coe_of {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (Y : Type v) [TopologicalSpace Y] : ↑{ carrier := Y, str := inst✝ } = Y

theorem ContinuousGeneratedByCat.of_carrier {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (Y : ContinuousGeneratedByCat X) : { carrier := ↑Y, str := Y.str } = Y

structure ContinuousGeneratedByCat.Hom {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (Y Z : ContinuousGeneratedByCat X) : Type v

The type of morphisms in the category ContinuousGeneratedByCat X is a one-field structure containing a field of type ContinuousMapGeneratedBy, i.e. X-continuous maps.

• hom : Topology.ContinuousMapGeneratedBy X ↑Y ↑Z

  the underlying X-continuous map of a morphism in ContinuousGeneratedByCat X.

@[implicit_reducible]

instance ContinuousGeneratedByCat.instCategory {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Category.{v, v + 1} (ContinuousGeneratedByCat X)

Equations

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

@[implicit_reducible]

instance ContinuousGeneratedByCat.instConcreteCategoryContinuousMapGeneratedByCarrier {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.ConcreteCategory (ContinuousGeneratedByCat X) fun (Y Z : ContinuousGeneratedByCat X) => Topology.ContinuousMapGeneratedBy X ↑Y ↑Z

Equations

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

def ContinuousGeneratedByCat.homMk {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X} (f : ↑Y → ↑Z) (hf : Topology.ContinuousGeneratedBy X f) : Y ⟶ Z

Constructor for morphisms in ContinuousGeneratedByCat X.

Equations

• ContinuousGeneratedByCat.homMk f hf = { hom := { toFun := f, prop := hf } }

@[simp]

theorem ContinuousGeneratedByCat.homMk_hom_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X} (f : ↑Y → ↑Z) (hf : Topology.ContinuousGeneratedBy X f) (a✝ : ↑Y) : (homMk f hf).hom a✝ = f a✝

@[implicit_reducible]

instance ContinuousGeneratedByCat.instHasForget₂TopCatContinuousMapCarrierContinuousMapGeneratedByCarrier {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.HasForget₂ TopCat (ContinuousGeneratedByCat X)

Use the abbreviation TopCat.toContinuousGeneratedByCat for the faithful functor TopCat ⥤ ContinuousGeneratedByCat X which sends a topological space Y to the same type Y, with the same topology, but considered as an object of ContinuousGeneratedByCat X.

Equations

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

@[simp]

theorem ContinuousGeneratedByCat.forget₂_obj {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (Y : TopCat) : CategoryTheory.HasForget₂.forget₂.obj Y = { carrier := ↑Y, str := Y.str }

@[simp]

theorem ContinuousGeneratedByCat.forget₂_map_hom_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {X✝ Y✝ : TopCat} (f : X✝ ⟶ Y✝) (a : ↑X✝) : (CategoryTheory.HasForget₂.forget₂.map f).hom a = (CategoryTheory.ConcreteCategory.hom f) a

@[reducible, inline]

abbrev TopCat.toContinuousGeneratedByCat {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor TopCat (ContinuousGeneratedByCat X)

The faithful functor TopCat ⥤ ContinuousGeneratedByCat X which sends a topological space Y to the same type Y, with the same topology, but considered as an object of ContinuousGeneratedByCat X.

Equations

• TopCat.toContinuousGeneratedByCat X = CategoryTheory.forget₂ TopCat (ContinuousGeneratedByCat X)

instance instFaithfulTopCatContinuousGeneratedByCatToContinuousGeneratedByCat {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : (TopCat.toContinuousGeneratedByCat X).Faithful

def ContinuousGeneratedByCat.toTopCat {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor (ContinuousGeneratedByCat X) TopCat

The functor ContinuousGeneratedByCat X ⥤ TopCat which sends a topological space Y in the category ContinuousGeneratedByCat X to the topological space WithGeneratedByTopology X Y.

Equations

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

@[simp]

theorem ContinuousGeneratedByCat.toTopCat_obj {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] (Y : ContinuousGeneratedByCat X) : (toTopCat X).obj Y = TopCat.of (Topology.WithGeneratedByTopology X ↑Y)

theorem ContinuousGeneratedByCat.toTopCat_map_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X} (f : Y ⟶ Z) (y : Topology.WithGeneratedByTopology X ↑Y) : (CategoryTheory.ConcreteCategory.hom ((toTopCat X).map f)) y = Topology.WithGeneratedByTopology.equiv.symm ((CategoryTheory.ConcreteCategory.hom f) (Topology.WithGeneratedByTopology.equiv y))

def ContinuousGeneratedByCat.fullyFaithfulToTopCat {ι : Type t} (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] : (toTopCat X).FullyFaithful

The functor ContinuousGeneratedByCat.toTopCat : ContinuousGeneratedByCat X ⥤ TopCat is fully faithful.

Equations

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

def ContinuousGeneratedByCat.adjUnitIso {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor.id (ContinuousGeneratedByCat X) ≅ (toTopCat X).comp (TopCat.toContinuousGeneratedByCat X)

The unit (isomorphism) of the adjunction ContinuousGeneratedByCat.adj between the categories ContinuousGeneratedByCat X and TopCat.

Equations

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

def ContinuousGeneratedByCat.adjCounit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : (TopCat.toContinuousGeneratedByCat X).comp (toTopCat X) ⟶ CategoryTheory.Functor.id TopCat

The counit of the adjunction ContinuousGeneratedByCat.adj between the categories ContinuousGeneratedByCat X and TopCat.

Equations

• ContinuousGeneratedByCat.adjCounit = { app := fun (Z : TopCat) => TopCat.ofHom { toFun := ⇑Topology.WithGeneratedByTopology.equiv, continuous_toFun := ⋯ }, naturality := ⋯ }

def ContinuousGeneratedByCat.adj {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : toTopCat X ⊣ TopCat.toContinuousGeneratedByCat X

The adjunction between the categories ContinuousGeneratedByCat X and TopCat.

Equations

• ContinuousGeneratedByCat.adj = { unit := ContinuousGeneratedByCat.adjUnitIso.hom, counit := ContinuousGeneratedByCat.adjCounit, left_triangle_components := ⋯, right_triangle_components := ⋯ }

@[simp]

theorem ContinuousGeneratedByCat.adj_unit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : adj.unit = adjUnitIso.hom

@[simp]

theorem ContinuousGeneratedByCat.adj_counit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : adj.counit = adjCounit

instance ContinuousGeneratedByCat.instIsLeftAdjointTopCatToTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : (toTopCat X).IsLeftAdjoint

instance ContinuousGeneratedByCat.instIsRightAdjointTopCatToContinuousGeneratedByCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : (TopCat.toContinuousGeneratedByCat X).IsRightAdjoint

instance ContinuousGeneratedByCat.instIsIsoFunctorUnitTopCatAdj {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.IsIso adj.unit

def ContinuousGeneratedByCat.fromGeneratedByTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor (GeneratedByTopCat X) (ContinuousGeneratedByCat X)

The functor GeneratedByTopCat X ⥤ ContinuousGeneratedByCat X which is part of the equivalence ContinuousGeneratedByCat.equivalence. It sends an X-generated topological space Y to the topological space Y, considered as an object of ContinuousGeneratedByCat X.

Equations

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

@[simp]

theorem ContinuousGeneratedByCat.fromGeneratedByTopCat_obj {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (Y : GeneratedByTopCat X) : fromGeneratedByTopCat.obj Y = { carrier := ↑Y.obj, str := Y.obj.str }

@[simp]

theorem ContinuousGeneratedByCat.fromGeneratedByTopCat_map_hom_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {X✝ Y✝ : GeneratedByTopCat X} (f : X✝ ⟶ Y✝) (a : ↑X✝.obj) : (fromGeneratedByTopCat.map f).hom a = (CategoryTheory.ConcreteCategory.hom f) a

def ContinuousGeneratedByCat.equivalenceFunctorIso {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : fromGeneratedByTopCat.comp (toTopCat X) ≅ GeneratedByTopCat.toTopCat

The isomorphism between fromGeneratedByTopCat ⋙ toTopCat X ≅ GeneratedByTopCat.toTopCat.

Equations

• ContinuousGeneratedByCat.equivalenceFunctorIso = CategoryTheory.NatIso.ofComponents (fun (Y : GeneratedByTopCat X) => TopCat.isoOfHomeo Topology.IsGeneratedBy.homeomorph) ⋯

def ContinuousGeneratedByCat.toGeneratedByTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor (ContinuousGeneratedByCat X) (GeneratedByTopCat X)

The functor ContinuousGeneratedByCat X ⥤ GeneratedByTopCat X which is part of the equivalence ContinuousGeneratedByCat.equivalence.

Equations

• ContinuousGeneratedByCat.toGeneratedByTopCat = (TopCat.generatedBy X).lift (ContinuousGeneratedByCat.toTopCat X) ⋯

@[simp]

theorem ContinuousGeneratedByCat.toGeneratedByTopCat_obj {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] (X✝ : ContinuousGeneratedByCat X) : toGeneratedByTopCat.obj X✝ = { obj := TopCat.of (Topology.WithGeneratedByTopology X ↑X✝), property := ⋯ }

theorem ContinuousGeneratedByCat.toGeneratedByTopCat_map_apply {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X} (f : Y ⟶ Z) (y : Topology.WithGeneratedByTopology X ↑Y) : (CategoryTheory.ConcreteCategory.hom (toGeneratedByTopCat.map f)) y = Topology.WithGeneratedByTopology.equiv.symm ((CategoryTheory.ConcreteCategory.hom f) (Topology.WithGeneratedByTopology.equiv y))

def ContinuousGeneratedByCat.equivalenceUnitIso {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor.id (GeneratedByTopCat X) ≅ fromGeneratedByTopCat.comp toGeneratedByTopCat

The unit isomorphism of the equivalence ContinuousGeneratedByCat.equivalence.

Equations

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

@[reducible, inline]

abbrev ContinuousGeneratedByCat.equivalenceCounitIso {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : toGeneratedByTopCat.comp fromGeneratedByTopCat ≅ CategoryTheory.Functor.id (ContinuousGeneratedByCat X)

The counit isomorphism of the equivalence ContinuousGeneratedByCat.equivalence.

Equations

• ContinuousGeneratedByCat.equivalenceCounitIso = ContinuousGeneratedByCat.adjUnitIso.symm

def ContinuousGeneratedByCat.equivalence {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : GeneratedByTopCat X ≌ ContinuousGeneratedByCat X

The equivalence of categories GeneratedByTopCat X ≌ ContinuousGeneratedByCat X.

Equations

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

@[simp]

theorem ContinuousGeneratedByCat.equivalence_unitIso {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : equivalence.unitIso = equivalenceUnitIso

@[simp]

theorem ContinuousGeneratedByCat.equivalence_counitIso {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : equivalence.counitIso = equivalenceCounitIso

@[simp]

theorem ContinuousGeneratedByCat.equivalence_functor {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : equivalence.functor = fromGeneratedByTopCat

@[simp]

theorem ContinuousGeneratedByCat.equivalence_inverse {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : equivalence.inverse = toGeneratedByTopCat

instance ContinuousGeneratedByCat.instIsEquivalenceGeneratedByTopCatFromGeneratedByTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : fromGeneratedByTopCat.IsEquivalence

instance ContinuousGeneratedByCat.instIsEquivalenceGeneratedByTopCatToGeneratedByTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : toGeneratedByTopCat.IsEquivalence

def TopCat.toGeneratedByTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor TopCat (GeneratedByTopCat X)

The functor TopCat.{v} ⥤ GeneratedByTopCat X.

Equations

• TopCat.toGeneratedByTopCat = (TopCat.toContinuousGeneratedByCat X).comp ContinuousGeneratedByCat.toGeneratedByTopCat

def GeneratedByTopCat.adjUnitIso {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.Functor.id (GeneratedByTopCat X) ≅ toTopCat.comp TopCat.toGeneratedByTopCat

The unit (isomorphism) of the adjunction GeneratedByTopCat.adj between the categories GeneratedByTopCat X and TopCat.

Equations

• GeneratedByTopCat.adjUnitIso = ContinuousGeneratedByCat.equivalenceUnitIso

def GeneratedByTopCat.adjCounit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : TopCat.toGeneratedByTopCat.comp toTopCat ⟶ CategoryTheory.Functor.id TopCat

The counit of the adjunction GeneratedByTopCat.adj between the categories GeneratedByTopCat X and TopCat.

Equations

• GeneratedByTopCat.adjCounit = ContinuousGeneratedByCat.adjCounit

def GeneratedByTopCat.adj {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : toTopCat ⊣ TopCat.toGeneratedByTopCat

The adjunction between the categories GeneratedByTopCat X and TopCat. The left adjoint is the inclusion functor, and the right adjoint sends a topological space Y to the underlying type of Y endowed with the X-generated topology.

Equations

• GeneratedByTopCat.adj = { unit := GeneratedByTopCat.adjUnitIso.hom, counit := GeneratedByTopCat.adjCounit, left_triangle_components := ⋯, right_triangle_components := ⋯ }

@[simp]

theorem GeneratedByTopCat.adj_unit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : adj.unit = adjUnitIso.hom

@[simp]

theorem GeneratedByTopCat.adj_counit {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : adj.counit = adjCounit

instance GeneratedByTopCat.instIsIsoFunctorUnitTopCatAdj {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : CategoryTheory.IsIso adj.unit

instance GeneratedByTopCat.instIsLeftAdjointTopCatToTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : toTopCat.IsLeftAdjoint

instance GeneratedByTopCat.instIsRightAdjointTopCatToGeneratedByTopCat {ι : Type t} {X : ι → Type u} [(i : ι) → TopologicalSpace (X i)] : TopCat.toGeneratedByTopCat.IsRightAdjoint