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.
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.
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.
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
Instances For
Equations
- TopCat.topologicalSpaceConePtOfConeForget c = ⨅ (j : J), TopologicalSpace.induced (c.π.app j) (F.obj j).str
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 := ⋯ } }
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.
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
Instances For
Equations
- TopCat.topologicalSpaceCoconePtOfCoconeForget c = ⨆ (j : J), TopologicalSpace.coinduced (c.ι.app j) (F.obj j).str
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 := ⋯ } }
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.
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
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.