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