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.

source

def TopCat.limitCone {J : Type v} [CategoryTheory.SmallCategory 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.

Instances For

source

def TopCat.limitConeInfi {J : Type v} [CategoryTheory.SmallCategory 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.

Instances For

source

def TopCat.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) :

CategoryTheory.Limits.IsLimit (TopCat.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.

Instances For

source

def TopCat.limitConeInfiIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) :

CategoryTheory.Limits.IsLimit (TopCat.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.

Instances For

source

instance TopCat.topCat_hasLimitsOfSize :

CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} TopCat

source

instance TopCat.topCat_hasLimits :

CategoryTheory.Limits.HasLimits TopCat

source

instance TopCat.forget_preservesLimitsOfSize :

CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget TopCat)

source

instance TopCat.forget_preservesLimits :

CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget TopCat)

source

def TopCat.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) :

CategoryTheory.Limits.Cocone F

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

Equations

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

Instances For

source

def TopCat.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) :

CategoryTheory.Limits.IsColimit (TopCat.colimitCocone F)

The chosen cocone TopCat.colimitCocone F for a functor F : J ⥤ TopCat is a colimit cocone. Generally you should just use colimit.isColimit F, unless you need the actual definition (which is in terms of Types.colimitCoconeIsColimit).

Equations