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 RingMon_ 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.

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
    @[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_1 : C), ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1

    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

      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
        @[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_1 : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.map α).hom.app X_1 = (α.app X_1).hom

        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
          @[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)
          @[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)
          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
            @[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
            @[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
            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

              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

                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
                  @[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_1 : C), ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1

                  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

                    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
                      @[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
                      @[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
                      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

                        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
                          @[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
                          @[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_1 : C), ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1
                          @[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
                          @[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
                          @[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

                          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
                            @[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_1 : C), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.map α).hom.app X_1 = (α.app X_1).hom
                            @[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
                            @[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
                            @[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
                            @[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

                            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
                              @[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
                              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
                                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

                                  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