Theorems · Definition · category theory

CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor

{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.Functor
                          (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))
                          (CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D))

The functor that makes up TransportEnrichment.forgetEnrichmentEquiv.

Defined in

Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

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