Documentation

Mathlib.Topology.Category.TopCat.Limits.Basic

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
          Equations
          source
          instance TopCat.topCat_hasLimits :
          CategoryTheory.Limits.HasLimits TopCat
          Equations
          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)
          Equations
          source
          instance TopCat.forget_preservesLimits :
          CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget TopCat)
          Equations
          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
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance TopCat.topCat_hasColimitsOfSize :
              CategoryTheory.Limits.HasColimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} TopCat
              Equations
              source
              instance TopCat.topCat_hasColimits :
              CategoryTheory.Limits.HasColimits TopCat
              Equations
              source
              instance TopCat.forget_preservesColimitsOfSize :
              CategoryTheory.Limits.PreservesColimitsOfSize.{v, v, max u v, max u v, max (u + 1) (v + 1), max (u + 1) (v + 1)} (CategoryTheory.forget TopCat)
              Equations
              source
              instance TopCat.forget_preservesColimits :
              CategoryTheory.Limits.PreservesColimits (CategoryTheory.forget TopCat)
              Equations
              source
              def TopCat.isTerminalPUnit :
              CategoryTheory.Limits.IsTerminal (TopCat.of PUnit.{u + 1} )

              The terminal object of Top is PUnit.

              Equations
              Instances For
                source
                def TopCat.terminalIsoPUnit :
                ⊤_ TopCat ≅ TopCat.of PUnit.{u + 1}

                The terminal object of Top is PUnit.

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

                  The initial object of Top is PEmpty.

                  Equations
                  Instances For
                    source
                    def TopCat.initialIsoPEmpty :
                    ⊥_ TopCat ≅ TopCat.of PEmpty.{u + 1}

                    The initial object of Top is PEmpty.

                    Equations
                    Instances For