Documentation

Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D #

When D is a monoidal category, monoid objects in C ⥤ D are the same thing as functors from C into the monoid objects of D.

This is formalised as:

The intended application is that as Ring ≌ Mon_ Ab (not yet constructed!), we have presheaf Ring X ≌ presheaf (Mon_ Ab) X ≌ Mon_ (presheaf Ab X), and we can model a module over a presheaf of rings as a module object in presheaf Ab X.

Future work #

Presumably this statement is not specific to monoids, and could be generalised to any internal algebraic objects, if the appropriate framework was available.

source
def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Mon_ (CategoryTheory.Functor C D)) :
CategoryTheory.Functor C (Mon_ D)

A monoid object in a functor category induces a functor to the category of monoid objects.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_obj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Mon_ (CategoryTheory.Functor C D)) (X : C) :
    ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).obj X).one = A.one.app X
    source
    @[simp]
    theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_obj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Mon_ (CategoryTheory.Functor C D)) (X : C) :
    ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).obj X).X = A.X.obj X
    source
    @[simp]
    theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Mon_ (CategoryTheory.Functor C D)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
    ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).map f).hom = A.X.map f
    source
    @[simp]
    theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_obj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Mon_ (CategoryTheory.Functor C D)) (X : C) :
    ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).obj X).mul = A.mul.app X
    source
    def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
    CategoryTheory.Functor (Mon_ (CategoryTheory.Functor C D)) (CategoryTheory.Functor C (Mon_ D))

    Functor translating a monoid object in a functor category to a functor into the category of monoid objects.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Mon_ (CategoryTheory.Functor C D)) :
      CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.obj A = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A
      source
      @[simp]
      theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X✝ Y✝ : Mon_ (CategoryTheory.Functor C D)} (f : X✝ ⟶ Y✝) (X : C) :
      ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.map f).app X).hom = f.hom.app X
      source
      def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Mon_ D)) :
      Mon_ (CategoryTheory.Functor C D)

      A functor to the category of monoid objects can be translated as a monoid object in the functor category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Mon_ D)) :
        (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).X = F.comp (Mon_.forget D)
        source
        @[simp]
        theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_one_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Mon_ D)) (X : C) :
        (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).one.app X = (F.obj X).one
        source
        @[simp]
        theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mul_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Mon_ D)) (X : C) :
        (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).mul.app X = (F.obj X).mul
        source
        def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
        CategoryTheory.Functor (CategoryTheory.Functor C (Mon_ D)) (Mon_ (CategoryTheory.Functor C D))

        Functor translating a functor into the category of monoid objects to a monoid object in the functor category

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Mon_ D)) :
          CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.obj F = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F
          source
          @[simp]
          theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X✝ Y✝ : CategoryTheory.Functor C (Mon_ D)} (α : X✝ ⟶ Y✝) (X : C) :
          (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.map α).hom.app X = (α.app X).hom
          source
          def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
          CategoryTheory.Functor.id (Mon_ (CategoryTheory.Functor C D)) ≅ CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.comp CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse

          The unit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (X : Mon_ (CategoryTheory.Functor C D)) (x✝ : C) :
            (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso.inv.app X).hom.app x✝ = CategoryTheory.CategoryStruct.id (X.X.obj x✝)
            source
            @[simp]
            theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (X : Mon_ (CategoryTheory.Functor C D)) (x✝ : C) :
            (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso.hom.app X).hom.app x✝ = CategoryTheory.CategoryStruct.id (X.X.obj x✝)
            source
            def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
            CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.comp CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor ≅ CategoryTheory.Functor.id (CategoryTheory.Functor C (Mon_ D))

            The counit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Functor C (Mon_ D)) (X✝ : C) :
              ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso.hom.app X).app X✝).hom = CategoryTheory.CategoryStruct.id (X.obj X✝).X
              source
              @[simp]
              theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Functor C (Mon_ D)) (X✝ : C) :
              ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso.inv.app X).app X✝).hom = CategoryTheory.CategoryStruct.id (X.obj X✝).X
              source
              def CategoryTheory.Monoidal.monFunctorCategoryEquivalence (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
              Mon_ (CategoryTheory.Functor C D) ≌ CategoryTheory.Functor C (Mon_ D)

              When D is a monoidal category, monoid objects in C ⥤ D are the same thing as functors from C into the monoid objects of D.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                (CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).counitIso = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso
                source
                @[simp]
                theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                (CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).inverse = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse
                source
                @[simp]
                theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                (CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).unitIso = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso
                source
                @[simp]
                theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                (CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).functor = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor
                source
                def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Comon_ (CategoryTheory.Functor C D)) :
                CategoryTheory.Functor C (Comon_ D)

                A comonoid object in a functor category induces a functor to the category of comonoid objects.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Comon_ (CategoryTheory.Functor C D)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                  ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).map f).hom = A.X.map f
                  source
                  @[simp]
                  theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Comon_ (CategoryTheory.Functor C D)) (X : C) :
                  ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).obj X).X = A.X.obj X
                  source
                  @[simp]
                  theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Comon_ (CategoryTheory.Functor C D)) (X : C) :
                  ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).obj X).comul = A.comul.app X
                  source
                  @[simp]
                  theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Comon_ (CategoryTheory.Functor C D)) (X : C) :
                  ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).obj X).counit = A.counit.app X
                  source
                  def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                  CategoryTheory.Functor (Comon_ (CategoryTheory.Functor C D)) (CategoryTheory.Functor C (Comon_ D))

                  Functor translating a comonoid object in a functor category to a functor into the category of comonoid objects.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (A : Comon_ (CategoryTheory.Functor C D)) :
                    CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor.obj A = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A
                    source
                    @[simp]
                    theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X✝ Y✝ : Comon_ (CategoryTheory.Functor C D)} (f : X✝ ⟶ Y✝) (X : C) :
                    ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor.map f).app X).hom = f.hom.app X
                    source
                    def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Comon_ D)) :
                    Comon_ (CategoryTheory.Functor C D)

                    A functor to the category of comonoid objects can be translated as a comonoid object in the functor category.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Comon_ D)) :
                      (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F).X = F.comp (Comon_.forget D)
                      source
                      @[simp]
                      theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comul_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Comon_ D)) (X : C) :
                      (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F).comul.app X = (F.obj X).comul
                      source
                      @[simp]
                      theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_counit_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C (Comon_ D)) (X : C) :
                      (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F).counit.app X = (F.obj X).counit
                      source
                      def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                      CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝.comp CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor ≅ CategoryTheory.Functor.id (CategoryTheory.Functor C (Comon_ D))

                      The counit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Functor C (Comon_ D)) (X✝ : C) :
                        ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso.hom.app X).app X✝).hom = CategoryTheory.CategoryStruct.id (X.obj X✝).X
                        source
                        @[simp]
                        theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Functor C (Comon_ D)) (X✝ : C) :
                        ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso.inv.app X).app X✝).hom = CategoryTheory.CategoryStruct.id (X.obj X✝).X
                        source
                        def CategoryTheory.Monoidal.comonFunctorCategoryEquivalence (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                        Comon_ (CategoryTheory.Functor C D) ≌ CategoryTheory.Functor C (Comon_ D)

                        When D is a monoidal category, comonoid objects in C ⥤ D are the same thing as functors from C into the comonoid objects of D.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                          (CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).functor = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor
                          source
                          @[simp]
                          theorem CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                          (CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).inverse = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝
                          source
                          @[simp]
                          theorem CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                          (CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).unitIso = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso✝
                          source
                          @[simp]
                          theorem CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
                          (CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).counitIso = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso
                          source
                          def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                          CategoryTheory.Functor (CommMon_ (CategoryTheory.Functor C D)) (CategoryTheory.Functor C (CommMon_ D))

                          Functor translating a commutative monoid object in a functor category to a functor into the category of commutative monoid objects.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : CommMon_ (CategoryTheory.Functor C D)) (X : C) :
                            ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).X = A.X.obj X
                            source
                            @[simp]
                            theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : CommMon_ (CategoryTheory.Functor C D)) (X : C) :
                            ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).mul = A.mul.app X
                            source
                            @[simp]
                            theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {X✝ Y✝ : CommMon_ (CategoryTheory.Functor C D)} (f : X✝ ⟶ Y✝) (X : C) :
                            ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.map f).app X).hom = f.hom.app X
                            source
                            @[simp]
                            theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : CommMon_ (CategoryTheory.Functor C D)) (X : C) :
                            ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).one = A.one.app X
                            source
                            @[simp]
                            theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (A : CommMon_ (CategoryTheory.Functor C D)) {X Y : C} (a✝ : X ⟶ Y) :
                            ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).map a✝).hom = A.X.map a✝
                            source
                            def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                            CategoryTheory.Functor (CategoryTheory.Functor C (CommMon_ D)) (CommMon_ (CategoryTheory.Functor C D))

                            Functor translating a functor into the category of commutative monoid objects to a commutative monoid object in the functor category

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mul_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C (CommMon_ D)) (X : C) :
                              (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).mul.app X = (F.obj X).mul
                              source
                              @[simp]
                              theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C (CommMon_ D)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                              (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).X.map f = (F.map f).hom
                              source
                              @[simp]
                              theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_one_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C (CommMon_ D)) (X : C) :
                              (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).one.app X = (F.obj X).one
                              source
                              @[simp]
                              theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.Functor C (CommMon_ D)) (X : C) :
                              (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).X.obj X = ((CommMon_.forget₂Mon_ D).obj (F.obj X)).X
                              source
                              @[simp]
                              theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {X✝ Y✝ : CategoryTheory.Functor C (CommMon_ D)} (α : X✝ ⟶ Y✝) (X : C) :
                              (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.map α).hom.app X = (α.app X).hom
                              source
                              def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                              CategoryTheory.Functor.id (CommMon_ (CategoryTheory.Functor C D)) ≅ CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.comp CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse

                              The unit for the equivalence CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[simp]
                                theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (X : CommMon_ (CategoryTheory.Functor C D)) (x✝ : C) :
                                (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso.hom.app X).hom.app x✝ = CategoryTheory.CategoryStruct.id (X.X.obj x✝)
                                source
                                @[simp]
                                theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (X : CommMon_ (CategoryTheory.Functor C D)) (x✝ : C) :
                                (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso.inv.app X).hom.app x✝ = CategoryTheory.CategoryStruct.id ((CommMon_.forget₂Mon_ D).obj ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj X).obj x✝)).X
                                source
                                def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                                CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.comp CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor ≅ CategoryTheory.Functor.id (CategoryTheory.Functor C (CommMon_ D))

                                The counit for the equivalence CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (X : CategoryTheory.Functor C (CommMon_ D)) (X✝ : C) :
                                  ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso.inv.app X).app X✝).hom = CategoryTheory.CategoryStruct.id (X.obj X✝).X
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (X : CategoryTheory.Functor C (CommMon_ D)) (X✝ : C) :
                                  ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso.hom.app X).app X✝).hom = CategoryTheory.CategoryStruct.id ((CommMon_.forget₂Mon_ D).obj (X.obj X✝)).X
                                  source
                                  def CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                                  CommMon_ (CategoryTheory.Functor C D) ≌ CategoryTheory.Functor C (CommMon_ D)

                                  When D is a braided monoidal category, commutative monoid objects in C ⥤ D are the same thing as functors from C into the commutative monoid objects of D.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                                    (CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).unitIso = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_functor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                                    (CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).functor = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                                    (CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).counitIso = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_inverse (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :
                                    (CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).inverse = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse