structure CategoryTheory.Enriched.ConicalLimitCone {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) : Type (max (max (max (max u u') u₁) v) v')

Mirrors LimitCone F.

• limitCone : Limits.LimitCone F
• isConicalLimit (X : C) : Limits.IsLimit ((eCoyoneda V X).mapCone self.limitCone.cone)

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 = { limitCone := CategoryTheory.Limits.getLimitCone F, isConicalLimit := fun (X : C) => 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).limitCone.cone.pt

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).limitCone.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

theorem CategoryTheory.Enriched.HasConicalLimitsOfSize.of_univLE (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] [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}] : 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

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