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.

@[inline, reducible]

abbrev TopCatMax : Type ((max u v) + 1)

Universe inequalities in Mathlib 3 are expressed through use of max u v. Unfortunately, this leads to unbound universes which cannot be solved for during unification, eg max u v =?= max v ?. The current solution is to wrap Type max u v in TypeMax.{u,v} to expose both universe parameters directly.

Similarly, for other concrete categories for which we need to refer to the maximum of two universes (e.g. any category for which we are constructing limits), we need an analogous abbreviation.

Equations

• TopCatMax = TopCat

def TopCat.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) : 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.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) : 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.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) : 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.

def TopCat.limitConeInfiIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) : 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.

instance TopCat.topCat_hasLimitsOfSize : CategoryTheory.Limits.HasLimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} TopCatMax

Equations

• TopCat.topCat_hasLimitsOfSize = ⋯

instance TopCat.topCat_hasLimits : CategoryTheory.Limits.HasLimits TopCat

Equations

• TopCat.topCat_hasLimits = TopCat.topCat_hasLimitsOfSize

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

Equations

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

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

Equations

• TopCat.forgetPreservesLimits = TopCat.forgetPreservesLimitsOfSize

def TopCat.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) : 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.

def TopCat.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) : 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

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

instance TopCat.topCat_hasColimitsOfSize : CategoryTheory.Limits.HasColimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} TopCatMax

Equations

• TopCat.topCat_hasColimitsOfSize = ⋯

instance TopCat.topCat_hasColimits : CategoryTheory.Limits.HasColimits TopCat

Equations

• TopCat.topCat_hasColimits = TopCat.topCat_hasColimitsOfSize

instance TopCat.forgetPreservesColimitsOfSize : CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, max v u_1, max v u_1, (max v u_1) + 1, (max v u_1) + 1} (CategoryTheory.forget TopCat)

Equations

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

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

Equations

• TopCat.forgetPreservesColimits = TopCat.forgetPreservesColimitsOfSize

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

The terminal object of Top is PUnit.

Equations

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

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

The terminal object of Top is PUnit.

Equations

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

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

The initial object of Top is PEmpty.

Equations

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

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

The initial object of Top is PEmpty.

Equations

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