Documentation

Mathlib.CategoryTheory.Monoidal.Discrete

Monoids as discrete monoidal categories #

The discrete category on a monoid is a monoidal category. Multiplicative morphisms induced monoidal functors.

source
instance CategoryTheory.Discrete.addMonoidal (M : Type u) [AddMonoid M] :
CategoryTheory.MonoidalCategory (CategoryTheory.Discrete M)
Equations
source
@[simp]
theorem CategoryTheory.Discrete.addMonoidal_tensorObj_as (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) :
(CategoryTheory.MonoidalCategory.tensorObj X Y).as = X.as + Y.as
source
@[simp]
theorem CategoryTheory.Discrete.addMonoidal_leftUnitor (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) :
CategoryTheory.MonoidalCategory.leftUnitor X = CategoryTheory.Discrete.eqToIso ⋯
source
@[simp]
theorem CategoryTheory.Discrete.monoidal_leftUnitor (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) :
CategoryTheory.MonoidalCategory.leftUnitor X = CategoryTheory.Discrete.eqToIso ⋯
source
@[simp]
theorem CategoryTheory.Discrete.monoidal_tensorObj_as (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) :
(CategoryTheory.MonoidalCategory.tensorObj X Y).as = X.as * Y.as
source
@[simp]
theorem CategoryTheory.Discrete.monoidal_rightUnitor (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) :
CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯
source
@[simp]
theorem CategoryTheory.Discrete.monoidal_associator (M : Type u) [Monoid M] :
∀ (x x_1 x_2 : CategoryTheory.Discrete M), CategoryTheory.MonoidalCategory.associator x x_1 x_2 = CategoryTheory.Discrete.eqToIso ⋯
source
@[simp]
theorem CategoryTheory.Discrete.addMonoidal_associator (M : Type u) [AddMonoid M] :
∀ (x x_1 x_2 : CategoryTheory.Discrete M), CategoryTheory.MonoidalCategory.associator x x_1 x_2 = CategoryTheory.Discrete.eqToIso ⋯
source
@[simp]
theorem CategoryTheory.Discrete.addMonoidal_rightUnitor (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) :
CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯
source
instance CategoryTheory.Discrete.monoidal (M : Type u) [Monoid M] :
CategoryTheory.MonoidalCategory (CategoryTheory.Discrete M)
Equations
source
@[simp]
theorem CategoryTheory.Discrete.addMonoidal_tensorUnit_as (M : Type u) [AddMonoid M] :
(𝟙_ (CategoryTheory.Discrete M)).as = 0
source
@[simp]
theorem CategoryTheory.Discrete.monoidal_tensorUnit_as (M : Type u) [Monoid M] :
(𝟙_ (CategoryTheory.Discrete M)).as = 1
source
def CategoryTheory.Discrete.addMonoidalFunctor {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) :
CategoryTheory.MonoidalFunctor (CategoryTheory.Discrete M) (CategoryTheory.Discrete N)

An additive morphism between add_monoids gives a monoidal functor between the corresponding discrete monoidal categories.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) :
    ((CategoryTheory.Discrete.addMonoidalFunctor F).obj X).as = F X.as
    source
    @[simp]
    theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_μ {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) :
    (CategoryTheory.Discrete.monoidalFunctor F).μ X Y = CategoryTheory.Discrete.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (X : CategoryTheory.Discrete M) :
    ((CategoryTheory.Discrete.monoidalFunctor F).obj X).as = F X.as
    source
    @[simp]
    theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_map {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) :
    ∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y), (CategoryTheory.Discrete.addMonoidalFunctor F).map f = CategoryTheory.Discrete.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_map {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) :
    ∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y), (CategoryTheory.Discrete.monoidalFunctor F).map f = CategoryTheory.Discrete.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_μ {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) :
    (CategoryTheory.Discrete.addMonoidalFunctor F).μ X Y = CategoryTheory.Discrete.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_ε {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) :
    (CategoryTheory.Discrete.monoidalFunctor F).ε = CategoryTheory.Discrete.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_ε {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) :
    (CategoryTheory.Discrete.addMonoidalFunctor F).ε = CategoryTheory.Discrete.eqToHom ⋯
    source
    def CategoryTheory.Discrete.monoidalFunctor {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) :
    CategoryTheory.MonoidalFunctor (CategoryTheory.Discrete M) (CategoryTheory.Discrete N)

    A multiplicative morphism between monoids gives a monoidal functor between the corresponding discrete monoidal categories.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.Discrete.addMonoidalFunctorComp {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] {K : Type u} [AddMonoid K] (F : M →+ N) (G : N →+ K) :
      CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G ≅ CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)

      The monoidal natural isomorphism corresponding to composing two additive morphisms.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CategoryTheory.Discrete.monoidalFunctorComp {M : Type u} [Monoid M] {N : Type u'} [Monoid N] {K : Type u} [Monoid K] (F : M →* N) (G : N →* K) :
        CategoryTheory.Discrete.monoidalFunctor F ⊗⋙ CategoryTheory.Discrete.monoidalFunctor G ≅ CategoryTheory.Discrete.monoidalFunctor (G.comp F)

        The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

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