# mathlib3documentation

topology.category.Top.limits.basic

# The category of topological spaces has all limits and colimits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 Top.limit_cone {J : Type v} (F : J Top) :

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

Equations
def Top.limit_cone_infi {J : Type v} (F : J Top) :

A choice of limit cone for a functor F : J ⥤ Top 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.limit_cone).

Equations
def Top.limit_cone_is_limit {J : Type v} (F : J Top) :

The chosen cone Top.limit_cone F for a functor F : J ⥤ Top is a limit cone. Generally you should just use limit.is_limit F, unless you need the actual definition (which is in terms of types.limit_cone_is_limit).

Equations
def Top.limit_cone_infi_is_limit {J : Type v} (F : J Top) :

The chosen cone Top.limit_cone_infi F for a functor F : J ⥤ Top is a limit cone. Generally you should just use limit.is_limit F, unless you need the actual definition (which is in terms of types.limit_cone_is_limit).

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
def Top.colimit_cocone {J : Type v} (F : J Top) :

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

Equations
def Top.colimit_cocone_is_colimit {J : Type v} (F : J Top) :

The chosen cocone Top.colimit_cocone F for a functor F : J ⥤ Top is a colimit cocone. Generally you should just use colimit.is_colimit F, unless you need the actual definition (which is in terms of types.colimit_cocone_is_colimit).

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations

The terminal object of Top is punit.

Equations
noncomputable def Top.terminal_iso_punit  :

The terminal object of Top is punit.

Equations

The initial object of Top is pempty.

Equations
noncomputable def Top.initial_iso_pempty  :

The initial object of Top is pempty.

Equations