HasConicalLimits

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

The main constructions are the following.

• HasConicalLimit: there exists a limit cone with IsConicalLimit V cone
• 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 : has all (small) conical limits.

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) : Prop

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

• mk' :: (
• exists_conicalLimitCone : Nonempty (ConicalLimitCone V F)

  There is some limit cone for F

• )

theorem CategoryTheory.Enriched.HasConicalLimit.mk {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} (d : ConicalLimitCone V F) : HasConicalLimit V F

noncomputable def CategoryTheory.Enriched.HasConicalLimit.getConicalLimitCone {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] : ConicalLimitCone V F

Use the axiom of choice to extract explicit ConicalLimitCone F from HasConicalLimit F.

Equations

• CategoryTheory.Enriched.HasConicalLimit.getConicalLimitCone V F = Classical.choice ⋯

noncomputable def CategoryTheory.Enriched.HasConicalLimit.conicalLimitCone {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] : ConicalLimitCone V F

An arbitrary choice of conical limit cone for a functor.

Equations

• CategoryTheory.Enriched.HasConicalLimit.conicalLimitCone V F = CategoryTheory.Enriched.HasConicalLimit.getConicalLimitCone V F

noncomputable def CategoryTheory.Enriched.HasConicalLimit.conicalLimit {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] : C

An arbitrary choice of conical limit object of a functor.

Equations

• CategoryTheory.Enriched.HasConicalLimit.conicalLimit V F = (CategoryTheory.Enriched.HasConicalLimit.conicalLimitCone V F).cone.pt

instance CategoryTheory.Enriched.HasConicalLimit.hasLimit {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] : Limits.HasLimit F

noncomputable def CategoryTheory.Enriched.HasConicalLimit.conicalLimit.π {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] (j : J) : conicalLimit V F ⟶ F.obj j

The projection from the conical limit object to a value of the functor.

Equations

• CategoryTheory.Enriched.HasConicalLimit.conicalLimit.π V F j = (CategoryTheory.Enriched.HasConicalLimit.conicalLimitCone V F).cone.π.app j

@[simp]

theorem CategoryTheory.Enriched.HasConicalLimit.conicalLimit.w {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] {j j' : J} (f : j ⟶ j') : CategoryStruct.comp (conicalLimit.π V F j) (F.map f) = conicalLimit.π V F j'

@[simp]

theorem CategoryTheory.Enriched.HasConicalLimit.conicalLimit.w_assoc {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] {j j' : J} (f : j ⟶ j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryStruct.comp (conicalLimit.π V F j) (CategoryStruct.comp (F.map f) h) = CategoryStruct.comp (conicalLimit.π V F j') h

noncomputable def CategoryTheory.Enriched.HasConicalLimit.conicalLimit.isConicalLimit {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] : IsConicalLimit V (conicalLimitCone V F).cone

Evidence that the arbitrary choice of cone provided by (conicalLimitCone V F).cone is a conical limit cone.

Equations

• CategoryTheory.Enriched.HasConicalLimit.conicalLimit.isConicalLimit V F = (CategoryTheory.Enriched.HasConicalLimit.getConicalLimitCone V F).isConicalLimit

noncomputable def CategoryTheory.Enriched.HasConicalLimit.conicalLimit.lift {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) (c : Limits.Cone F) [HasConicalLimit V F] : c.pt ⟶ conicalLimit V F

The morphism from the cone point of any other cone to the limit object.

Equations

• CategoryTheory.Enriched.HasConicalLimit.conicalLimit.lift V F c = (CategoryTheory.Enriched.HasConicalLimit.conicalLimit.isConicalLimit V F).isLimit.lift c

@[simp]

theorem CategoryTheory.Enriched.HasConicalLimit.conicalLimit.lift_π {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) (c : Limits.Cone F) [HasConicalLimit V F] (j : J) : CategoryStruct.comp (lift V F c) (conicalLimit.π V F j) = c.π.app j

@[simp]

theorem CategoryTheory.Enriched.HasConicalLimit.conicalLimit.lift_π_assoc {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) (c : Limits.Cone F) [HasConicalLimit V F] (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (lift V F c) (CategoryStruct.comp (conicalLimit.π V F j) h) = CategoryStruct.comp (c.π.app j) h

theorem CategoryTheory.Enriched.HasConicalLimit.ofIso {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 C} (α : F ≅ G) : HasConicalLimit V G

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

instance CategoryTheory.Enriched.HasConicalLimit.hasConicalLimitEquivalenceComp {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (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] (e : K ≌ J) : HasConicalLimit V (e.functor.comp F)

theorem CategoryTheory.Enriched.HasConicalLimit.hasConicalLimitOfEquivalenceComp {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (F : Functor J C) (e : K ≌ J) [HasConicalLimit V (e.functor.comp F)] : HasConicalLimit V F

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

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.

@[instance 100]

instance CategoryTheory.Enriched.HasConicalLimitsOfShape.instHasConicalLimit {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) [HasConicalLimitsOfShape J V C] : HasConicalLimit V F

instance CategoryTheory.Enriched.HasConicalLimitsOfShape.instHasLimitsOfShape {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

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

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

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

@[instance 100]

instance CategoryTheory.Enriched.HasConicalLimitsOfSize.instHasConicalLimitsOfShape {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] [HasConicalLimitsOfSize.{v₁, u₁, v', v, u, u'} V C] : HasConicalLimitsOfShape J V C

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

theorem CategoryTheory.Enriched.HasConicalLimitsOfSize.hasConicalLimitsOfSize_of_univLE (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}] [h : HasConicalLimitsOfSize.{v₁, u₁, v', v, u, u'} V C] : HasConicalLimitsOfSize.{v₂, u₂, v', v, u, u'} V C

A category that has larger conical limits also has smaller conical limits.

theorem CategoryTheory.Enriched.HasConicalLimitsOfSize.shrink (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalLimitsOfSize.{max v₁ v₂, max u₁ u₂, v', v, u, u'} V C] : HasConicalLimitsOfSize.{v₁, u₁, v', v, u, u'} V C

HasConicalLimitsOfSize.shrink.{v, u} C tries to obtain HasConicalLimitsOfSize.{v, u} C from some other HasConicalLimitsOfSize.{v₁, u₁} C.

@[reducible, inline]

abbrev CategoryTheory.Enriched.HasConicalLimits (V : 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.44, ?u.44, ?u.45, ?u.44, ?u.43, ?u.42} V C

@[instance 100]

instance CategoryTheory.Enriched.HasConicalLimits.hasSmallestConicalLimitsOfHasConicalLimits (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalLimits V C] : HasConicalLimitsOfSize.{0, 0, v', v, u, u'} V C

instance CategoryTheory.Enriched.HasConicalLimits.instHasConicalLimitsOfShape (J : Type v) [Category.{v, v} J] (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] [HasConicalLimits V C] : HasConicalLimitsOfShape J V C