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.

@[reducible, inline]

abbrev CategoryTheory.Enriched.eCoyoneda (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : C) : Functor C V

enriched coyoneda functor (X ⟶[V] _) : C ⥤ V.

Equations

• CategoryTheory.Enriched.eCoyoneda V X = (CategoryTheory.eHomFunctor V C).obj (Opposite.op X)

structure CategoryTheory.Enriched.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} (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.

noncomputable def CategoryTheory.Enriched.IsConicalLimit.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} {r₁ r₂ : Limits.Cone F} (h : IsConicalLimit V r₁) (i : r₁ ≅ r₂) : IsConicalLimit V r₂

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

The canonical comparison map with the limit in V.

Equations

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

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} (X : C) [Limits.HasLimitsOfShape J V] (h : IsConicalLimit V c) [Limits.HasLimit (F.comp (eCoyoneda V X))] : limitComparison V c X = ((h.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} (X : C) [Limits.HasLimitsOfShape J V] (h : IsConicalLimit V 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} (X : C) [Limits.HasLimitsOfShape J V] (h : IsConicalLimit V 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

• CategoryTheory.Enriched.IsConicalLimit.limitComparisonIso X h = 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.

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

ConicalLimitCone V F contains a cone over F together with the information that it is a conical limit.

• cone : Limits.Cone F

  The cone itself

• isConicalLimit : IsConicalLimit V self.cone

  The proof that is the limit cone