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
🔸 coverage
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.

Instances For
    source
    🔸 coverage
    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.

    Instances For
      source
      🔸 coverage
      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.

      Instances For
        source
        🔸 coverage
        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.

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