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

Equations

• TopCat.conePtOfConeForget c = c.pt

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)

Equations

• TopCat.topologicalSpaceConePtOfConeForget c = ⨅ (j : J), TopologicalSpace.induced (c.π.app j) (F.obj j).str

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.

Equations

• TopCat.coneOfConeForget c = { pt := TopCat.of (TopCat.conePtOfConeForget c), π := { app := fun (j : J) => TopCat.ofHom { toFun := c.π.app j, continuous_toFun := ⋯ }, naturality := ⋯ } }

@[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)

@[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 := ⋯ }

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.

Equations

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

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

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 supremum 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 supremum 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 supremum 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 supremum 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 [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.

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