The category of topological spaces has all limits and colimits

Further, these limits and colimits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

def TopCat.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) : CategoryTheory.Limits.Cone F

A choice of limit cone for a functor F : J ⥤ TopCat. Generally you should just use limit.cone F, unless you need the actual definition (which is in terms of Types.limitCone).

def TopCat.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) : CategoryTheory.Limits.IsLimit (limitCone F)

The chosen cone TopCat.limitCone F for a functor F : J ⥤ TopCat is a limit cone. Generally you should just use limit.isLimit F, unless you need the actual definition (which is in terms of Types.limitConeIsLimit).

def TopCat.conePtOfConeForget {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) : Type u

Given a functor F : J ⥤ TopCat and a cone c : Cone (F ⋙ forget) of the underlying functor to types, this is the type c.pt with the infimum of the induced topologies by the maps c.π.app j.

@[implicit_reducible]

instance TopCat.topologicalSpaceConePtOfConeForget {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) : TopologicalSpace (conePtOfConeForget c)

def TopCat.coneOfConeForget {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) : CategoryTheory.Limits.Cone F

Given a functor F : J ⥤ TopCat and a cone c : Cone (F ⋙ forget) of the underlying functor to types, this is a cone for F whose point is c.pt with the infimum of the induced topologies by the maps c.π.app j.

@[simp]

theorem TopCat.coneOfConeForget_π_app {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) (j : J) : (coneOfConeForget c).π.app j = ofHom { toFun := c.π.app j, continuous_toFun := ⋯ }

@[simp]

theorem TopCat.coneOfConeForget_pt {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) : (coneOfConeForget c).pt = of (conePtOfConeForget c)

def TopCat.isLimitConeOfForget {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (coneOfConeForget c)

Given a functor F : J ⥤ TopCat and a cone c : Cone (F ⋙ forget) of the underlying functor to types, the limit of F is c.pt equipped with the infimum of the induced topologies by the maps c.π.app j.

theorem TopCat.induced_of_isLimit {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cone F) (hc : CategoryTheory.Limits.IsLimit c) : c.pt.str = ⨅ (j : J), TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (c.π.app j))) (F.obj j).str

theorem TopCat.nonempty_isLimit_iff_eq_induced {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cone F) (hc : CategoryTheory.Limits.IsLimit ((CategoryTheory.forget TopCat).mapCone c)) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ c.pt.str = ⨅ (j : J), TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (c.π.app j))) (F.obj j).str

theorem TopCat.limit_topology {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) [CategoryTheory.Limits.HasLimit F] : (CategoryTheory.Limits.limit F).str = ⨅ (j : J), TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j))) (F.obj j).str

theorem TopCat.hasLimit_iff_small_sections {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) : CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget TopCat)).sections

instance TopCat.topCat_hasLimitsOfShape (J : Type v) [CategoryTheory.Category.{v_1, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasLimitsOfShape J TopCat

instance TopCat.topCat_hasLimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} TopCat

instance TopCat.topCat_hasLimits : CategoryTheory.Limits.HasLimits TopCat

instance TopCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget TopCat)

instance TopCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget TopCat)

def TopCat.coconePtOfCoconeForget {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) : Type u

Given a functor F : J ⥤ TopCat and a cocone c : Cocone (F ⋙ forget) of the underlying cocone of types, this is the type c.pt with the supremum of the topologies that are coinduced by the maps c.ι.app j.

@[implicit_reducible]

instance TopCat.topologicalSpaceCoconePtOfCoconeForget {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) : TopologicalSpace (coconePtOfCoconeForget c)

def TopCat.coconeOfCoconeForget {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) : CategoryTheory.Limits.Cocone F

Given a functor F : J ⥤ TopCat and a cocone c : Cocone (F ⋙ forget) of the underlying cocone of types, this is a cocone for F whose point is c.pt with the supremum of the coinduced topologies by the maps c.ι.app j.

@[simp]

theorem TopCat.coconeOfCoconeForget_pt {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) : (coconeOfCoconeForget c).pt = of (coconePtOfCoconeForget c)

@[simp]

theorem TopCat.coconeOfCoconeForget_ι_app {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) (j : J) : (coconeOfCoconeForget c).ι.app j = ofHom { toFun := c.ι.app j, continuous_toFun := ⋯ }

def TopCat.isColimitCoconeOfForget {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (coconeOfCoconeForget c)

Given a functor F : J ⥤ TopCat and a cocone c : Cocone (F ⋙ forget) of the underlying cocone of types, the colimit of F is c.pt equipped with the supremum of the coinduced topologies by the maps c.ι.app j.

theorem TopCat.coinduced_of_isColimit {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) : c.pt.str = ⨆ (j : J), TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

theorem TopCat.isOpen_iff_of_isColimit {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) (X : Set ↑c.pt) : IsOpen X ↔ ∀ (j : J), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

theorem TopCat.isClosed_iff_of_isColimit {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) (X : Set ↑c.pt) : IsClosed X ↔ ∀ (j : J), IsClosed (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

theorem TopCat.continuous_iff_of_isColimit {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) {X : Type u'} [TopologicalSpace X] (f : ↑c.pt → X) : Continuous f ↔ ∀ (j : J), Continuous (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)))

theorem TopCat.nonempty_isColimit_iff_eq_coinduced {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit ((CategoryTheory.forget TopCat).mapCocone c)) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ c.pt.str = ⨆ (j : J), TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) (F.obj j).str

theorem TopCat.colimit_topology {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) [CategoryTheory.Limits.HasColimit F] : (CategoryTheory.Limits.colimit F).str = ⨆ (j : J), TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j))) (F.obj j).str

theorem TopCat.colimit_isOpen_iff {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) [CategoryTheory.Limits.HasColimit F] (U : Set ↑(CategoryTheory.Limits.colimit F)) : IsOpen U ↔ ∀ (j : J), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) ⁻¹' U)

theorem TopCat.hasColimit_iff_small_colimitType {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) : CategoryTheory.Limits.HasColimit F ↔ Small.{u, max u v} (F.comp (CategoryTheory.forget TopCat)).ColimitType

instance TopCat.topCat_hasColimitsOfShape (J : Type v) [CategoryTheory.Category.{v_1, v} J] [Small.{u, v} J] : CategoryTheory.Limits.HasColimitsOfShape J TopCat

instance TopCat.topCat_hasColimitsOfSize [UnivLE.{v, u}] : CategoryTheory.Limits.HasColimitsOfSize.{w, v, u, u + 1} TopCat

instance TopCat.topCat_hasColimits : CategoryTheory.Limits.HasColimits TopCat

instance TopCat.forget_preservesColimitsOfSize : CategoryTheory.Limits.PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget TopCat)

instance TopCat.forget_preservesColimits : CategoryTheory.Limits.PreservesColimits (CategoryTheory.forget TopCat)

def TopCat.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (of PUnit.{u + 1})

The terminal object of Top is PUnit.

noncomputable def TopCat.terminalIsoPUnit : ⊤_ TopCat ≅ of PUnit.{u + 1}

The terminal object of Top is PUnit.

def TopCat.isInitialPEmpty : CategoryTheory.Limits.IsInitial (of PEmpty.{u + 1})

The initial object of Top is PEmpty.

noncomputable def TopCat.initialIsoPEmpty : ⊥_ TopCat ≅ of PEmpty.{u + 1}

The initial object of Top is PEmpty.