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.functorObjObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [MonObj A] (X : C) :
Mon D

A monoid object in a functor category sends any object to a monoid object.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_one {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [MonObj A] (X : C) :
    MonObj.one = MonObj.one.app X
    source
    @[simp]
    theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_X {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [MonObj A] (X : C) :
    (functorObjObj A X).X = A.obj X
    source
    @[simp]
    theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_mul {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [MonObj A] (X : C) :
    MonObj.mul = MonObj.mul.app X
    source
    def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [MonObj A] :
    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_map_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [MonObj A] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
      ((functorObj A).map f).hom = A.map f
      source
      @[simp]
      theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [MonObj A] (X : C) :
      (functorObj A).obj X = functorObjObj A X
      source
      def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] :
      Functor (Mon (Functor C D)) (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_map_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {X✝ Y✝ : Mon (Functor C D)} (f : X✝ ⟶ Y✝) (X : C) :
        ((functor.map f).app X).hom = f.hom.app X
        source
        @[simp]
        theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Mon (Functor C D)) :
        functor.obj A = functorObj A.X
        source
        def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Mon D)) :
        Mon (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_mon_one_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Mon D)) (X : C) :
          MonObj.one.app X = MonObj.one
          source
          @[simp]
          theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Mon D)) (X : C) :
          MonObj.mul.app X = MonObj.mul
          source
          @[simp]
          theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_X {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Mon D)) :
          (inverseObj F).X = F.comp (Mon.forget D)
          source
          def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] :
          Functor (Functor C (Mon D)) (Mon (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Mon D)) :
            inverse.obj F = inverseObj F
            source
            @[simp]
            theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {X✝ Y✝ : Functor C (Mon D)} (α : X✝ ⟶ Y✝) (X : C) :
            (inverse.map α).hom.app X = (α.app X).hom
            source
            def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] :
            Functor.id (Mon (Functor C D)) ≅ functor.comp 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (X : Mon (Functor C D)) (x✝ : C) :
              (unitIso.inv.app X).hom.app x✝ = CategoryStruct.id (X.X.obj x✝)
              source
              @[simp]
              theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (X : Mon (Functor C D)) (x✝ : C) :
              (unitIso.hom.app X).hom.app x✝ = CategoryStruct.id (X.X.obj x✝)
              source
              def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] :
              inverse.comp functor ≅ Functor.id (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (X : Functor C (Mon D)) (X✝ : C) :
                ((counitIso.hom.app X).app X✝).hom = CategoryStruct.id (X.obj X✝).X
                source
                @[simp]
                theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (X : Functor C (Mon D)) (X✝ : C) :
                ((counitIso.inv.app X).app X✝).hom = CategoryStruct.id (X.obj X✝).X
                source
                def CategoryTheory.Monoidal.monFunctorCategoryEquivalence (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                Mon (Functor C D) ≌ 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_functor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                  (monFunctorCategoryEquivalence C D).functor = MonFunctorCategoryEquivalence.functor
                  source
                  @[simp]
                  theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_inverse (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                  (monFunctorCategoryEquivalence C D).inverse = MonFunctorCategoryEquivalence.inverse
                  source
                  @[simp]
                  theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_unitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                  (monFunctorCategoryEquivalence C D).unitIso = MonFunctorCategoryEquivalence.unitIso
                  source
                  @[simp]
                  theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_counitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                  (monFunctorCategoryEquivalence C D).counitIso = MonFunctorCategoryEquivalence.counitIso
                  source
                  def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [ComonObj A] (X : C) :
                  Comon D

                  A comonoid object in a functor category sends any object to a comonoid object.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_comul {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [ComonObj A] (X : C) :
                    ComonObj.comul = ComonObj.comul.app X
                    source
                    @[simp]
                    theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_X {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [ComonObj A] (X : C) :
                    (functorObjObj A X).X = A.obj X
                    source
                    @[simp]
                    theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_counit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [ComonObj A] (X : C) :
                    ComonObj.counit = ComonObj.counit.app X
                    source
                    def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [ComonObj A] :
                    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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [ComonObj A] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                      ((functorObj A).map f).hom = A.map f
                      source
                      @[simp]
                      theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Functor C D) [ComonObj A] (X : C) :
                      (functorObj A).obj X = functorObjObj A X
                      source
                      def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] :
                      Functor (Comon (Functor C D)) (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (A : Comon (Functor C D)) :
                        functor.obj A = functorObj A.X
                        source
                        @[simp]
                        theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {X✝ Y✝ : Comon (Functor C D)} (f : X✝ ⟶ Y✝) (X : C) :
                        ((functor.map f).app X).hom = f.hom.app X
                        source
                        def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Comon D)) :
                        Comon (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Comon D)) :
                          (inverseObj F).X = F.comp (Comon.forget D)
                          source
                          @[simp]
                          theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Comon D)) (X : C) :
                          ComonObj.comul.app X = ComonObj.comul
                          source
                          @[simp]
                          theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C (Comon D)) (X : C) :
                          ComonObj.counit.app X = ComonObj.counit
                          source
                          def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] :
                          CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝.comp functor ≅ Functor.id (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_inv_app_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (X : Functor C (Comon D)) (X✝ : C) :
                            ((counitIso.inv.app X).app X✝).hom = CategoryStruct.id (X.obj X✝).X
                            source
                            @[simp]
                            theorem CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (X : Functor C (Comon D)) (X✝ : C) :
                            ((counitIso.hom.app X).app X✝).hom = CategoryStruct.id (X.obj X✝).X
                            source
                            def CategoryTheory.Monoidal.comonFunctorCategoryEquivalence (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                            Comon (Functor C D) ≌ 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_unitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                              (comonFunctorCategoryEquivalence C D).unitIso = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso✝
                              source
                              @[simp]
                              theorem CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_functor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                              (comonFunctorCategoryEquivalence C D).functor = ComonFunctorCategoryEquivalence.functor
                              source
                              @[simp]
                              theorem CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_counitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                              (comonFunctorCategoryEquivalence C D).counitIso = ComonFunctorCategoryEquivalence.counitIso
                              source
                              @[simp]
                              theorem CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_inverse (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] :
                              (comonFunctorCategoryEquivalence C D).inverse = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝
                              source
                              def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                              Functor (CommMon (Functor C D)) (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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (A : CommMon (Functor C D)) (X : C) :
                                ((functor.obj A).obj X).X = A.X.obj X
                                source
                                @[simp]
                                theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {X✝ Y✝ : CommMon (Functor C D)} (f : X✝ ⟶ Y✝) (X : C) :
                                ((functor.map f).app X).hom = f.hom.app X
                                source
                                @[simp]
                                theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (A : CommMon (Functor C D)) (X : C) :
                                MonObj.mul = MonObj.mul.app X
                                source
                                @[simp]
                                theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (A : CommMon (Functor C D)) (X : C) :
                                MonObj.one = MonObj.one.app X
                                source
                                @[simp]
                                theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (A : CommMon (Functor C D)) {X Y : C} (a✝ : X ⟶ Y) :
                                ((functor.obj A).map a✝).hom = A.X.map a✝
                                source
                                def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                Functor (Functor C (CommMon D)) (CommMon (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_X_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C (CommMon D)) (X : C) :
                                  (inverse.obj F).X.obj X = (F.obj X).X
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {X✝ Y✝ : Functor C (CommMon D)} (α : X✝ ⟶ Y✝) (X : C) :
                                  (inverse.map α).hom.app X = (α.app X).hom
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C (CommMon D)) (X : C) :
                                  MonObj.one.app X = MonObj.one
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C (CommMon D)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                                  (inverse.obj F).X.map f = (F.map f).hom
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C (CommMon D)) (X : C) :
                                  MonObj.mul.app X = MonObj.mul
                                  source
                                  def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                  Functor.id (CommMon (Functor C D)) ≅ functor.comp 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (X : CommMon (Functor C D)) (x✝ : C) :
                                    (unitIso.hom.app X).hom.app x✝ = CategoryStruct.id (X.X.obj x✝)
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (X : CommMon (Functor C D)) (x✝ : C) :
                                    (unitIso.inv.app X).hom.app x✝ = CategoryStruct.id (X.X.obj x✝)
                                    source
                                    def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                    inverse.comp functor ≅ Functor.id (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_hom_app_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (X : Functor C (CommMon D)) (X✝ : C) :
                                      ((counitIso.hom.app X).app X✝).hom = CategoryStruct.id (X.obj X✝).X
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (X : Functor C (CommMon D)) (X✝ : C) :
                                      ((counitIso.inv.app X).app X✝).hom = CategoryStruct.id (X.obj X✝).X
                                      source
                                      def CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                      CommMon (Functor C D) ≌ 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_functor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                        (commMonFunctorCategoryEquivalence C D).functor = CommMonFunctorCategoryEquivalence.functor
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_unitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                        (commMonFunctorCategoryEquivalence C D).unitIso = CommMonFunctorCategoryEquivalence.unitIso
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_inverse (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                        (commMonFunctorCategoryEquivalence C D).inverse = CommMonFunctorCategoryEquivalence.inverse
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_counitIso (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                                        (commMonFunctorCategoryEquivalence C D).counitIso = CommMonFunctorCategoryEquivalence.counitIso