Documentation

Mathlib.CategoryTheory.Monoidal.Comon_

The category of comonoids in a monoidal category. #

We define comonoids in a monoidal category C, and show that they are equivalently monoid objects in the opposite category.

We construct the monoidal structure on Comon_ C, when C is braided.

An oplax monoidal functor takes comonoid objects to comonoid objects. That is, a oplax monoidal functor F : C ⥤ D induces a functor Comon_ C ⥤ Comon_ D.

TODO #

A comonoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called a "coalgebra object".

Instances For

    The trivial comonoid object. We later show this is terminal in Comon_ C.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Comon_.Hom.ext {C : Type u₁} :
      ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : Comon_ C} {x y : M.Hom N}, x.hom = y.homx = y
      theorem Comon_.Hom.ext_iff {C : Type u₁} :
      ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M N : Comon_ C} {x y : M.Hom N}, x = y x.hom = y.hom

      A morphism of comonoid objects.

      Instances For
        @[simp]
        theorem Comon_.Hom.hom_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Comon_ C} {N : Comon_ C} (self : M.Hom N) :
        CategoryTheory.CategoryStruct.comp self.hom N.counit = M.counit

        The identity morphism on a comonoid object.

        Equations
        Instances For
          Equations
          • M.homInhabited = { default := M.id }
          @[simp]
          theorem Comon_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Comon_ C} {N : Comon_ C} {O : Comon_ C} (f : M.Hom N) (g : N.Hom O) :
          def Comon_.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Comon_ C} {N : Comon_ C} {O : Comon_ C} (f : M.Hom N) (g : N.Hom O) :
          M.Hom O

          Composition of morphisms of monoid objects.

          Equations
          Instances For
            theorem Comon_.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Comon_ C} {Y : Comon_ C} {f : X Y} {g : X Y} :
            f = g f.hom = g.hom
            theorem Comon_.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Comon_ C} {Y : Comon_ C} {f : X Y} {g : X Y} (w : f.hom = g.hom) :
            f = g
            @[simp]
            theorem Comon_.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
            ∀ {X Y : Comon_ C} (f : X Y), (Comon_.forget C).map f = f.hom

            The forgetful functor from comonoid objects to the ambient category.

            Equations
            Instances For

              The forgetful functor from comonoid objects to the ambient category reflects isomorphisms.

              Equations
              • =
              @[simp]
              theorem Comon_.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Comon_ C} {N : Comon_ C} (f : M.X N.X) (f_counit : autoParam (CategoryTheory.CategoryStruct.comp f.hom N.counit = M.counit) _auto✝) (f_comul : autoParam (CategoryTheory.CategoryStruct.comp f.hom N.comul = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.MonoidalCategory.tensorHom f.hom f.hom)) _auto✝) :
              (Comon_.mkIso f f_counit f_comul).inv.hom = f.inv
              @[simp]
              theorem Comon_.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {M : Comon_ C} {N : Comon_ C} (f : M.X N.X) (f_counit : autoParam (CategoryTheory.CategoryStruct.comp f.hom N.counit = M.counit) _auto✝) (f_comul : autoParam (CategoryTheory.CategoryStruct.comp f.hom N.comul = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.MonoidalCategory.tensorHom f.hom f.hom)) _auto✝) :
              (Comon_.mkIso f f_counit f_comul).hom.hom = f.hom

              Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects and checking compatibility with counit and comultiplication only in the forward direction.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • A.uniqueHomToTrivial = { default := { hom := A.counit, hom_counit := , hom_comul := }, uniq := }

                Turn a comonoid object into a monoid object in the opposite category.

                Equations
                Instances For
                  @[simp]
                  theorem Comon_.Comon_ToMon_OpOp_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                  ∀ {X Y : Comon_ C} (f : X Y), (Comon_.Comon_ToMon_OpOp C).map f = Opposite.op { hom := f.hom.op, one_hom := , mul_hom := }

                  The contravariant functor turning comonoid objects into monoid objects in the opposite category.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Turn a monoid object in the opposite category into a comonoid object.

                    Equations
                    Instances For
                      @[simp]

                      The contravariant functor turning monoid objects in the opposite category into comonoid objects.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Comonoid objects are contravariantly equivalent to monoid objects in the opposite category.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Comonoid objects in a braided category form a monoidal category.

                          This definition is via transporting back and forth to monoids in the opposite category,

                          Equations

                          Preliminary statement of the comultiplication for a tensor product of comonoids. This version is the definitional equality provided by transport, and not quite as good as the version provided in tensorObj_comul below.

                          The comultiplication on the tensor product of two comonoids is the tensor product of the comultiplications followed by the tensor strength (to shuffle the factors back into order).

                          The forgetful functor from Comon_ C to C is monoidal when C is braided monoidal.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            A oplax monoidal functor takes comonoid objects to comonoid objects.

                            That is, a oplax monoidal functor F : C ⥤ D induces a functor Comon_ C ⥤ Comon_ D.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For