Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

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

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

    Equations
    Instances For
      source
      @[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
      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.

      Equations
      Instances For
        source
        @[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
        @[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
        @[simp]
        theorem CategoryTheory.CommMon.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        (trivial C).X = MonoidalCategoryStruct.tensorUnit C
        source
        @[implicit_reducible]
        instance CategoryTheory.CommMon.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        Inhabited (CommMon C)
        Equations
        source
        @[implicit_reducible]
        instance CategoryTheory.CommMon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        Category.{v₁, max u₁ v₁} (CommMon C)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[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
        @[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
        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
        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.

        Equations
        Instances For
          source
          @[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
          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.

          Equations
          Instances For
            source
            @[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
            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.

            Equations
            Instances For
              source
              instance CategoryTheory.CommMon.instFullMonForget₂Mon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
              (forget₂Mon C).Full
              source
              instance CategoryTheory.CommMon.instFaithfulMonForget₂Mon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
              (forget₂Mon C).Faithful
              source
              @[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
              @[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
              @[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
              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.

              Equations
              Instances For
                source
                @[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
                @[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
                instance CategoryTheory.CommMon.instFaithfulForget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                (forget C).Faithful
                source
                @[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
                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
                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.

                Equations
                Instances For
                  source
                  @[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
                  @[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
                  @[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.

                  Equations
                  Instances For
                    source
                    @[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
                    @[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
                    @[implicit_reducible]
                    instance CategoryTheory.CommMon.uniqueHomFromTrivial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                    Unique (trivial C ⟶ A)
                    Equations
                    source
                    instance CategoryTheory.CommMon.instHasInitial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                    Limits.HasInitial (CommMon C)
                    source
                    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
                    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.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[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
                      @[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
                      @[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
                      @[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
                      @[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
                      @[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
                      @[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
                      @[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
                      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.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[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
                        @[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
                        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.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[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
                          @[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
                          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.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[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
                            @[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
                            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
                            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.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[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
                              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.

                              Equations
                              Instances For
                                source
                                @[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
                                @[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
                                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.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  @[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
                                  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
                                  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.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    @[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
                                    @[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
                                    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.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      @[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
                                      @[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
                                      @[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
                                      @[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
                                      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.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        @[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
                                        @[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
                                        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.

                                        Equations
                                        Instances For
                                          source
                                          @[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
                                          @[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
                                          @[implicit_reducible]
                                          instance CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                          (commMonToLaxBraidedObj A).LaxMonoidal
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          source
                                          @[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
                                          @[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
                                          @[implicit_reducible]
                                          instance CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon C) :
                                          (commMonToLaxBraidedObj A).LaxBraided
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          source
                                          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.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            @[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
                                            @[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
                                            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.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              @[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
                                              @[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
                                              @[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
                                              @[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
                                              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.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                @[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
                                                @[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
                                                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.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  equivLaxBraidedFunctorPUnit.unitIso = EquivLaxBraidedFunctorPUnit.unitIso C
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  equivLaxBraidedFunctorPUnit.functor = EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  equivLaxBraidedFunctorPUnit.counitIso = EquivLaxBraidedFunctorPUnit.counitIso C
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                                  equivLaxBraidedFunctorPUnit.inverse = EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C