Theorems · Definition · category theory

CategoryTheory.ForgetEnrichment

(W : Type v) →
  [inst : CategoryTheory.Category.{w, v} W] →
    [inst_1 : CategoryTheory.MonoidalCategory W] → (C : Type u₁) → [CategoryTheory.EnrichedCategory W C] → Type u₁

A type synonym for C, which should come equipped with a V-enriched category structure. In a moment we will equip this with the (honest) category structure so that X ⟶ Y is (𝟙_ W) ⟶ (X ⟶[W] Y). We obtain this category by transporting the enrichment in V along the lax monoidal functor coyonedaTensorUnit, then using the equivalence of Type-enriched categories with honest categories. This is sometimes called the "underlying" category of an enriched category, although some care is needed as the functor coyonedaTensorUnit, which always exists, does not necessarily coincide with "the forgetful functor" from V to Type, if such exists. When V is any of Type, Top, AddCommGroup, or Module R, coyonedaTensorUnit is just the usual forgetful functor, however. For V = Algebra R, the usual forgetful functor is coyoneda of R[X], not of R. (Perhaps we should have a typeclass for this situation: ConcreteMonoidal?)

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

50 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.EnrichedCategory