Theorems · Definition · category theory

CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv

{V : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {W : Type u''} →
        [inst_2 : CategoryTheory.Category.{v'', u''} W] →
          [inst_3 : CategoryTheory.MonoidalCategory W] →
            (F : CategoryTheory.Functor V W) →
              [inst_4 : F.LaxMonoidal] →
                (D : Type u) →
                  [inst_5 : CategoryTheory.EnrichedCategory V D] →
                    (e :
                        (v : V) →
                          (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) →
                      (∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
                          (e v) f =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) →
                        (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D) ≌
                          CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D))

If D is a V-enriched category, then forgetting the enrichment and transporting the resulting enriched ordinary category along a functor F : V ⥤ W, for which f ↦ Functor.LaxMonoidal.ε F ≫ F.map f has an inverse, results in a category equivalent to transporting along F and then forgetting about the resulting W-enrichment.

Defined in

Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Cited by

4 results in Mathlib

Foundations

Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Functor.LaxMonoidalCategoryTheory.EnrichedCategory