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).

Equations

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

def TopCat.limitConeInfi {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 whose topology is defined as an infimum of topologies infimum. Generally you should just use limit.cone F, unless you need the actual definition (which is in terms of Types.limitCone).

Equations

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

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).

Equations

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

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

The chosen cone TopCat.limitConeInfi 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).

Equations

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

instance TopCat.topCat_hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{w, v, max u v, max (u + 1) (v + 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 infimum of the topologies that are coinduced by the maps c.ι.app j.

Equations

• TopCat.coconePtOfCoconeForget c = c.pt

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)

Equations

• TopCat.topologicalSpaceCoconePtOfCoconeForget c = ⨆ (j : J), TopologicalSpace.coinduced (c.ι.app j) (F.obj j).str

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 infimum of the coinduced topologies by the maps c.ι.app j.

Equations

• TopCat.coconeOfCoconeForget c = { pt := TopCat.of (TopCat.coconePtOfCoconeForget c), ι := { app := fun (j : J) => TopCat.ofHom { toFun := c.ι.app j, continuous_toFun := ⋯ }, naturality := ⋯ } }

@[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 infimum of the coinduced topologies by the maps c.ι.app j.

Equations

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

@[deprecated TopCat.coconeOfCoconeForget (since := "2024-12-31")]

def TopCat.colimitCocone {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

Alias of TopCat.coconeOfCoconeForget.

---

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 infimum of the coinduced topologies by the maps c.ι.app j.

Equations

• @TopCat.colimitCocone = @TopCat.coconeOfCoconeForget

@[deprecated TopCat.isColimitCoconeOfForget (since := "2024-12-31")]

def TopCat.colimitCoconeIsColimit {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)

Alias of TopCat.isColimitCoconeOfForget.

---

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 infimum of the coinduced topologies by the maps c.ι.app j.

Equations

• @TopCat.colimitCoconeIsColimit = @TopCat.isColimitCoconeOfForget

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 w} [TopologicalSpace X] (f : ↑c.pt → X) : Continuous f ↔ ∀ (j : J), Continuous (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)))

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_quot {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat) : CategoryTheory.Limits.HasColimit F ↔ Small.{u, max u v} (CategoryTheory.Limits.Types.Quot (F.comp (CategoryTheory.forget TopCat)))

instance TopCat.topCat_hasColimitsOfSize : CategoryTheory.Limits.HasColimitsOfSize.{w, v, max u v, max (u + 1) (v + 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.

Equations

• TopCat.isTerminalPUnit = CategoryTheory.Limits.IsTerminal.ofUnique (TopCat.of PUnit.{?u.10 + 1})

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

The terminal object of Top is PUnit.

Equations

• TopCat.terminalIsoPUnit = CategoryTheory.Limits.terminalIsTerminal.uniqueUpToIso TopCat.isTerminalPUnit

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

The initial object of Top is PEmpty.

Equations

• TopCat.isInitialPEmpty = CategoryTheory.Limits.IsInitial.ofUnique (TopCat.of PEmpty.{?u.10 + 1})

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

The initial object of Top is PEmpty.

Equations

• TopCat.initialIsoPEmpty = CategoryTheory.Limits.initialIsInitial.uniqueUpToIso TopCat.isInitialPEmpty