Monoids as discrete monoidal categories #

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

source

@[instance_reducible]

instance CategoryTheory.Discrete.monoidal (M : Type u) [Monoid M] :

MonoidalCategory (Discrete M)

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_tensorObj_as (M : Type u) [AddMonoid M] (X Y : Discrete M) :

(MonoidalCategoryStruct.tensorObj X Y).as = X.as + Y.as

source

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_rightUnitor (M : Type u) [AddMonoid M] (X : Discrete M) :

MonoidalCategoryStruct.rightUnitor X = Discrete.eqToIso ⋯

source

@[simp]

theorem CategoryTheory.Discrete.monoidal_tensorObj_as (M : Type u) [Monoid M] (X Y : Discrete M) :

(MonoidalCategoryStruct.tensorObj X Y).as = X.as * Y.as

source

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_associator (M : Type u) [AddMonoid M] (x✝ x✝¹ x✝² : Discrete M) :

MonoidalCategoryStruct.associator x✝ x✝¹ x✝² = Discrete.eqToIso ⋯

source

@[simp]

theorem CategoryTheory.Discrete.monoidal_associator (M : Type u) [Monoid M] (x✝ x✝¹ x✝² : Discrete M) :

MonoidalCategoryStruct.associator x✝ x✝¹ x✝² = Discrete.eqToIso ⋯

source

@[simp]

theorem CategoryTheory.Discrete.monoidal_rightUnitor (M : Type u) [Monoid M] (X : Discrete M) :

MonoidalCategoryStruct.rightUnitor X = Discrete.eqToIso ⋯

source

@[simp]

theorem CategoryTheory.Discrete.monoidal_leftUnitor (M : Type u) [Monoid M] (X : Discrete M) :

MonoidalCategoryStruct.leftUnitor X = Discrete.eqToIso ⋯

source

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_leftUnitor (M : Type u) [AddMonoid M] (X : Discrete M) :

MonoidalCategoryStruct.leftUnitor X = Discrete.eqToIso ⋯

source

@[instance_reducible]

instance CategoryTheory.Discrete.addMonoidal (M : Type u) [AddMonoid M] :

MonoidalCategory (Discrete M)

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Discrete.monoidal_tensorUnit_as (M : Type u) [Monoid M] :

(MonoidalCategoryStruct.tensorUnit (Discrete M)).as = 1

source

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_tensorUnit_as (M : Type u) [AddMonoid M] :

(MonoidalCategoryStruct.tensorUnit (Discrete M)).as = 0

source

def CategoryTheory.Discrete.monoidalFunctor {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) :

Functor (Discrete M) (Discrete N)

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

Equations

CategoryTheory.Discrete.monoidalFunctor F = CategoryTheory.Discrete.functor fun (X : M) => { as := F X }

Instances For

source

def CategoryTheory.Discrete.addMonoidalFunctor {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) :

Functor (Discrete M) (Discrete N)

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

Equations

CategoryTheory.Discrete.addMonoidalFunctor F = CategoryTheory.Discrete.functor fun (X : M) => { as := F X }

Instances For

source

@[simp]

theorem CategoryTheory.Discrete.monoidalFunctor_obj {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m : M) :

(monoidalFunctor F).obj { as := m } = { as := F m }

source

@[simp]

theorem CategoryTheory.Discrete.addMonoidalFunctor_obj {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m : M) :

(addMonoidalFunctor F).obj { as := m } = { as := F m }

source

@[instance_reducible]

instance CategoryTheory.Discrete.monoidalFunctorMonoidal {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) :

(monoidalFunctor F).Monoidal

Equations

One or more equations did not get rendered due to their size.

source

@[instance_reducible]

instance CategoryTheory.Discrete.addMonoidalFunctorMonoidal {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) :

(addMonoidalFunctor F).Monoidal

Equations

One or more equations did not get rendered due to their size.

source

theorem CategoryTheory.Discrete.monoidalFunctor_ε {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) :

Functor.LaxMonoidal.ε (monoidalFunctor F) = Discrete.eqToHom ⋯

source

theorem CategoryTheory.Discrete.addMonoidalFunctor_ε {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) :

Functor.LaxMonoidal.ε (addMonoidalFunctor F) = Discrete.eqToHom ⋯

source

theorem CategoryTheory.Discrete.monoidalFunctor_η {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) :

Functor.OplaxMonoidal.η (monoidalFunctor F) = Discrete.eqToHom ⋯

source

theorem CategoryTheory.Discrete.addMonoidalFunctor_η {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) :

Functor.OplaxMonoidal.η (addMonoidalFunctor F) = Discrete.eqToHom ⋯

source

theorem CategoryTheory.Discrete.monoidalFunctor_μ {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m₁ m₂ : Discrete M) :

Functor.LaxMonoidal.μ (monoidalFunctor F) m₁ m₂ = Discrete.eqToHom ⋯

source

theorem CategoryTheory.Discrete.addMonoidalFunctor_μ {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m₁ m₂ : Discrete M) :

Functor.LaxMonoidal.μ (addMonoidalFunctor F) m₁ m₂ = Discrete.eqToHom ⋯

source

theorem CategoryTheory.Discrete.monoidalFunctor_δ {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m₁ m₂ : Discrete M) :

Functor.OplaxMonoidal.δ (monoidalFunctor F) m₁ m₂ = Discrete.eqToHom ⋯

source

theorem CategoryTheory.Discrete.addMonoidalFunctor_δ {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m₁ m₂ : Discrete M) :

Functor.OplaxMonoidal.δ (addMonoidalFunctor F) m₁ m₂ = Discrete.eqToHom ⋯

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) :

(monoidalFunctor F).comp (monoidalFunctor G) ≅ monoidalFunctor (G.comp F)

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

Equations

CategoryTheory.Discrete.monoidalFunctorComp F G = CategoryTheory.Iso.refl ((CategoryTheory.Discrete.monoidalFunctor F).comp (CategoryTheory.Discrete.monoidalFunctor G))

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) :

(addMonoidalFunctor F).comp (addMonoidalFunctor G) ≅ addMonoidalFunctor (G.comp F)

The monoidal natural isomorphism corresponding to composing two additive morphisms.

Equations

CategoryTheory.Discrete.addMonoidalFunctorComp F G = CategoryTheory.Iso.refl ((CategoryTheory.Discrete.addMonoidalFunctor F).comp (CategoryTheory.Discrete.addMonoidalFunctor G))

Instances For

source

instance CategoryTheory.Discrete.monoidalFunctorComp_isMonoidal {M : Type u} [Monoid M] {N : Type u'} [Monoid N] {K : Type u} [Monoid K] (F : M →* N) (G : N →* K) :

NatTrans.IsMonoidal (monoidalFunctorComp F G).hom

source

instance CategoryTheory.Discrete.addMonoidalFunctorComp_isMonoidal {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] {K : Type u} [AddMonoid K] (F : M →+ N) (G : N →+ K) :

NatTrans.IsMonoidal (addMonoidalFunctorComp F G).hom

Documentation

Mathlib.CategoryTheory.Monoidal.Discrete

Monoids as discrete monoidal categories #