Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

The category of commutative monoids in a braided monoidal category. #

source
🔶 coverage
structure CategoryTheory.CommMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
Type (max u₁ v₁)

A commutative monoid object internal to a monoidal category.

  • X : C

    The underlying object in the ambient monoidal category

  • mon : MonObj self.X
  • comm : IsCommMonObj self.X
Instances For
    source
    🔸 coverage
    def CategoryTheory.CommMon.toMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
    Mon C

    A commutative monoid object is a monoid object.

    Instances For
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.CommMon.toMon_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
      A.toMon.X = A.X
      source
      🔸 coverage
      def CategoryTheory.CommMon.trivial (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
      CommMon C

      The trivial commutative monoid object. We later show this is initial in CommMon C.

      Instances For
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.CommMon.trivial_mon_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        MonObj.mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.CommMon.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        (trivial C).X = MonoidalCategoryStruct.tensorUnit C
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.CommMon.trivial_mon_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        MonObj.one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
        source
        🔸 coverage
        @[implicit_reducible]
        instance CategoryTheory.CommMon.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        Inhabited (CommMon C)
        source
        🔸 coverage
        @[implicit_reducible]
        instance CategoryTheory.CommMon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        Category.{v₁, max u₁ v₁} (CommMon C)
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.CommMon.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
        (CategoryStruct.id A).hom.hom = CategoryStruct.id A.X
        source
        📐 coverage
        @[simp]
        theorem CategoryTheory.CommMon.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {R S T : CommMon C} (f : R ⟶ S) (g : S ⟶ T) :
        (CategoryStruct.comp f g).hom.hom = CategoryStruct.comp f.hom.hom g.hom.hom
        source
        theorem CategoryTheory.CommMon.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {A B : CommMon C} (f g : A ⟶ B) (h : f.hom.hom = g.hom.hom) :
        f = g
        source
        📐 coverage
        theorem CategoryTheory.CommMon.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {A B : CommMon C} {f g : A ⟶ B} :
        f = g ↔ f.hom.hom = g.hom.hom
        source
        🔸 coverage
        def CategoryTheory.CommMon.homMk {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {A B : CommMon C} (f : A.toMon ⟶ B.toMon) :
        A ⟶ B

        Constructor for morphisms in CommMon C.

        Instances For
          source
          📐 coverage
          @[simp]
          theorem CategoryTheory.CommMon.homMk_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {A B : CommMon C} (f : A.toMon ⟶ B.toMon) :
          (homMk f).hom = f
          source
          🔸 coverage
          def CategoryTheory.CommMon.forget₂Mon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
          Functor (CommMon C) (Mon C)

          The forgetful functor from commutative monoid objects to monoid objects.

          Instances For
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.CommMon.forget₂Mon_obj_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
            ((forget₂Mon C).obj A).X = A.X
            source
            🔸 coverage
            def CategoryTheory.CommMon.fullyFaithfulForget₂Mon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
            (forget₂Mon C).FullyFaithful

            The forgetful functor from commutative monoid objects to monoid objects is fully faithful.

            Instances For
              source
              📐 coverage
              instance CategoryTheory.CommMon.instFullMonForget₂Mon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
              (forget₂Mon C).Full
              source
              📐 coverage
              instance CategoryTheory.CommMon.instFaithfulMonForget₂Mon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
              (forget₂Mon C).Faithful
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.CommMon.forget₂Mon_obj_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
              MonObj.one = MonObj.one
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.CommMon.forget₂Mon_obj_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
              MonObj.mul = MonObj.mul
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.CommMon.forget₂Mon_map_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {A B : CommMon C} (f : A ⟶ B) :
              ((forget₂Mon C).map f).hom = f.hom.hom
              source
              🔸 coverage
              def CategoryTheory.CommMon.forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
              Functor (CommMon C) C

              The forgetful functor from commutative monoid objects to the ambient category.

              Instances For
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.CommMon.forget_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                (forget C).obj X = X.X
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.CommMon.forget_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : CommMon C} (f : X✝ ⟶ Y✝) :
                (forget C).map f = f.hom.hom
                source
                📐 coverage
                instance CategoryTheory.CommMon.instFaithfulForget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                (forget C).Faithful
                source
                📐 coverage
                @[simp]
                theorem CategoryTheory.CommMon.forget₂Mon_comp_forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                (forget₂Mon C).comp (Mon.forget C) = forget C
                source
                📐 coverage
                instance CategoryTheory.CommMon.instIsIsoHomHomMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : CommMon C} {f : M ⟶ N} [IsIso f] :
                IsIso f.hom.hom
                source
                🔸 coverage
                def CategoryTheory.CommMon.mkIso' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} (e : M ≅ N) [MonObj M] [IsCommMonObj M] [MonObj N] [IsCommMonObj N] [IsMonHom e.hom] :
                { X := M, mon := inst✝, comm := inst✝¹ } ≅ { X := N, mon := inst✝², comm := inst✝³ }

                Construct an isomorphism of commutative monoid objects by giving a monoid isomorphism between the underlying objects.

                Instances For
                  source
                  📐 coverage
                  @[simp]
                  theorem CategoryTheory.CommMon.mkIso'_inv_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} (e : M ≅ N) [MonObj M] [IsCommMonObj M] [MonObj N] [IsCommMonObj N] [IsMonHom e.hom] :
                  (mkIso' e).inv.hom.hom = e.inv
                  source
                  📐 coverage
                  @[simp]
                  theorem CategoryTheory.CommMon.mkIso'_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} (e : M ≅ N) [MonObj M] [IsCommMonObj M] [MonObj N] [IsCommMonObj N] [IsMonHom e.hom] :
                  (mkIso' e).hom.hom.hom = e.hom
                  source
                  🔸 coverage
                  @[reducible, inline]
                  abbrev CategoryTheory.CommMon.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                  M ≅ N

                  Construct an isomorphism of commutative monoid objects by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.

                  Instances For
                    source
                    📐 coverage
                    @[simp]
                    theorem CategoryTheory.CommMon.mkIso_inv_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                    (mkIso e one_f mul_f).inv.hom.hom = e.inv
                    source
                    📐 coverage
                    @[simp]
                    theorem CategoryTheory.CommMon.mkIso_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : CommMon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                    (mkIso e one_f mul_f).hom.hom.hom = e.hom
                    source
                    🔸 coverage
                    @[implicit_reducible]
                    instance CategoryTheory.CommMon.uniqueHomFromTrivial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                    Unique (trivial C ⟶ A)
                    source
                    📐 coverage
                    instance CategoryTheory.CommMon.instHasInitial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                    Limits.HasInitial (CommMon C)
                    source
                    📐 coverage
                    instance CategoryTheory.Functor.isCommMonObj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.LaxBraided] {M : C} [MonObj M] [IsCommMonObj M] :
                    IsCommMonObj (F.obj M)
                    source
                    🔸 coverage
                    def CategoryTheory.Functor.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] :
                    Functor (CommMon C) (CommMon D)

                    A lax braided functor takes commutative monoid objects to commutative monoid objects.

                    That is, a lax braided functor F : C ⥤ D induces a functor CommMon C ⥤ CommMon D.

                    Instances For
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.Functor.mapCommMon_map_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] {X✝ Y✝ : CommMon C} (f : X✝ ⟶ Y✝) :
                      (F.mapCommMon.map f).hom.hom = F.map f.hom.hom
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.Functor.mapCommMon_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon C) :
                      (F.mapCommMon.obj A).X = F.obj A.X
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.Functor.mapCommMon_obj_mon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon C) :
                      MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.Functor.mapCommMon_obj_mon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.LaxBraided] (A : CommMon C) :
                      MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map MonObj.mul)
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.Functor.mapCommMon_id_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                      MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.Functor.mapCommMon_id_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                      MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) MonObj.mul
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.Functor.comp_mapCommMon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] (A : CommMon C) :
                      MonObj.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map MonObj.one)
                      source
                      📐 coverage
                      @[simp]
                      theorem CategoryTheory.Functor.comp_mapCommMon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] (A : CommMon C) :
                      MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map MonObj.mul)
                      source
                      🔸 coverage
                      def CategoryTheory.Functor.mapCommMonIdIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                      (Functor.id C).mapCommMon ≅ Functor.id (CommMon C)

                      The identity functor is also the identity on commutative monoid objects.

                      Instances For
                        source
                        📐 coverage
                        @[simp]
                        theorem CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                        (mapCommMonIdIso.inv.app X).hom.hom = CategoryStruct.id X.X
                        source
                        📐 coverage
                        @[simp]
                        theorem CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                        (mapCommMonIdIso.hom.app X).hom.hom = CategoryStruct.id X.X
                        source
                        🔸 coverage
                        def CategoryTheory.Functor.mapCommMonCompIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] :
                        (F.comp G).mapCommMon ≅ F.mapCommMon.comp G.mapCommMon

                        The composition functor is also the composition on commutative monoid objects.

                        Instances For
                          source
                          📐 coverage
                          @[simp]
                          theorem CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] (X : CommMon C) :
                          (mapCommMonCompIso.inv.app X).hom.hom = CategoryStruct.id (G.obj (F.obj X.X))
                          source
                          📐 coverage
                          @[simp]
                          theorem CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] [BraidedCategory E] {F : Functor C D} {G : Functor D E} [F.LaxBraided] [G.LaxBraided] (X : CommMon C) :
                          (mapCommMonCompIso.hom.app X).hom.hom = CategoryStruct.id (G.obj (F.obj X.X))
                          source
                          🔸 coverage
                          def CategoryTheory.Functor.mapCommMonFunctor (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] :
                          Functor (LaxBraidedFunctor C D) (Functor (CommMon C) (CommMon D))

                          mapCommMon is functorial in the lax braided functor.

                          Instances For
                            source
                            📐 coverage
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMonFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (F : LaxBraidedFunctor C D) :
                            (mapCommMonFunctor C D).obj F = F.mapCommMon
                            source
                            📐 coverage
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMonFunctor_map_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {X✝ Y✝ : LaxBraidedFunctor C D} (α : X✝ ⟶ Y✝) (A : CommMon C) :
                            ((mapCommMonFunctor C D).map α).app A = CommMon.homMk (Mon.Hom.mk' (α.hom.hom.app A.X) ⋯ ⋯)
                            source
                            📐 coverage
                            instance CategoryTheory.Functor.Faithful.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.LaxBraided] [F.Faithful] :
                            F.mapCommMon.Faithful
                            source
                            🔸 coverage
                            def CategoryTheory.Functor.mapCommMonNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (f : F ⟶ F') [NatTrans.IsMonoidal f] :
                            F.mapCommMon ⟶ F'.mapCommMon

                            Natural transformations between functors lift to monoid objects.

                            Instances For
                              source
                              📐 coverage
                              @[simp]
                              theorem CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (f : F ⟶ F') [NatTrans.IsMonoidal f] (X : CommMon C) :
                              ((mapCommMonNatTrans f).app X).hom.hom = f.app X.X
                              source
                              🔸 coverage
                              def CategoryTheory.Functor.mapCommMonNatIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] :
                              F.mapCommMon ≅ F'.mapCommMon

                              Natural isomorphisms between functors lift to monoid objects.

                              Instances For
                                source
                                📐 coverage
                                @[simp]
                                theorem CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : CommMon C) :
                                ((mapCommMonNatIso e).hom.app X).hom.hom = e.hom.app X.X
                                source
                                📐 coverage
                                @[simp]
                                theorem CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.LaxBraided] [F'.LaxBraided] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : CommMon C) :
                                ((mapCommMonNatIso e).inv.app X).hom.hom = e.inv.app X.X
                                source
                                🔸 coverage
                                def CategoryTheory.Functor.FullyFaithful.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] (hF : F.FullyFaithful) :
                                F.mapCommMon.FullyFaithful

                                If F : C ⥤ D is a fully faithful monoidal functor, then CommMonCat(F) : CommMonCat C ⥤ CommMonCat D is fully faithful too.

                                Instances For
                                  source
                                  📐 coverage
                                  @[simp]
                                  theorem CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] (hF : F.FullyFaithful) {X✝ Y✝ : CommMon C} (f : F.mapCommMon.obj X✝ ⟶ F.mapCommMon.obj Y✝) :
                                  hF.mapCommMon.preimage f = CommMon.homMk (hF.mapMon.preimage f.hom)
                                  source
                                  📐 coverage
                                  instance CategoryTheory.Functor.Full.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] [F.Full] [F.Faithful] :
                                  F.mapCommMon.Full
                                  source
                                  🔸 coverage
                                  def CategoryTheory.Adjunction.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :
                                  F.mapCommMon ⊣ G.mapCommMon

                                  An adjunction of braided functors lifts to an adjunction of their lifts to commutative monoid objects.

                                  Instances For
                                    source
                                    📐 coverage
                                    @[simp]
                                    theorem CategoryTheory.Adjunction.mapCommMon_unit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :
                                    a.mapCommMon.unit = CategoryStruct.comp Functor.mapCommMonIdIso.inv (CategoryStruct.comp (Functor.mapCommMonNatTrans a.unit) Functor.mapCommMonCompIso.hom)
                                    source
                                    📐 coverage
                                    @[simp]
                                    theorem CategoryTheory.Adjunction.mapCommMon_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a.IsMonoidal] :
                                    a.mapCommMon.counit = CategoryStruct.comp Functor.mapCommMonCompIso.inv (CategoryStruct.comp (Functor.mapCommMonNatTrans a.counit) Functor.mapCommMonIdIso.hom)
                                    source
                                    🔸 coverage
                                    def CategoryTheory.Equivalence.mapCommMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                    CommMon C ≌ CommMon D

                                    An equivalence of categories lifts to an equivalence of their commutative monoid objects.

                                    Instances For
                                      source
                                      📐 coverage
                                      @[simp]
                                      theorem CategoryTheory.Equivalence.mapCommMon_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                      e.mapCommMon.inverse = e.inverse.mapCommMon
                                      source
                                      📐 coverage
                                      @[simp]
                                      theorem CategoryTheory.Equivalence.mapCommMon_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                      e.mapCommMon.unitIso = Functor.mapCommMonIdIso.symm ≪≫ Functor.mapCommMonNatIso e.unitIso ≪≫ Functor.mapCommMonCompIso
                                      source
                                      📐 coverage
                                      @[simp]
                                      theorem CategoryTheory.Equivalence.mapCommMon_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                      e.mapCommMon.counitIso = Functor.mapCommMonCompIso.symm ≪≫ Functor.mapCommMonNatIso e.counitIso ≪≫ Functor.mapCommMonIdIso
                                      source
                                      📐 coverage
                                      @[simp]
                                      theorem CategoryTheory.Equivalence.mapCommMon_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
                                      e.mapCommMon.functor = e.functor.mapCommMon
                                      source
                                      🔸 coverage
                                      def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                      Functor (LaxBraidedFunctor (Discrete PUnit.{u + 1}) C) (CommMon C)

                                      Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                      Instances For
                                        source
                                        📐 coverage
                                        @[simp]
                                        theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (F : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C) :
                                        (laxBraidedToCommMon C).obj F = F.mapCommMon.obj (trivial (Discrete PUnit.{u + 1}))
                                        source
                                        📐 coverage
                                        @[simp]
                                        theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C} (α : X✝ ⟶ Y✝) :
                                        (laxBraidedToCommMon C).map α = ((Functor.mapCommMonFunctor (Discrete PUnit.{u + 1}) C).map α).app (trivial (Discrete PUnit.{u + 1}))
                                        source
                                        🔸 coverage
                                        def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                        Functor (Discrete PUnit.{u + 1}) C

                                        Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                        Instances For
                                          source
                                          📐 coverage
                                          @[simp]
                                          theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) (x✝ : Discrete PUnit.{u + 1}) :
                                          (commMonToLaxBraidedObj A).obj x✝ = A.X
                                          source
                                          📐 coverage
                                          @[simp]
                                          theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_map {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) {X✝ Y✝ : Discrete PUnit.{u + 1}} (x✝ : X✝ ⟶ Y✝) :
                                          (commMonToLaxBraidedObj A).map x✝ = CategoryStruct.id A.X
                                          source
                                          🔸 coverage
                                          @[implicit_reducible]
                                          instance CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                          (commMonToLaxBraidedObj A).LaxMonoidal
                                          source
                                          📐 coverage
                                          @[simp]
                                          theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                          Functor.LaxMonoidal.ε (commMonToLaxBraidedObj A) = MonObj.one
                                          source
                                          📐 coverage
                                          @[simp]
                                          theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) (X Y : Discrete PUnit.{u_1 + 1}) :
                                          Functor.LaxMonoidal.μ (commMonToLaxBraidedObj A) X Y = MonObj.mul
                                          source
                                          🔸 coverage
                                          @[implicit_reducible]
                                          instance CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                          (commMonToLaxBraidedObj A).LaxBraided
                                          source
                                          🔸 coverage
                                          def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                          Functor (CommMon C) (LaxBraidedFunctor (Discrete PUnit.{u + 1}) C)

                                          Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                          Instances For
                                            source
                                            📐 coverage
                                            @[simp]
                                            theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                            (commMonToLaxBraided C).obj A = LaxBraidedFunctor.of (commMonToLaxBraidedObj A)
                                            source
                                            📐 coverage
                                            @[simp]
                                            theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : CommMon C} (f : X✝ ⟶ Y✝) (x✝ : Discrete PUnit.{u + 1}) :
                                            ((commMonToLaxBraided C).map f).hom.hom.app x✝ = f.hom.hom
                                            source
                                            🔸 coverage
                                            def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                            Functor.id (LaxBraidedFunctor (Discrete PUnit.{u + 1}) C) ≅ (laxBraidedToCommMon C).comp (commMonToLaxBraided C)

                                            Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                            Instances For
                                              source
                                              📐 coverage
                                              @[simp]
                                              theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C) (X✝ : Discrete PUnit.{u + 1}) :
                                              ((unitIso C).inv.app X).hom.hom.app X✝ = CategoryStruct.id (X.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{u + 1})))
                                              source
                                              📐 coverage
                                              @[simp]
                                              theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C) (X✝ : Discrete PUnit.{u + 1}) :
                                              ((unitIso C).hom.app X).hom.hom.app X✝ = CategoryStruct.id (X.obj X✝)
                                              source
                                              📐 coverage
                                              @[simp]
                                              theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                              MonObj.one = CategoryStruct.comp MonObj.one (CategoryStruct.id A.X)
                                              source
                                              📐 coverage
                                              @[simp]
                                              theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                              MonObj.mul = CategoryStruct.comp MonObj.mul (CategoryStruct.id A.X)
                                              source
                                              🔸 coverage
                                              def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                              (commMonToLaxBraided C).comp (laxBraidedToCommMon C) ≅ Functor.id (CommMon C)

                                              Implementation of CommMon.equivLaxBraidedFunctorPUnit.

                                              Instances For
                                                source
                                                📐 coverage
                                                @[simp]
                                                theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                                                ((counitIso C).hom.app X).hom.hom = CategoryStruct.id X.X
                                                source
                                                📐 coverage
                                                @[simp]
                                                theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon C) :
                                                ((counitIso C).inv.app X).hom.hom = CategoryStruct.id X.X
                                                source
                                                🔸 coverage
                                                def CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                LaxBraidedFunctor (Discrete PUnit.{u + 1}) C ≌ CommMon C

                                                Commutative monoid objects in C are "just" braided lax monoidal functors from the trivial braided monoidal category to C.

                                                Instances For
                                                  source
                                                  📐 coverage
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  equivLaxBraidedFunctorPUnit.unitIso = EquivLaxBraidedFunctorPUnit.unitIso C
                                                  source
                                                  📐 coverage
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  equivLaxBraidedFunctorPUnit.counitIso = EquivLaxBraidedFunctorPUnit.counitIso C
                                                  source
                                                  📐 coverage
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  equivLaxBraidedFunctorPUnit.inverse = EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C
                                                  source
                                                  📐 coverage
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  equivLaxBraidedFunctorPUnit.functor = EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C