discrete punit
has limits and colimits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
def
category_theory.limits.punit_cone
{J : Type v}
[category_theory.category J]
{F : J ⥤ category_theory.discrete punit} :
A trivial cone for a functor into punit
. punit_cone_is_limit
shows it is a limit.
def
category_theory.limits.punit_cocone
{J : Type v}
[category_theory.category J]
{F : J ⥤ category_theory.discrete punit} :
A trivial cocone for a functor into punit
. punit_cocone_is_limit
shows it is a colimit.
def
category_theory.limits.punit_cone_is_limit
{J : Type v}
[category_theory.category J]
{F : J ⥤ category_theory.discrete punit}
{c : category_theory.limits.cone F} :
Any cone over a functor into punit
is a limit cone.
def
category_theory.limits.punit_cocone_is_colimit
{J : Type v}
[category_theory.category J]
{F : J ⥤ category_theory.discrete punit}
{c : category_theory.limits.cocone F} :
Any cocone over a functor into punit
is a colimit cocone.