Conical limits in enriched ordinary categories

A limit cone in the underlying category of an enriched ordinary category is a conical limit if it is a limit cone in the underlying ordinary category and moreover this limit cone is preserved by covariant enriched representable functors. These conditions are encoded in the structure IsConicalLimit.

The universal property of a conical limit is enriched as follows: the canonical comparison map defines an isomorphism in the enriching category:

limitComparisonIso (h : IsConicalLimit V c) : (X ⟶[V] c.pt) ≅ (limit (F ⋙ eCoyoneda V X))

Conversely, if the canonical maps define isomorphisms for all X then c is a conical limit cone:

ofIsIsoLimitComparison [∀ X, IsIso (IsConicalLimit.limitComparison V c X)] (hc : IsLimit c) : IsConicalLimit V c

This file develops some general API for conical limits in enriched ordinary categories.

TODO: Dualize everything to define conical colimits.

structure CategoryTheory.Enriched.IsConicalLimit {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} (c : Limits.Cone F) : Type (max (max (max (max u u') u₁) v) v')

A limit cone c in a V-enriched ordinary category C is a V-enriched limit (or conical limit) if for every X : C, the cone obtained by applying the coyoneda functor (X ⟶[V] -) to c is a limit cone in V.

• isLimit : Limits.IsLimit c

  A conical limit cone is a limit cone.

• isConicalLimit (X : C) : Limits.IsLimit ((eCoyoneda V X).mapCone c)

  The cone obtained by applying the coyoneda functor (X ⟶[V] -) to c is a limit cone in V.

theorem CategoryTheory.Enriched.IsConicalLimit.hasConicalLimit {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} (hc : IsConicalLimit V c) : HasConicalLimit V F

noncomputable def CategoryTheory.Enriched.IsConicalLimit.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 : Functor J C} {c d : Limits.Cone F} (hc : IsConicalLimit V c) (i : c ≅ d) : IsConicalLimit V d

Transport evidence that a cone is a V-enriched limit cone across an isomorphism of cones.

Equations

• One or more equations did not get rendered due to their size.

Characterization in terms of the comparison map.

There is a canonical comparison map with the limit in V, the following proves that a limit cone in C is a V-enriched limit if and only if the comparison map is an isomorphism for every X : C.

noncomputable def CategoryTheory.Enriched.IsConicalLimit.limitComparison {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) [Limits.HasLimitsOfShape J V] (X : C) : EnrichedCategory.Hom X c.pt ⟶ Limits.limit (F.comp (eCoyoneda V X))

The canonical comparison map with the limit in V.

Equations

• CategoryTheory.Enriched.IsConicalLimit.limitComparison V c X = CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.eCoyoneda V X)) ((CategoryTheory.eCoyoneda V X).mapCone c)

theorem CategoryTheory.Enriched.IsConicalLimit.limitComparison_eq_conePointUniqueUpToIso {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} [Limits.HasLimitsOfShape J V] (hc : IsConicalLimit V c) (X : C) [Limits.HasLimit (F.comp (eCoyoneda V X))] : limitComparison V c X = ((hc.isConicalLimit X).conePointUniqueUpToIso (Limits.limit.isLimit (F.comp (eCoyoneda V X)))).hom

theorem CategoryTheory.Enriched.IsConicalLimit.isIso_limitComparison {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} [Limits.HasLimitsOfShape J V] (hc : IsConicalLimit V c) (X : C) : IsIso (limitComparison V c X)

IsConicalLimit.limitComparison is an isomorphism.

noncomputable def CategoryTheory.Enriched.IsConicalLimit.limitComparisonIso {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} [Limits.HasLimitsOfShape J V] (hc : IsConicalLimit V c) (X : C) : EnrichedCategory.Hom X c.pt ≅ Limits.limit (F.comp (eCoyoneda V X))

For all X : C, the canonical comparison map with the limit in V as isomorphism

Equations

• hc.limitComparisonIso X = CategoryTheory.asIso (CategoryTheory.Enriched.IsConicalLimit.limitComparison V c X)

noncomputable def CategoryTheory.Enriched.IsConicalLimit.ofIsIsoLimitComparison {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} [Limits.HasLimitsOfShape J V] [∀ (X : C), IsIso (limitComparison V c X)] (hc : Limits.IsLimit c) : IsConicalLimit V c

Reverse direction: if the comparison map is an isomorphism, then c is a conical limit.

Equations

• CategoryTheory.Enriched.IsConicalLimit.ofIsIsoLimitComparison V hc = { isLimit := hc, isConicalLimit := fun (X : C) => let_fun this := ⋯; Classical.choice ⋯ }

theorem CategoryTheory.Enriched.IsConicalLimit.nonempty_isConicalLimit_iff {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} [Limits.HasLimitsOfShape J V] (hc : Limits.IsLimit c) : Nonempty (IsConicalLimit V c) ↔ ∀ (X : C), IsIso (limitComparison V c X)

A limit cone in C is a V-enriched limit if and only if the comparison map is an isomorphism for every X : C. Note: it's easier to use the two directions limitComparisonIso and ofIsIsoLimitComparison directly.

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

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

Equations

• One or more equations did not get rendered due to their size.

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 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 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 c) (CategoryStruct.comp (conicalLimit.π V F j) h) = CategoryStruct.comp (c.π.app j) h