Documentation

InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Limits.IsConicalTerminal

Conical terminal objects in enriched ordinary categories #

An object T in an enriched ordinary category C is a conical terminal object if the empty cone with summit T is a conical limit cone. By IsConicalTerminal.isTerminal this implies that T is a terminal object in the underlying ordinary category of C. When the ambient enriching category V has a terminal object, this provides a natural family of isomorphisms:

IsConicalTerminal.eHomIso {T : C} (hT : IsConicalTerminal V T) (X : C) : (X ⟶[V] T) ≅ ⊤_ V

In general the universal property of being terminal is weaker than the universal property of being conical terminal, but if HasConicalTerminal V C any terminal object in C is conical terminal:

terminalIsConicalTerminal {T : C} (hT : IsTerminal T) : IsConicalTerminal V T .

TODO: Develop similar API for other conical limit and colimit shapes.

source
@[reducible, inline]
abbrev CategoryTheory.Enriched.IsConicalTerminal (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (T : C) :
Type (max (max (max (max u u') 0) v) v')

X is conical terminal if the cone it induces on the empty diagram is a conical limit cone.

Equations
Instances For
    source
    def CategoryTheory.Enriched.IsConicalTerminal.isTerminal (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {T : C} (hT : IsConicalTerminal V T) :
    Limits.IsTerminal T

    A conical terminal object is also terminal.

    Equations
    Instances For
      source
      noncomputable def CategoryTheory.Enriched.IsConicalTerminal.eHomIso (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] [Limits.HasTerminal V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {T : C} (hT : IsConicalTerminal V T) (X : C) :
      EnrichedCategory.Hom X T ≅ ⊤_ V

      The defining universal property of a conical terminal object gives an isomorphism of homs.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def CategoryTheory.Enriched.IsConicalTerminal.ofIso {V : Type u'} [Category.{v', u'} V] [MonoidalCategory V] {C : Type u} [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {Y Z : C} (hY : IsConicalTerminal V Y) (i : Y ≅ Z) :
        IsConicalTerminal V Z

        Transport a term of type IsConicalTerminal across an isomorphism.

        Equations
        Instances For