Documentation

Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Enriched ordinary categories #

If V is a monoidal category, a V-enriched category C does not need to be a category. However, when we have both Category C and EnrichedCategory V C, we may require that the type of morphisms X āŸ¶ Y in C identify to šŸ™_ V āŸ¶ EnrichedCategory.Hom X Y. This data shall be packaged in the typeclass EnrichedOrdinaryCategory V C.

In particular, if C is a V-enriched category, it is shown that the "underlying" category ForgetEnrichment V C is equipped with a EnrichedOrdinaryCategory V C instance.

Simplicial categories are implemented in AlgebraicTopology.SimplicialCategory.Basic using an abbreviation for EnrichedOrdinaryCategory SSet C.

An enriched ordinary category is a category C that is also enriched over a category V in such a way that morphisms X āŸ¶ Y in C identify to morphisms šŸ™_ V āŸ¶ (X āŸ¶[V] Y) in V.

Instances

    The bijection (X āŸ¶ Y) ā‰ƒ (šŸ™_ V āŸ¶ (X āŸ¶[V] Y)) given by a EnrichedOrdinaryCategory instance.

    Equations
    Instances For

      The morphism (X' āŸ¶[V] Y) āŸ¶ (X āŸ¶[V] Y) induced by a morphism X āŸ¶ X'.

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

        Whiskering commutes with the enriched composition.

        The morphism (X āŸ¶[V] Y) āŸ¶ (X āŸ¶[V] Y') induced by a morphism Y āŸ¶ Y'.

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

          Whiskering commutes with the enriched composition.

          Given an isomorphism Ī± : Y ā‰… Yā‚ in C, the enriched composition map eComp V X Y Z : (X āŸ¶[V] Y) āŠ— (Y āŸ¶[V] Z) āŸ¶ (X āŸ¶[V] Z) factors through the V object (X āŸ¶[V] Yā‚) āŠ— (Yā‚ āŸ¶[V] Z) via the map defined by whiskering in the middle with Ī±.hom and Ī±.inv.

          The bifunctor Cįµ’įµ– ā„¤ C ā„¤ V which sends X : Cįµ’įµ– and Y : C to X āŸ¶[V] Y.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.eHomFunctor_map_app (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] {Xāœ Yāœ : Cįµ’įµ–} (Ļ† : Xāœ āŸ¶ Yāœ) (Y : C) :
            ((eHomFunctor V C).map Ļ†).app Y = eHomWhiskerRight V Ļ†.unop Y
            @[simp]
            theorem CategoryTheory.eHomFunctor_obj_map (V : Type u') [Category.{v', u'} V] [MonoidalCategory V] (C : Type u) [Category.{v, u} C] [EnrichedOrdinaryCategory V C] (X : Cįµ’įµ–) {Xāœ Yāœ : C} (Ļ† : Xāœ āŸ¶ Yāœ) :
            ((eHomFunctor V C).obj X).map Ļ† = eHomWhiskerLeft V (Opposite.unop X) Ļ†
            @[reducible, inline]

            enriched coyoneda functor (X āŸ¶[V] _) : C ā„¤ V.

            Equations
            Instances For