mathlib3 documentation

category_theory.monoidal.discrete

Monoids as discrete monoidal categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[simp]
theorem discrete.add_monoidal_tensor_add_unit_as (M : Type u) [add_monoid M] :
(𝟙_ (category_theory.discrete M)).as = 0
source
@[simp]
theorem category_theory.discrete.monoidal_tensor_unit_as (M : Type u) [monoid M] :
(𝟙_ (category_theory.discrete M)).as = 1
source
@[simp]
theorem category_theory.discrete.monoidal_tensor_obj_as (M : Type u) [monoid M] (X Y : category_theory.discrete M) :
(X ⊗ Y).as = X.as * Y.as
source
@[protected, instance]
def discrete.add_monoidal (M : Type u) [add_monoid M] :
category_theory.monoidal_category (category_theory.discrete M)
Equations
source
@[protected, instance]
def category_theory.discrete.monoidal (M : Type u) [monoid M] :
category_theory.monoidal_category (category_theory.discrete M)
Equations
source
@[simp]
theorem discrete.add_monoidal_tensor_obj_as (M : Type u) [add_monoid M] (X Y : category_theory.discrete M) :
(X ⊗ Y).as = X.as + Y.as
source
def category_theory.discrete.monoidal_functor {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) :
category_theory.monoidal_functor (category_theory.discrete M) (category_theory.discrete N)

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

Equations
source
@[simp]
theorem discrete.add_monoidal_functor_to_lax_monoidal_functor_ε {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) :
(discrete.add_monoidal_functor F).to_lax_monoidal_functor.ε = category_theory.discrete.eq_to_hom _
source
@[simp]
theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_μ {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) (X Y : category_theory.discrete M) :
(category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor.μ X Y = category_theory.discrete.eq_to_hom _
source
@[simp]
theorem discrete.add_monoidal_functor_to_lax_monoidal_functor_to_functor_obj_as {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) (X : category_theory.discrete M) :
((discrete.add_monoidal_functor F).to_lax_monoidal_functor.to_functor.obj X).as = ⇑F X.as
source
@[simp]
theorem discrete.add_monoidal_functor_to_lax_monoidal_functor_μ {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) (X Y : category_theory.discrete M) :
(discrete.add_monoidal_functor F).to_lax_monoidal_functor.μ X Y = category_theory.discrete.eq_to_hom _
source
@[simp]
theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_ε {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) :
(category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor.ε = category_theory.discrete.eq_to_hom _
source
@[simp]
theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_to_functor_obj_as {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) (X : category_theory.discrete M) :
((category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor.to_functor.obj X).as = ⇑F X.as
source
def discrete.add_monoidal_functor {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) :
category_theory.monoidal_functor (category_theory.discrete M) (category_theory.discrete N)

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

Equations
source
@[simp]
theorem discrete.add_monoidal_functor_to_lax_monoidal_functor_to_functor_map {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) (X Y : category_theory.discrete M) (f : X ⟶ Y) :
(discrete.add_monoidal_functor F).to_lax_monoidal_functor.to_functor.map f = category_theory.discrete.eq_to_hom _
source
@[simp]
theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_to_functor_map {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) (X Y : category_theory.discrete M) (f : X ⟶ Y) :
(category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor.to_functor.map f = category_theory.discrete.eq_to_hom _
source
def discrete.add_monoidal_functor_comp {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] {K : Type u} [add_monoid K] (F : M →+ N) (G : N →+ K) :
discrete.add_monoidal_functor F ⊗⋙ discrete.add_monoidal_functor G ≅ discrete.add_monoidal_functor (G.comp F)

The monoidal natural isomorphism corresponding to composing two additive morphisms.

Equations
source
def category_theory.discrete.monoidal_functor_comp {M : Type u} [monoid M] {N : Type u} [monoid N] {K : Type u} [monoid K] (F : M →* N) (G : N →* K) :
category_theory.discrete.monoidal_functor F ⊗⋙ category_theory.discrete.monoidal_functor G ≅ category_theory.discrete.monoidal_functor (G.comp F)

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

Equations