Existence of conical limits

This file contains different statements about the (non-constructive) existence of conical limits.

The main constructions are the following.

• HasConicalLimit: there exists a conical limit for F : J ⥤ C.
• HasConicalLimitsOfShape J: All functors F : J ⥤ C have conical limits.
• HasConicalLimitsOfSize.{v₁, u₁}: For all small J all functors F : J ⥤ C have conical limits.
• HasConicalLimits : C has all (small) conical limits.

References

• Kelly G.M., Basic concepts of enriched category theory: See section 3.8 for a similar treatment, although the content of this file is not directly adapted from there.

Implementation notes

V has been made an (V : outParam <| Type u') in the classes below as it seems instance inference prefers this. Otherwise it failed with cannot find synthesization order on the instances below. However, it is not fully clear yet whether this could lead to potential issues, for example if there are multiple MonoidalCategory _ instances in scope.

class CategoryTheory.Enriched.HasConicalLimit {J : Type u₁} [Category.{v₁, u₁} J] (V : outParam (Type u')) [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (F : Functor J C) extends CategoryTheory.Limits.HasLimit F : Prop

HasConicalLimit F represents the mere existence of a conical limit for F.

• exists_limit : Nonempty (LimitCone F)
• preservesLimit_eCoyoneda (X : C) : Limits.PreservesLimit F (eCoyoneda V X)

class CategoryTheory.Enriched.HasConicalLimitsOfShape (J : Type u₁) [Category.{v₁, u₁} J] (V : outParam (Type u')) [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] : Prop

C has conical limits of shape J if there exists a conical limit for every functor F : J ⥤ C.

• hasConicalLimit (F : Functor J C) : HasConicalLimit V F

  All functors F : J ⥤ C from J have limits.

class CategoryTheory.Enriched.HasConicalLimitsOfSize (V : outParam (Type u')) [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] : Prop

C has all conical limits of size v₁ u₁ (HasLimitsOfSize.{v₁ u₁} C) if it has conical limits of every shape J : Type u₁ with [Category.{v₁} J].

• hasConicalLimitsOfShape (J : Type u₁) [Category.{v₁, u₁} J] : HasConicalLimitsOfShape J V C

  All functors F : J ⥤ C from all small J have conical limits

@[reducible, inline]

abbrev CategoryTheory.Enriched.HasConicalLimits (V : outParam (Type u')) [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] : Prop

C has all (small) conical limits if it has limits of every shape that is as big as its hom-sets.

Equations

• CategoryTheory.Enriched.HasConicalLimits V C = CategoryTheory.Enriched.HasConicalLimitsOfSize.{?u.50, ?u.50, ?u.51, ?u.50, ?u.49, ?u.48} V C

theorem CategoryTheory.Enriched.HasConicalLimit.of_iso {J : Type u₁} [Category.{v₁, u₁} J] (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {F G : Functor J C} [HasConicalLimit V F] (e : F ≅ G) : HasConicalLimit V G

If a functor F has a conical limit, so does any naturally isomorphic functor.

instance CategoryTheory.Enriched.HasConicalLimit.of_equiv {J : Type u₁} [Category.{v₁, u₁} J] {J' : Type u₂} [Category.{v₂, u₂} J'] (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (F : Functor J C) [HasConicalLimit V F] (G : Functor J' J) [G.IsEquivalence] : HasConicalLimit V (G.comp F)

theorem CategoryTheory.Enriched.HasConicalLimit.of_equiv_comp {J : Type u₁} [Category.{v₁, u₁} J] {J' : Type u₂} [Category.{v₂, u₂} J'] (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (F : Functor J C) (G : Functor J' J) [G.IsEquivalence] [HasConicalLimit V (G.comp F)] : HasConicalLimit V F

If a G ⋙ F has a limit, and G is an equivalence, we can construct a limit of F.

instance CategoryTheory.Enriched.HasConicalLimitsOfShape.hasLimitsOfShape (J : Type u₁) [Category.{v₁, u₁} J] (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalLimitsOfShape J V C] : Limits.HasLimitsOfShape J C

existence of conical limits (of shape) implies existence of limits (of shape)

theorem CategoryTheory.Enriched.HasConicalLimitsOfShape.of_equiv {J : Type u₁} [Category.{v₁, u₁} J] {J' : Type u₂} [Category.{v₂, u₂} J'] (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalLimitsOfShape J' V C] (G : Functor J' J) [G.IsEquivalence] : HasConicalLimitsOfShape J V C

We can transport conical limits of shape J' along an equivalence J' ≌ J.

instance CategoryTheory.Enriched.HasConicalLimitsOfSize.hasLimitsOfSize (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalLimitsOfSize.{v₁, u₁, v', v, u, u'} V C] : Limits.HasLimitsOfSize.{v₁, u₁, v, u} C

existence of conical limits (of size) implies existence of limits (of size)