Documentation

Mathlib.CategoryTheory.Monoidal.CommMon_

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

source
structure CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.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 : Mon_Class self.X
  • comm : IsCommMon self.X
Instances For
    source
    def CommMon_.toMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
    Mon_ C

    A commutative monoid object is a monoid object.

    Equations
    Instances For
      source
      @[simp]
      theorem CommMon_.toMon__X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
      A.toMon_.X = A.X
      source
      def CommMon_.trivial (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
      CommMon_ C

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

      Equations
      Instances For
        source
        @[simp]
        theorem CommMon_.trivial_mon_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
        Mon_Class.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
        source
        @[simp]
        theorem CommMon_.trivial_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
        (trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
        source
        @[simp]
        theorem CommMon_.trivial_mon_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
        Mon_Class.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        source
        instance CommMon_.instInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
        Inhabited (CommMon_ C)
        Equations
        source
        instance CommMon_.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
        CategoryTheory.Category.{v₁, max u₁ v₁} (CommMon_ C)
        Equations
        source
        @[simp]
        theorem CommMon_.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
        (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.X
        source
        @[simp]
        theorem CommMon_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {R S T : CommMon_ C} (f : R ⟶ S) (g : S ⟶ T) :
        (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
        source
        theorem CommMon_.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommMon_ C} (f g : A ⟶ B) (h : f.hom = g.hom) :
        f = g
        source
        theorem CommMon_.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommMon_ C} {f g : A ⟶ B} :
        f = g ↔ f.hom = g.hom
        source
        @[simp]
        theorem CommMon_.id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
        CategoryTheory.CategoryStruct.id A = CategoryTheory.CategoryStruct.id A.toMon_
        source
        @[simp]
        theorem CommMon_.comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A₁ A₂ A₃ : CommMon_ C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :
        CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g
        source
        def CommMon_.forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
        CategoryTheory.Functor (CommMon_ C) (Mon_ C)

        The forgetful functor from commutative monoid objects to monoid objects.

        Equations
        Instances For
          source
          def CommMon_.fullyFaithfulForget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
          (forget₂Mon_ C).FullyFaithful

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

          Equations
          Instances For
            source
            instance CommMon_.instFullMon_Forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            (forget₂Mon_ C).Full
            source
            instance CommMon_.instFaithfulMon_Forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            (forget₂Mon_ C).Faithful
            source
            @[simp]
            theorem CommMon_.forget₂Mon_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
            Mon_Class.one = Mon_Class.one
            source
            @[simp]
            theorem CommMon_.forget₂Mon_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
            Mon_Class.mul = Mon_Class.mul
            source
            @[simp]
            theorem CommMon_.forget₂Mon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommMon_ C} (f : A ⟶ B) :
            ((forget₂Mon_ C).map f).hom = f.hom
            source
            @[deprecated CommMon_.forget₂Mon_obj_one (since := "2025-02-07")]
            theorem CommMon_.forget₂_Mon_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
            Mon_Class.one = Mon_Class.one

            Alias of CommMon_.forget₂Mon_obj_one.

            source
            @[deprecated CommMon_.forget₂Mon_obj_mul (since := "2025-02-07")]
            theorem CommMon_.forget₂_Mon_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
            Mon_Class.mul = Mon_Class.mul

            Alias of CommMon_.forget₂Mon_obj_mul.

            source
            @[deprecated CommMon_.forget₂Mon_map_hom (since := "2025-02-07")]
            theorem CommMon_.forget₂_Mon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommMon_ C} (f : A ⟶ B) :
            ((forget₂Mon_ C).map f).hom = f.hom

            Alias of CommMon_.forget₂Mon_map_hom.

            source
            def CommMon_.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
            CategoryTheory.Functor (CommMon_ C) C

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

            Equations
            Instances For
              source
              @[simp]
              theorem CommMon_.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CommMon_ C} (f : X✝ ⟶ Y✝) :
              (forget C).map f = f.hom
              source
              @[simp]
              theorem CommMon_.forget_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CommMon_ C) :
              (forget C).obj X = ((forget₂Mon_ C).obj X).X
              source
              instance CommMon_.instFaithfulForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
              (forget C).Faithful
              source
              @[simp]
              theorem CommMon_.forget₂Mon_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
              (forget₂Mon_ C).comp (Mon_.forget C) = forget C
              source
              instance CommMon_.instIsIsoHom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} {f : M ⟶ N} [CategoryTheory.IsIso f] :
              CategoryTheory.IsIso f.hom
              source
              def CommMon_.mkIso' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} (e : M ≅ N) [Mon_Class M] [IsCommMon M] [Mon_Class N] [IsCommMon N] [IsMon_Hom 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 CommMon_.mkIso'_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} (e : M ≅ N) [Mon_Class M] [IsCommMon M] [Mon_Class N] [IsCommMon N] [IsMon_Hom e.hom] :
                (mkIso' e).hom.hom = e.hom
                source
                @[simp]
                theorem CommMon_.mkIso'_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} (e : M ≅ N) [Mon_Class M] [IsCommMon M] [Mon_Class N] [IsCommMon N] [IsMon_Hom e.hom] :
                (mkIso' e).inv.hom = e.inv
                source
                @[reducible, inline]
                abbrev CommMon_.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} (e : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp Mon_Class.one e.hom = Mon_Class.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp Mon_Class.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) Mon_Class.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 CommMon_.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} (e : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp Mon_Class.one e.hom = Mon_Class.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp Mon_Class.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) Mon_Class.mul := by cat_disch) :
                  (mkIso e one_f mul_f).inv.hom = e.inv
                  source
                  @[simp]
                  theorem CommMon_.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommMon_ C} (e : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp Mon_Class.one e.hom = Mon_Class.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp Mon_Class.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) Mon_Class.mul := by cat_disch) :
                  (mkIso e one_f mul_f).hom.hom = e.hom
                  source
                  instance CommMon_.uniqueHomFromTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
                  Unique (trivial C ⟶ A)
                  Equations
                  source
                  instance CommMon_.instHasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                  CategoryTheory.Limits.HasInitial (CommMon_ C)
                  source
                  instance CategoryTheory.Functor.isCommMon_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} [Mon_Class M] [IsCommMon M] :
                  IsCommMon (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_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) :
                    Mon_Class.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map Mon_Class.one)
                    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_map_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 = F.map f.hom
                    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) :
                    Mon_Class.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map Mon_Class.mul)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.mapCommMon_id_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon_ C) :
                    Mon_Class.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) Mon_Class.one
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.mapCommMon_id_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : CommMon_ C) :
                    Mon_Class.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) Mon_Class.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) :
                    Mon_Class.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map Mon_Class.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) :
                    Mon_Class.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map Mon_Class.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_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon_ C) :
                      (mapCommMonIdIso.inv.app X).hom = CategoryStruct.id X.X
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : CommMon_ C) :
                      (mapCommMonIdIso.hom.app X).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
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.mapCommMonCompIso_hom_app_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 = CategoryStruct.id (G.obj (F.obj X.X))
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.mapCommMonCompIso_inv_app_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 = 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_map_app_hom (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).hom = α.hom.app A.X
                          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
                          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
                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.Functor.mapCommMonNatTrans_app_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 = 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 {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 = e.hom.app X.X
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.mapCommMonNatIso_inv_app_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 = e.inv.app X.X
                              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.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 Grp(F) : Grp C ⥤ Grp 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_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.Braided] (hF : F.FullyFaithful) {X✝ Y✝ : CommMon_ C} (f : F.mapCommMon.obj X✝ ⟶ F.mapCommMon.obj Y✝) :
                                (hF.mapCommMon.preimage f).hom = hF.preimage f.hom
                                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_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
                                  @[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
                                  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_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_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
                                    @[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_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
                                    def CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                    CategoryTheory.Functor (CategoryTheory.LaxBraidedFunctor (CategoryTheory.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 CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (F : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) :
                                      (laxBraidedToCommMon C).obj F = F.mapCommMon.obj (trivial (CategoryTheory.Discrete PUnit.{u + 1}))
                                      source
                                      @[simp]
                                      theorem CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C} (α : X✝ ⟶ Y✝) :
                                      (laxBraidedToCommMon C).map α = ((CategoryTheory.Functor.mapCommMonFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C).map α).app (trivial (CategoryTheory.Discrete PUnit.{u + 1}))
                                      source
                                      def CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
                                      CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u + 1}) C

                                      Implementation of CommMon_.equivLaxBraidedFunctorPUnit.

                                      Equations
                                      Instances For
                                        source
                                        @[simp]
                                        theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) {X✝ Y✝ : CategoryTheory.Discrete PUnit.{u + 1}} (x✝ : X✝ ⟶ Y✝) :
                                        (commMonToLaxBraidedObj A).map x✝ = CategoryTheory.CategoryStruct.id A.X
                                        source
                                        @[simp]
                                        theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) (x✝ : CategoryTheory.Discrete PUnit.{u + 1}) :
                                        (commMonToLaxBraidedObj A).obj x✝ = A.X
                                        source
                                        instance CommMon_.EquivLaxBraidedFunctorPUnit.instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
                                        (commMonToLaxBraidedObj A).LaxMonoidal
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        source
                                        @[simp]
                                        theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
                                        CategoryTheory.Functor.LaxMonoidal.ε (commMonToLaxBraidedObj A) = Mon_Class.one
                                        source
                                        @[simp]
                                        theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}) :
                                        CategoryTheory.Functor.LaxMonoidal.μ (commMonToLaxBraidedObj A) X Y = Mon_Class.mul
                                        source
                                        instance CommMon_.EquivLaxBraidedFunctorPUnit.instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
                                        (commMonToLaxBraidedObj A).LaxBraided
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        source
                                        def CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                        CategoryTheory.Functor (CommMon_ C) (CategoryTheory.LaxBraidedFunctor (CategoryTheory.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 CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CommMon_ C} (f : X✝ ⟶ Y✝) (x✝ : CategoryTheory.Discrete PUnit.{u + 1}) :
                                          ((commMonToLaxBraided C).map f).hom.app x✝ = f.hom
                                          source
                                          @[simp]
                                          theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
                                          (commMonToLaxBraided C).obj A = CategoryTheory.LaxBraidedFunctor.of (commMonToLaxBraidedObj A)
                                          source
                                          def CommMon_.EquivLaxBraidedFunctorPUnit.unitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                          CategoryTheory.Functor.id (CategoryTheory.LaxBraidedFunctor (CategoryTheory.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 CommMon_.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) (X✝ : CategoryTheory.Discrete PUnit.{u + 1}) :
                                            ((unitIso C).inv.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{u + 1})))
                                            source
                                            @[simp]
                                            theorem CommMon_.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) (X✝ : CategoryTheory.Discrete PUnit.{u + 1}) :
                                            ((unitIso C).hom.app X).hom.app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
                                            source
                                            @[simp]
                                            theorem CommMon_.EquivLaxBraidedFunctorPUnit.counitIso_aux_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
                                            Mon_Class.one = CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.id A.X)
                                            source
                                            @[simp]
                                            theorem CommMon_.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommMon_ C) :
                                            Mon_Class.mul = CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.id A.X)
                                            source
                                            def CommMon_.EquivLaxBraidedFunctorPUnit.counitIso (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                            (commMonToLaxBraided C).comp (laxBraidedToCommMon C) ≅ CategoryTheory.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 CommMon_.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CommMon_ C) :
                                              ((counitIso C).hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
                                              source
                                              @[simp]
                                              theorem CommMon_.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CommMon_ C) :
                                              ((counitIso C).inv.app X).hom = CategoryTheory.CategoryStruct.id X.X
                                              source
                                              def CommMon_.equivLaxBraidedFunctorPUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                              CategoryTheory.LaxBraidedFunctor (CategoryTheory.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 CommMon_.equivLaxBraidedFunctorPUnit_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                equivLaxBraidedFunctorPUnit.inverse = EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C
                                                source
                                                @[simp]
                                                theorem CommMon_.equivLaxBraidedFunctorPUnit_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                equivLaxBraidedFunctorPUnit.functor = EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C
                                                source
                                                @[simp]
                                                theorem CommMon_.equivLaxBraidedFunctorPUnit_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                equivLaxBraidedFunctorPUnit.counitIso = EquivLaxBraidedFunctorPUnit.counitIso C
                                                source
                                                @[simp]
                                                theorem CommMon_.equivLaxBraidedFunctorPUnit_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
                                                equivLaxBraidedFunctorPUnit.unitIso = EquivLaxBraidedFunctorPUnit.unitIso C