Documentation

Mathlib.CategoryTheory.Limits.Unit

Discrete PUnit has limits and colimits #

Mostly for the sake of constructing trivial examples, we show all (co)cones into Discrete PUnit are (co)limit (co)cones. We also show that such (co)cones exist, and that Discrete PUnit has all (co)limits.

source
def CategoryTheory.Limits.punitCone {J : Type v} [Category.{v', v} J] {F : Functor J (Discrete PUnit.{u_1 + 1})} :
Cone F

A trivial cone for a functor into PUnit. punitConeIsLimit shows it is a limit.

Equations
    Instances For
      source
      def CategoryTheory.Limits.punitCocone {J : Type v} [Category.{v', v} J] {F : Functor J (Discrete PUnit.{u_1 + 1})} :
      Cocone F

      A trivial cocone for a functor into PUnit. punitCoconeIsLimit shows it is a colimit.

      Equations
        Instances For
          source
          def CategoryTheory.Limits.punitConeIsLimit {J : Type v} [Category.{v', v} J] {F : Functor J (Discrete PUnit.{u_1 + 1})} {c : Cone F} :
          IsLimit c

          Any cone over a functor into PUnit is a limit cone.

          Equations
            Instances For
              source
              def CategoryTheory.Limits.punitCoconeIsColimit {J : Type v} [Category.{v', v} J] {F : Functor J (Discrete PUnit.{u_1 + 1})} {c : Cocone F} :
              IsColimit c

              Any cocone over a functor into PUnit is a colimit cocone.

              Equations
                Instances For
                  source
                  instance CategoryTheory.Limits.instHasLimitsOfSizeDiscretePUnit :
                  HasLimitsOfSize.{v', v, u_1, u_1} (Discrete PUnit.{u_1 + 1})
                  source
                  instance CategoryTheory.Limits.instHasColimitsOfSizeDiscretePUnit :
                  HasColimitsOfSize.{v', v, u_1, u_1} (Discrete PUnit.{u_1 + 1})