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.

theorem CategoryTheory.Discrete.addMonoidal.proof_3 (M : Type u_1) [AddMonoid M] :
∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.Discrete M}, (X₁ Y₁)(X₂ Y₂)(fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ Y₂
theorem CategoryTheory.Discrete.addMonoidal.proof_2 (M : Type u_1) [AddMonoid M] :
∀ {X₁ X₂ : CategoryTheory.Discrete M}, (X₁ X₂)∀ (X : CategoryTheory.Discrete M), (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₂ X
theorem CategoryTheory.Discrete.addMonoidal.proof_1 (M : Type u_1) [AddMonoid M] (X : CategoryTheory.Discrete M) :
∀ (x x_1 : CategoryTheory.Discrete M), (x x_1)(fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X x = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X x_1
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_11 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) :
CategoryTheory.IsIso { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X Y) => CategoryTheory.Discrete.eqToHom , map_id := , map_comp := , ε := CategoryTheory.Discrete.eqToHom , μ := fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom , μ_natural_left := , μ_natural_right := , associativity := , left_unitality := , right_unitality := }
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_1 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) :
∀ {X Y : CategoryTheory.Discrete M}, (X Y)F X.as = F Y.as
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_4 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) :
0 = F 0

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
    theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_5 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) :
    F X.as + F Y.as = F (X.as + Y.as)
    theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_12 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) :
    CategoryTheory.IsIso ({ obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X Y) => CategoryTheory.Discrete.eqToHom , map_id := , map_comp := , ε := CategoryTheory.Discrete.eqToHom , μ := fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom , μ_natural_left := , μ_natural_right := , associativity := , left_unitality := , right_unitality := } X Y)

    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

      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

        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