The category of monoids in a monoidal category.

We define monoids in a monoidal category C and show that the category of monoids is equivalent to the category of lax monoidal functors from the unit monoidal category to C. We also show that if C is braided, then the category of monoids is naturally monoidal. We use the to_additive attribute in order to generate a parallel API for additive monoids.

Simp set for monoid object tautologies

In this file, we also provide a simp set called mon_tauto whose goal is to prove all tautologies about morphisms from some (tensor) power of M to M, where M is a (commutative) monoid object in a (braided) monoidal category.

Please read the documentation in Mathlib/Tactic/Attr/Register.lean for full details.

TODO

• Check that Mon MonCat ≌ CommMonCat, via the Eckmann-Hilton argument. (You'll have to hook up the Cartesian monoidal structure on MonCat first, available in https://github.com/leanprover-community/mathlib3/pull/3463)
• More generally, check that Mon (Mon C) ≌ CommMon C when C is braided.
• Check that Mon TopCat ≌ [bundled topological monoids].
• Check that Mon AddCommGrpCat ≌ RingCat. (We've already got Mon (ModuleCat R) ≌ AlgCat R, in Mathlib/CategoryTheory/Monoidal/Internal/Module.lean.)
• Can you transport this monoidal structure to RingCat or AlgCat R? How does it compare to the "native" one?

class CategoryTheory.AddMonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) : Type v₁

An additive monoid object internal to a monoidal category.

• zero : MonoidalCategoryStruct.tensorUnit C ⟶ X

  The zero morphism of an additive monoid object.

• add : MonoidalCategoryStruct.tensorObj X X ⟶ X

  The additiion morphism of an additive monoid object.

• zero_add : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight zero X) add = (MonoidalCategoryStruct.leftUnitor X).hom
• add_zero : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X zero) add = (MonoidalCategoryStruct.rightUnitor X).hom
• add_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight add X) add = CategoryStruct.comp (MonoidalCategoryStruct.associator X X X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X add) add)

class CategoryTheory.MonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : C) : Type v₁

A monoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called an "algebra object".

• one : MonoidalCategoryStruct.tensorUnit C ⟶ X

  The unit morphism of a monoid object.

• mul : MonoidalCategoryStruct.tensorObj X X ⟶ X

  The multiplication morphism of a monoid object.

• one_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one X) mul = (MonoidalCategoryStruct.leftUnitor X).hom
• mul_one : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X one) mul = (MonoidalCategoryStruct.rightUnitor X).hom
• mul_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul X) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator X X X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X mul) mul)

def CategoryTheory.AddMonObj.termσ : Lean.ParserDescr

The additiion morphism of an additive monoid object.

Equations

• CategoryTheory.AddMonObj.termσ = Lean.ParserDescr.node `CategoryTheory.AddMonObj.termσ 1024 (Lean.ParserDescr.symbol "σ")

def CategoryTheory.AddMonObj.«termσ[_]» : Lean.ParserDescr

The additiion morphism of an additive monoid object.

Equations

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

def CategoryTheory.AddMonObj.termζ : Lean.ParserDescr

The zero morphism of an additive monoid object.

Equations

• CategoryTheory.AddMonObj.termζ = Lean.ParserDescr.node `CategoryTheory.AddMonObj.termζ 1024 (Lean.ParserDescr.symbol "ζ")

def CategoryTheory.AddMonObj.«termζ[_]» : Lean.ParserDescr

The zero morphism of an additive monoid object.

Equations

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

def CategoryTheory.MonObj.termμ : Lean.ParserDescr

The multiplication morphism of a monoid object.

Equations

• CategoryTheory.MonObj.termμ = Lean.ParserDescr.node `CategoryTheory.MonObj.termμ 1024 (Lean.ParserDescr.symbol "μ")

def CategoryTheory.MonObj.«termμ[_]» : Lean.ParserDescr

The multiplication morphism of a monoid object.

Equations

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

def CategoryTheory.MonObj.termη : Lean.ParserDescr

The unit morphism of a monoid object.

Equations

• CategoryTheory.MonObj.termη = Lean.ParserDescr.node `CategoryTheory.MonObj.termη 1024 (Lean.ParserDescr.symbol "η")

def CategoryTheory.MonObj.«termη[_]» : Lean.ParserDescr

The unit morphism of a monoid object.

Equations

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

@[simp]

theorem CategoryTheory.MonObj.mul_one_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : MonObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X one) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom h

@[simp]

theorem CategoryTheory.MonObj.one_mul_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : MonObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one X) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom h

@[simp]

theorem CategoryTheory.MonObj.mul_assoc_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : MonObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul X) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.associator X X X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X mul) (CategoryStruct.comp mul h))

@[simp]

theorem CategoryTheory.AddMonObj.add_assoc_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : AddMonObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight add X) (CategoryStruct.comp add h) = CategoryStruct.comp (MonoidalCategoryStruct.associator X X X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X add) (CategoryStruct.comp add h))

@[simp]

theorem CategoryTheory.AddMonObj.zero_add_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : AddMonObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight zero X) (CategoryStruct.comp add h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom h

@[simp]

theorem CategoryTheory.AddMonObj.add_zero_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} (X : C) [self : AddMonObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X zero) (CategoryStruct.comp add h) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom h

@[implicit_reducible]

def CategoryTheory.MonObj.ofIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (e : M ≅ X) : MonObj X

Transfer MonObj along an isomorphism.

Equations

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

@[implicit_reducible]

def CategoryTheory.AddMonObj.ofIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [AddMonObj M] (e : M ≅ X) : AddMonObj X

Transfer AddMonObj along an isomorphism.

Equations

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

theorem CategoryTheory.MonObj.ofIso_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (e : M ≅ X) : one = CategoryStruct.comp one e.hom

theorem CategoryTheory.AddMonObj.ofIso_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [AddMonObj M] (e : M ≅ X) : add = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.inv e.inv) (CategoryStruct.comp add e.hom)

theorem CategoryTheory.MonObj.ofIso_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (e : M ≅ X) : mul = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.inv e.inv) (CategoryStruct.comp mul e.hom)

theorem CategoryTheory.AddMonObj.ofIso_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [AddMonObj M] (e : M ≅ X) : zero = CategoryStruct.comp zero e.hom

@[implicit_reducible]

instance CategoryTheory.MonObj.instTensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : MonObj (MonoidalCategoryStruct.tensorUnit C)

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMonObj.instTensorAddUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : AddMonObj (MonoidalCategoryStruct.tensorUnit C)

Equations

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

@[simp]

theorem CategoryTheory.AddMonObj.zero_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : zero = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.AddMonObj.add_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : add = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem CategoryTheory.MonObj.one_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.MonObj.mul_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

theorem CategoryTheory.MonObj.ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} (h₁ h₂ : MonObj X) (H : mul = mul) : h₁ = h₂

theorem CategoryTheory.AddMonObj.ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} (h₁ h₂ : AddMonObj X) (H : add = add) : h₁ = h₂

theorem CategoryTheory.MonObj.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} {h₁ h₂ : MonObj X} : h₁ = h₂ ↔ mul = mul

theorem CategoryTheory.AddMonObj.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} {h₁ h₂ : AddMonObj X} : h₁ = h₂ ↔ add = add

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) : CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj X₂ (MonoidalCategoryStruct.tensorObj Y₂ Z₂) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom h✝)

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) : CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X₂ Y₂) Z₂ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv h✝)

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (gh : MonoidalCategoryStruct.tensorObj Y₂ Z₂ ⟶ W) : CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (MonoidalCategoryStruct.tensorHom f (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g h) gh)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom (MonoidalCategoryStruct.tensorHom (CategoryStruct.id X₂) gh))

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (gh : MonoidalCategoryStruct.tensorObj Y₂ Z₂ ⟶ W) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj X₂ W ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g h) gh)) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.tensorHom f g) h) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id X₂) gh) h✝))

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (fg : MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ W) : CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) fg) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv (MonoidalCategoryStruct.tensorHom fg (CategoryStruct.id Z₂)))

theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) (fg : MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ W) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj W Z₂ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) fg) h) h✝) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (MonoidalCategoryStruct.tensorHom g h)) (CategoryStruct.comp (MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom fg (CategoryStruct.id Z₂)) h✝))

theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_one_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] : (MonoidalCategoryStruct.leftUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.one (CategoryStruct.id M)) MonObj.mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_zero_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] : (MonoidalCategoryStruct.leftUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom AddMonObj.zero (CategoryStruct.id M)) AddMonObj.add

theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_mul_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] : (MonoidalCategoryStruct.rightUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) MonObj.one) MonObj.mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_add_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] : (MonoidalCategoryStruct.rightUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) AddMonObj.zero) AddMonObj.add

theorem CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [MonObj M] (f : X₁ ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.one f) MonObj.mul) = f

theorem CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_neg_zero_tensor_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [AddMonObj M] (f : X₁ ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom AddMonObj.zero f) AddMonObj.add) = f

theorem CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [MonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.one f) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp f h

theorem CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_neg_zero_tensor_add_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [AddMonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom AddMonObj.zero f) (CategoryStruct.comp AddMonObj.add h)) = CategoryStruct.comp f h

theorem CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [MonObj M] (f : X₁ ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f MonObj.one) MonObj.mul) = f

theorem CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_neg_tensor_zero_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [AddMonObj M] (f : X₁ ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f AddMonObj.zero) AddMonObj.add) = f

theorem CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [MonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f MonObj.one) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp f h

theorem CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_neg_tensor_zero_add_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X₁ : C} [AddMonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X₁).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f AddMonObj.zero) (CategoryStruct.comp AddMonObj.add h)) = CategoryStruct.comp f h

theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (f : X ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.associator X M M).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f MonObj.mul) MonObj.mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id M)) MonObj.mul) (CategoryStruct.id M)) MonObj.mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [AddMonObj M] (f : X ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.associator X M M).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f AddMonObj.add) AddMonObj.add) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id M)) AddMonObj.add) (CategoryStruct.id M)) AddMonObj.add

theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator X M M).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f MonObj.mul) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id M)) MonObj.mul) (CategoryStruct.id M)) (CategoryStruct.comp MonObj.mul h)

theorem CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [AddMonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator X M M).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f AddMonObj.add) (CategoryStruct.comp AddMonObj.add h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f (CategoryStruct.id M)) AddMonObj.add) (CategoryStruct.id M)) (CategoryStruct.comp AddMonObj.add h)

theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (f : X ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul f) MonObj.mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) f) MonObj.mul)) MonObj.mul

theorem CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_neg {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [AddMonObj M] (f : X ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom AddMonObj.add f) AddMonObj.add) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) f) AddMonObj.add)) AddMonObj.add

theorem CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_neg_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [AddMonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom AddMonObj.add f) (CategoryStruct.comp AddMonObj.add h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) f) AddMonObj.add)) (CategoryStruct.comp AddMonObj.add h)

theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul f) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (CategoryStruct.id M) f) MonObj.mul)) (CategoryStruct.comp MonObj.mul h)

class CategoryTheory.IsAddMonHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M' N' : C} [AddMonObj M'] [AddMonObj N'] (f : M' ⟶ N') : Prop

The property that a morphism between additive monoid objects is an additive monoid morphism.

• zero_hom : CategoryStruct.comp AddMonObj.zero f = AddMonObj.zero
• add_hom : CategoryStruct.comp AddMonObj.add f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) AddMonObj.add

class CategoryTheory.IsMonHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (f : M ⟶ N) : Prop

The property that a morphism between monoid objects is a monoid morphism.

• one_hom : CategoryStruct.comp MonObj.one f = MonObj.one
• mul_hom : CategoryStruct.comp MonObj.mul f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) MonObj.mul

@[simp]

theorem CategoryTheory.IsMonHom.mul_hom_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : C} {inst✝² : MonObj M} {inst✝³ : MonObj N} (f : M ⟶ N) [self : IsMonHom f] {Z : C} (h : N ⟶ Z) : CategoryStruct.comp MonObj.mul (CategoryStruct.comp f h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) (CategoryStruct.comp MonObj.mul h)

@[simp]

theorem CategoryTheory.IsAddMonHom.zero_hom_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M' N' : C} {inst✝² : AddMonObj M'} {inst✝³ : AddMonObj N'} (f : M' ⟶ N') [self : IsAddMonHom f] {Z : C} (h : N' ⟶ Z) : CategoryStruct.comp AddMonObj.zero (CategoryStruct.comp f h) = CategoryStruct.comp AddMonObj.zero h

@[simp]

theorem CategoryTheory.IsAddMonHom.add_hom_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M' N' : C} {inst✝² : AddMonObj M'} {inst✝³ : AddMonObj N'} (f : M' ⟶ N') [self : IsAddMonHom f] {Z : C} (h : N' ⟶ Z) : CategoryStruct.comp AddMonObj.add (CategoryStruct.comp f h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) (CategoryStruct.comp AddMonObj.add h)

@[simp]

theorem CategoryTheory.IsMonHom.one_hom_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : C} {inst✝² : MonObj M} {inst✝³ : MonObj N} (f : M ⟶ N) [self : IsMonHom f] {Z : C} (h : N ⟶ Z) : CategoryStruct.comp MonObj.one (CategoryStruct.comp f h) = CategoryStruct.comp MonObj.one h

instance CategoryTheory.instIsMonHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] : IsMonHom (CategoryStruct.id M)

instance CategoryTheory.instIsAddMonHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] : IsAddMonHom (CategoryStruct.id M)

instance CategoryTheory.instIsAddMonHomComp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : C} [AddMonObj M] [AddMonObj N] [AddMonObj O] (f : M ⟶ N) (g : N ⟶ O) [IsAddMonHom f] [IsAddMonHom g] : IsAddMonHom (CategoryStruct.comp f g)

instance CategoryTheory.instIsMonHomComp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : C} [MonObj M] [MonObj N] [MonObj O] (f : M ⟶ N) (g : N ⟶ O) [IsMonHom f] [IsMonHom g] : IsMonHom (CategoryStruct.comp f g)

instance CategoryTheory.isMonHom_ofIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [MonObj M] (e : M ≅ X) : IsMonHom e.hom

instance CategoryTheory.isAddMonHom_ofIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M X : C} [AddMonObj M] (e : M ≅ X) : IsAddMonHom e.hom

instance CategoryTheory.instIsMonHomInvOfHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (f : M ≅ N) [IsMonHom f.hom] : IsMonHom f.inv

instance CategoryTheory.instIsAddMonHomNegOfHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] (f : M ≅ N) [IsAddMonHom f.hom] : IsAddMonHom f.inv

instance CategoryTheory.instIsMonHomHomAsIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] {f : M ⟶ N} [IsIso f] [IsMonHom f] : IsMonHom (asIso f).hom

instance CategoryTheory.instIsAddMonHomHomAsIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] {f : M ⟶ N} [IsIso f] [IsAddMonHom f] : IsAddMonHom (asIso f).hom

structure CategoryTheory.AddMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Type (max u₁ v₁)

An additive monoid object internal to a monoidal category.

• X : C

  The underlying object in the ambient monoidal category

• addMon : AddMonObj self.X

structure CategoryTheory.Mon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Type (max u₁ v₁)

A monoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called an "algebra object".

• X : C

  The underlying object in the ambient monoidal category

• mon : MonObj self.X

def CategoryTheory.Mon.trivial (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Mon C

The trivial monoid object. We later show this is initial in Mon C.

Equations

• CategoryTheory.Mon.trivial C = { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, mon := CategoryTheory.MonObj.instTensorUnit }

def CategoryTheory.AddMon.trivial (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : AddMon C

The trivial additive monoid object. We later show this is initial in AddMon C

Equations

• CategoryTheory.AddMon.trivial C = { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, addMon := CategoryTheory.AddMonObj.instTensorAddUnit }

@[simp]

theorem CategoryTheory.Mon.trivial_mon_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : MonObj.one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.trivial_mon_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : MonObj.mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem CategoryTheory.AddMon.trivial_addMon_add (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : AddMonObj.add = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem CategoryTheory.AddMon.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : (trivial C).X = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.AddMon.trivial_addMon_zero (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : AddMonObj.zero = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : (trivial C).X = MonoidalCategoryStruct.tensorUnit C

@[implicit_reducible]

instance CategoryTheory.Mon.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Inhabited (Mon C)

Equations

• CategoryTheory.Mon.instInhabited = { default := CategoryTheory.Mon.trivial C }

@[implicit_reducible]

instance CategoryTheory.AddMon.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Inhabited (AddMon C)

Equations

• CategoryTheory.AddMon.instInhabited = { default := CategoryTheory.AddMon.trivial C }

@[simp]

theorem CategoryTheory.MonObj.one_mul_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] {Z : C} (f : Z ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom one f) mul = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Z).hom f

@[simp]

theorem CategoryTheory.AddMonObj.zero_add_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] {Z : C} (f : Z ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom zero f) add = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Z).hom f

@[simp]

theorem CategoryTheory.MonObj.one_mul_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] {Z : C} (f : Z ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom one f) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Z).hom (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.AddMonObj.zero_add_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] {Z : C} (f : Z ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom zero f) (CategoryStruct.comp add h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Z).hom (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.MonObj.mul_one_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] {Z : C} (f : Z ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f one) mul = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Z).hom f

@[simp]

theorem CategoryTheory.AddMonObj.add_zero_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] {Z : C} (f : Z ⟶ M) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f zero) add = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Z).hom f

@[simp]

theorem CategoryTheory.AddMonObj.add_zero_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] {Z : C} (f : Z ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f zero) (CategoryStruct.comp add h) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Z).hom (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.MonObj.mul_one_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] {Z : C} (f : Z ⟶ M) {Z✝ : C} (h : M ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f one) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Z).hom (CategoryStruct.comp f h)

theorem CategoryTheory.MonObj.mul_assoc_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M mul) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator M M M).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul M) mul)

theorem CategoryTheory.AddMonObj.add_assoc_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M add) add = CategoryStruct.comp (MonoidalCategoryStruct.associator M M M).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight add M) add)

theorem CategoryTheory.AddMonObj.add_assoc_flip_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M add) (CategoryStruct.comp add h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M M M).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight add M) (CategoryStruct.comp add h))

theorem CategoryTheory.MonObj.mul_assoc_flip_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M mul) (CategoryStruct.comp mul h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M M M).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul M) (CategoryStruct.comp mul h))

In this section, we prove that the category of monoids in a braided monoidal category is monoidal.

Given two monoids M and N in a braided monoidal category C, the multiplication on the tensor product M.X ⊗ N.X is defined in the obvious way: it is the tensor product of the multiplications on M and N, except that the tensor factors in the source come in the wrong order, which we fix by pre-composing with a permutation isomorphism constructed from the braiding.

(There is a subtlety here: in fact there are two ways to do these, using either the positive or negative crossing.)

A more conceptual way of understanding this definition is the following: The braiding on C gives rise to a monoidal structure on the tensor product functor from C × C to C. A pair of monoids in C gives rise to a monoid in C × C, which the tensor product functor by being monoidal takes to a monoid in C. The permutation isomorphism appearing in the definition of the multiplication on the tensor product of two monoids is an instance of a more general family of isomorphisms which together form a strength that equips the tensor product functor with a monoidal structure, and the monoid axioms for the tensor product follow from the monoid axioms for the tensor factors plus the properties of the strength (i.e., monoidal functor axioms). The strength tensorμ of the tensor product functor has been defined in Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean. Its properties, stated as independent lemmas in that module, are used extensively in the proofs below. Notice that we could have followed the above plan not only conceptually but also as a possible implementation and could have constructed the tensor product of monoids via mapMon, but we chose to give a more explicit definition directly in terms of tensorμ.

To complete the definition of the monoidal category structure on the category of monoids, we need to provide definitions of associator and unitors. The obvious candidates are the associator and unitors from C, but we need to prove that they are monoid morphisms, i.e., compatible with unit and multiplication. These properties translate to the monoidality of the associator and unitors (with respect to the monoidal structures on the functors they relate), which have also been proved in Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean.

theorem CategoryTheory.MonObj.one_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N P : C} [MonObj M] [MonObj N] [MonObj P] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom one one)) one)) (MonoidalCategoryStruct.associator M N P).hom = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom one (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom one one)))

theorem CategoryTheory.AddMonObj.zero_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N P : C} [AddMonObj M] [AddMonObj N] [AddMonObj P] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom zero zero)) zero)) (MonoidalCategoryStruct.associator M N P).hom = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom zero (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom zero zero)))

theorem CategoryTheory.MonObj.one_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) one)) (MonoidalCategoryStruct.leftUnitor M).hom = one

theorem CategoryTheory.AddMonObj.zero_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) zero)) (MonoidalCategoryStruct.leftUnitor M).hom = zero

theorem CategoryTheory.MonObj.one_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom one (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)))) (MonoidalCategoryStruct.rightUnitor M).hom = one

theorem CategoryTheory.AddMonObj.zero_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom zero (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)))) (MonoidalCategoryStruct.rightUnitor M).hom = zero

theorem CategoryTheory.MonObj.Mon_tensor_one_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : C) [MonObj M] [MonObj N] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom one one)) (MonoidalCategoryStruct.tensorObj M N)) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul)) = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorObj M N)).hom

theorem CategoryTheory.AddMonObj.AddMon_tensor_zero_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : C) [AddMonObj M] [AddMonObj N] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom zero zero)) (MonoidalCategoryStruct.tensorObj M N)) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom add add)) = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorObj M N)).hom

theorem CategoryTheory.MonObj.Mon_tensor_mul_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : C) [MonObj M] [MonObj N] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorObj M N) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom one one))) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul)) = (MonoidalCategoryStruct.rightUnitor (MonoidalCategoryStruct.tensorObj M N)).hom

theorem CategoryTheory.AddMonObj.AddMon_tensor_add_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : C) [AddMonObj M] [AddMonObj N] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorObj M N) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom zero zero))) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom add add)) = (MonoidalCategoryStruct.rightUnitor (MonoidalCategoryStruct.tensorObj M N)).hom

theorem CategoryTheory.MonObj.Mon_tensor_mul_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : C) [MonObj M] [MonObj N] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul)) (MonoidalCategoryStruct.tensorObj M N)) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (MonoidalCategoryStruct.tensorObj M N) (MonoidalCategoryStruct.tensorObj M N) (MonoidalCategoryStruct.tensorObj M N)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorObj M N) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul))) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul)))

theorem CategoryTheory.AddMonObj.AddMon_tensor_add_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : C) [AddMonObj M] [AddMonObj N] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom add add)) (MonoidalCategoryStruct.tensorObj M N)) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom add add)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (MonoidalCategoryStruct.tensorObj M N) (MonoidalCategoryStruct.tensorObj M N) (MonoidalCategoryStruct.tensorObj M N)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (MonoidalCategoryStruct.tensorObj M N) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom add add))) (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom add add)))

theorem CategoryTheory.MonObj.mul_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N P : C} [MonObj M] [MonObj N] [MonObj P] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategory.tensorμ (MonoidalCategoryStruct.tensorObj M N) P (MonoidalCategoryStruct.tensorObj M N) P) (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul)) mul)) (MonoidalCategoryStruct.associator M N P).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.associator M N P).hom (MonoidalCategoryStruct.associator M N P).hom) (CategoryStruct.comp (MonoidalCategory.tensorμ M (MonoidalCategoryStruct.tensorObj N P) M (MonoidalCategoryStruct.tensorObj N P)) (MonoidalCategoryStruct.tensorHom mul (CategoryStruct.comp (MonoidalCategory.tensorμ N P N P) (MonoidalCategoryStruct.tensorHom mul mul))))

theorem CategoryTheory.AddMonObj.add_associator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N P : C} [AddMonObj M] [AddMonObj N] [AddMonObj P] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategory.tensorμ (MonoidalCategoryStruct.tensorObj M N) P (MonoidalCategoryStruct.tensorObj M N) P) (MonoidalCategoryStruct.tensorHom (CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom add add)) add)) (MonoidalCategoryStruct.associator M N P).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.associator M N P).hom (MonoidalCategoryStruct.associator M N P).hom) (CategoryStruct.comp (MonoidalCategory.tensorμ M (MonoidalCategoryStruct.tensorObj N P) M (MonoidalCategoryStruct.tensorObj N P)) (MonoidalCategoryStruct.tensorHom add (CategoryStruct.comp (MonoidalCategory.tensorμ N P N P) (MonoidalCategoryStruct.tensorHom add add))))

theorem CategoryTheory.MonObj.mul_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M : C} [MonObj M] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategory.tensorμ (MonoidalCategoryStruct.tensorUnit C) M (MonoidalCategoryStruct.tensorUnit C) M) (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom mul)) (MonoidalCategoryStruct.leftUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.leftUnitor M).hom (MonoidalCategoryStruct.leftUnitor M).hom) mul

theorem CategoryTheory.AddMonObj.add_leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M : C} [AddMonObj M] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategory.tensorμ (MonoidalCategoryStruct.tensorUnit C) M (MonoidalCategoryStruct.tensorUnit C) M) (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom add)) (MonoidalCategoryStruct.leftUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.leftUnitor M).hom (MonoidalCategoryStruct.leftUnitor M).hom) add

theorem CategoryTheory.MonObj.mul_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M : C} [MonObj M] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategory.tensorμ M (MonoidalCategoryStruct.tensorUnit C) M (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.tensorHom mul (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom)) (MonoidalCategoryStruct.rightUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.rightUnitor M).hom (MonoidalCategoryStruct.rightUnitor M).hom) mul

theorem CategoryTheory.AddMonObj.add_rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M : C} [AddMonObj M] : CategoryStruct.comp (CategoryStruct.comp (MonoidalCategory.tensorμ M (MonoidalCategoryStruct.tensorUnit C) M (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.tensorHom add (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom)) (MonoidalCategoryStruct.rightUnitor M).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (MonoidalCategoryStruct.rightUnitor M).hom (MonoidalCategoryStruct.rightUnitor M).hom) add

@[implicit_reducible]

instance CategoryTheory.MonObj.tensorObj.instTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] : MonObj (MonoidalCategoryStruct.tensorObj M N)

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMonObj.tensorObj.instTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [AddMonObj M] [AddMonObj N] : AddMonObj (MonoidalCategoryStruct.tensorObj M N)

Equations

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

theorem CategoryTheory.MonObj.tensorObj.mul_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] : mul = CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom mul mul)

theorem CategoryTheory.AddMonObj.tensorObj.add_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [AddMonObj M] [AddMonObj N] : add = CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom add add)

theorem CategoryTheory.MonObj.tensorObj.one_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] : one = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom one one)

theorem CategoryTheory.AddMonObj.tensorObj.zero_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [AddMonObj M] [AddMonObj N] : zero = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom zero zero)

instance CategoryTheory.MonObj.instIsMonHomTensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z W : C} [MonObj X] [MonObj Y] [MonObj Z] [MonObj W] {f : X ⟶ Y} {g : Z ⟶ W} [IsMonHom f] [IsMonHom g] : IsMonHom (MonoidalCategoryStruct.tensorHom f g)

instance CategoryTheory.AddMonObj.instIsAddMonHomTensorHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z W : C} [AddMonObj X] [AddMonObj Y] [AddMonObj Z] [AddMonObj W] {f : X ⟶ Y} {g : Z ⟶ W} [IsAddMonHom f] [IsAddMonHom g] : IsAddMonHom (MonoidalCategoryStruct.tensorHom f g)

instance CategoryTheory.MonObj.instIsMonHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [MonObj X] : IsMonHom (CategoryStruct.id X)

instance CategoryTheory.AddMonObj.instIsAddMonHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X : C} [AddMonObj X] : IsAddMonHom (CategoryStruct.id X)

instance CategoryTheory.MonObj.instIsMonHomWhiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [MonObj X] [MonObj Y] [MonObj Z] {f : Y ⟶ Z} [IsMonHom f] : IsMonHom (MonoidalCategoryStruct.whiskerLeft X f)

instance CategoryTheory.AddMonObj.instIsAddMonHomWhiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [AddMonObj X] [AddMonObj Y] [AddMonObj Z] {f : Y ⟶ Z} [IsAddMonHom f] : IsAddMonHom (MonoidalCategoryStruct.whiskerLeft X f)

instance CategoryTheory.MonObj.instIsMonHomWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [MonObj X] [MonObj Y] [MonObj Z] {f : X ⟶ Y} [IsMonHom f] : IsMonHom (MonoidalCategoryStruct.whiskerRight f Z)

instance CategoryTheory.AddMonObj.instIsAddMonHomWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [AddMonObj X] [AddMonObj Y] [AddMonObj Z] {f : X ⟶ Y} [IsAddMonHom f] : IsAddMonHom (MonoidalCategoryStruct.whiskerRight f Z)

instance CategoryTheory.MonObj.instIsMonHomHomAssociator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [MonObj X] [MonObj Y] [MonObj Z] : IsMonHom (MonoidalCategoryStruct.associator X Y Z).hom

instance CategoryTheory.AddMonObj.instIsAddMonHomHomAssociator {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y Z : C} [AddMonObj X] [AddMonObj Y] [AddMonObj Z] : IsAddMonHom (MonoidalCategoryStruct.associator X Y Z).hom

instance CategoryTheory.MonObj.instIsMonHomHomLeftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X : C} [MonObj X] : IsMonHom (MonoidalCategoryStruct.leftUnitor X).hom

instance CategoryTheory.AddMonObj.instIsAddMonHomHomLeftUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X : C} [AddMonObj X] : IsAddMonHom (MonoidalCategoryStruct.leftUnitor X).hom

instance CategoryTheory.MonObj.instIsMonHomHomRightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X : C} [MonObj X] : IsMonHom (MonoidalCategoryStruct.rightUnitor X).hom

instance CategoryTheory.AddMonObj.instIsAddMonHomHomRightUnitor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X : C} [AddMonObj X] : IsAddMonHom (MonoidalCategoryStruct.rightUnitor X).hom

theorem CategoryTheory.MonObj.one_braiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : C) [MonObj X] [MonObj Y] : CategoryStruct.comp one (β_ X Y).hom = one

theorem CategoryTheory.AddMonObj.zero_braiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : C) [AddMonObj X] [AddMonObj Y] : CategoryStruct.comp zero (β_ X Y).hom = zero

structure CategoryTheory.AddMon.Hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M N : AddMon C) : Type v₁

A morphism of additive monoid objects.

• hom : M.X ⟶ N.X

  The underlying morphism

• isAddMonHom_hom : IsAddMonHom self.hom

theorem CategoryTheory.AddMon.Hom.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : AddMon C} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.AddMon.Hom.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : AddMon C} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

structure CategoryTheory.Mon.Hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M N : Mon C) : Type v₁

A morphism of monoid objects.

• hom : M.X ⟶ N.X

  The underlying morphism

• isMonHom_hom : IsMonHom self.hom

theorem CategoryTheory.Mon.Hom.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : Mon C} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.Mon.Hom.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {M N : Mon C} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

@[reducible, inline]

abbrev CategoryTheory.Mon.Hom.mk' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (f : M.X ⟶ N.X) (one_f : CategoryStruct.comp MonObj.one f = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) MonObj.mul := by cat_disch) : M.Hom N

Construct a morphism M ⟶ N of Mon C from a map f : M ⟶ N and compatibilities with the unit and the multiplication.

Equations

• CategoryTheory.Mon.Hom.mk' f one_f mul_f = { hom := f, isMonHom_hom := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.AddMon.Hom.mk' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} (f : M.X ⟶ N.X) (zero_f : CategoryStruct.comp AddMonObj.zero f = AddMonObj.zero := by cat_disch) (add_f : CategoryStruct.comp AddMonObj.add f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) AddMonObj.add := by cat_disch) : M.Hom N

Construct a morphism M ⟶ N of AddMon C from a map f : M ⟶ N and compatibilities with the zero and the addition.

Equations

• CategoryTheory.AddMon.Hom.mk' f one_f mul_f = { hom := f, isAddMonHom_hom := ⋯ }

def CategoryTheory.Mon.id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Mon C) : M.Hom M

The identity morphism on a monoid object.

Equations

• M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isMonHom_hom := ⋯ }

def CategoryTheory.AddMon.id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : AddMon C) : M.Hom M

The identity morphism on an additive monoid object.

Equations

• M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isAddMonHom_hom := ⋯ }

@[simp]

theorem CategoryTheory.AddMon.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : AddMon C) : M.id.hom = CategoryStruct.id M.X

@[simp]

theorem CategoryTheory.Mon.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Mon C) : M.id.hom = CategoryStruct.id M.X

@[implicit_reducible]

instance CategoryTheory.Mon.homInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Mon C) : Inhabited (M.Hom M)

Equations

• M.homInhabited = { default := M.id }

@[implicit_reducible]

instance CategoryTheory.AddMon.homInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : AddMon C) : Inhabited (M.Hom M)

Equations

• M.homInhabited = { default := M.id }

def CategoryTheory.Mon.comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : Mon C} (f : M.Hom N) (g : N.Hom O) : M.Hom O

Composition of morphisms of monoid objects.

Equations

• CategoryTheory.Mon.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isMonHom_hom := ⋯ }

def CategoryTheory.AddMon.comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : AddMon C} (f : M.Hom N) (g : N.Hom O) : M.Hom O

Composition of morphisms of additive monoid objects.

Equations

• CategoryTheory.AddMon.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isAddMonHom_hom := ⋯ }

@[simp]

theorem CategoryTheory.Mon.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : Mon C} (f : M.Hom N) (g : N.Hom O) : (comp f g).hom = CategoryStruct.comp f.hom g.hom

@[simp]

theorem CategoryTheory.AddMon.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N O : AddMon C} (f : M.Hom N) (g : N.Hom O) : (comp f g).hom = CategoryStruct.comp f.hom g.hom

@[implicit_reducible]

instance CategoryTheory.Mon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Category.{v₁, max u₁ v₁} (Mon C)

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Category.{v₁, max u₁ v₁} (AddMon C)

Equations

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

instance CategoryTheory.Mon.instIsMonHomHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (f : M ⟶ N) : IsMonHom f.hom

instance CategoryTheory.AddMon.instIsAddMonHomHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} (f : M ⟶ N) : IsAddMonHom f.hom

theorem CategoryTheory.Mon.Hom.ext' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} {f g : M ⟶ N} (w : f.hom = g.hom) : f = g

theorem CategoryTheory.AddMon.Hom.ext' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} {f g : M ⟶ N} (w : f.hom = g.hom) : f = g

theorem CategoryTheory.Mon.Hom.ext'_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} {f g : M ⟶ N} : f = g ↔ f.hom = g.hom

theorem CategoryTheory.AddMon.Hom.ext'_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} {f g : M ⟶ N} : f = g ↔ f.hom = g.hom

theorem CategoryTheory.Mon.hom_injective {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} : Function.Injective Hom.hom

theorem CategoryTheory.AddMon.hom_injective {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} : Function.Injective Hom.hom

@[simp]

theorem CategoryTheory.Mon.id_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Mon C) : (CategoryStruct.id M).hom = CategoryStruct.id M.X

@[simp]

theorem CategoryTheory.AddMon.id_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : AddMon C) : (CategoryStruct.id M).hom = CategoryStruct.id M.X

@[simp]

theorem CategoryTheory.Mon.comp_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N K : Mon C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

@[simp]

theorem CategoryTheory.AddMon.comp_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N K : AddMon C} (f : M ⟶ N) (g : N ⟶ K) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.Mon.comp_hom'_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N K : Mon C} (f : M ⟶ N) (g : N ⟶ K) {Z : C} (h : K.X ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp g.hom h)

theorem CategoryTheory.AddMon.comp_hom'_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N K : AddMon C} (f : M ⟶ N) (g : N ⟶ K) {Z : C} (h : K.X ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp g.hom h)

def CategoryTheory.Mon.forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (Mon C) C

The forgetful functor from monoid objects to the ambient category.

Equations

• CategoryTheory.Mon.forget C = { obj := fun (A : CategoryTheory.Mon C) => A.X, map := fun {X Y : CategoryTheory.Mon C} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

def CategoryTheory.AddMon.forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (AddMon C) C

The forgetful functor from additive monoid objects to the ambient category.

Equations

• CategoryTheory.AddMon.forget C = { obj := fun (A : CategoryTheory.AddMon C) => A.X, map := fun {X Y : CategoryTheory.AddMon C} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Mon.forget_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : Mon C} (f : X✝ ⟶ Y✝) : (forget C).map f = f.hom

@[simp]

theorem CategoryTheory.AddMon.forget_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) : (forget C).obj A = A.X

@[simp]

theorem CategoryTheory.Mon.forget_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) : (forget C).obj A = A.X

@[simp]

theorem CategoryTheory.AddMon.forget_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : AddMon C} (f : X✝ ⟶ Y✝) : (forget C).map f = f.hom

instance CategoryTheory.Mon.forget_faithful {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (forget C).Faithful

instance CategoryTheory.AddMon.forget_faithful {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (forget C).Faithful

instance CategoryTheory.Mon.instIsIsoHomOfMapForget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {A B : Mon C} (f : A ⟶ B) [e : IsIso ((forget C).map f)] : IsIso f.hom

instance CategoryTheory.AddMon.instIsIsoHomOfMapForget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {A B : AddMon C} (f : A ⟶ B) [e : IsIso ((forget C).map f)] : IsIso f.hom

instance CategoryTheory.Mon.instReflectsIsomorphismsForget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (forget C).ReflectsIsomorphisms

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

instance CategoryTheory.AddMon.instReflectsIsomorphismsForget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (forget C).ReflectsIsomorphisms

instance CategoryTheory.Mon.instIsIsoHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} {f : M ⟶ N} [IsIso f] : IsIso f.hom

instance CategoryTheory.AddMon.instIsIsoHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} {f : M ⟶ N} [IsIso f] : IsIso f.hom

def CategoryTheory.Mon.mkIso' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] : { X := M, mon := inst✝ } ≅ { X := N, mon := inst✝¹ }

Construct an isomorphism of monoid objects by giving a monoid isomorphism between the underlying objects.

Equations

• CategoryTheory.Mon.mkIso' e = { hom := { hom := e.hom, isMonHom_hom := inst✝ }, inv := { hom := e.inv, isMonHom_hom := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def CategoryTheory.AddMon.mkIso' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] (e : M ≅ N) [IsAddMonHom e.hom] : { X := M, addMon := inst✝ } ≅ { X := N, addMon := inst✝¹ }

Construct an isomorphism of additive monoid objects by giving a additive monoid isomorphism between the underlying objects.

Equations

• CategoryTheory.AddMon.mkIso' e = { hom := { hom := e.hom, isAddMonHom_hom := inst✝ }, inv := { hom := e.inv, isAddMonHom_hom := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Mon.mkIso'_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] : (mkIso' e).inv.hom = e.inv

@[simp]

theorem CategoryTheory.AddMon.mkIso'_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] (e : M ≅ N) [IsAddMonHom e.hom] : (mkIso' e).hom.hom = e.hom

@[simp]

theorem CategoryTheory.AddMon.mkIso'_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [AddMonObj M] [AddMonObj N] (e : M ≅ N) [IsAddMonHom e.hom] : (mkIso' e).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Mon.mkIso'_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : C} [MonObj M] [MonObj N] (e : M ≅ N) [IsMonHom e.hom] : (mkIso' e).hom.hom = e.hom

@[reducible, inline]

abbrev CategoryTheory.Mon.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) : M ≅ N

Construct an isomorphism of monoid objects by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.

Equations

• CategoryTheory.Mon.mkIso e one_f mul_f = CategoryTheory.Mon.mkIso' e

@[reducible, inline]

abbrev CategoryTheory.AddMon.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} (e : M.X ≅ N.X) (zero_f : CategoryStruct.comp AddMonObj.zero e.hom = AddMonObj.zero := by cat_disch) (add_f : CategoryStruct.comp AddMonObj.add e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) AddMonObj.add := by cat_disch) : M ≅ N

Construct an isomorphism of additive monoid objects by giving an isomorphism between the underlying objects and checking compatibility with zero and addition only in the forward direction.

Equations

• CategoryTheory.AddMon.mkIso e one_f mul_f = CategoryTheory.AddMon.mkIso' e

@[simp]

theorem CategoryTheory.Mon.mkIso_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) : (mkIso e one_f mul_f).hom.hom = e.hom

@[simp]

theorem CategoryTheory.AddMon.mkIso_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} (e : M.X ≅ N.X) (zero_f : CategoryStruct.comp AddMonObj.zero e.hom = AddMonObj.zero := by cat_disch) (add_f : CategoryStruct.comp AddMonObj.add e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) AddMonObj.add := by cat_disch) : (mkIso e zero_f add_f).hom.hom = e.hom

@[simp]

theorem CategoryTheory.AddMon.mkIso_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : AddMon C} (e : M.X ≅ N.X) (zero_f : CategoryStruct.comp AddMonObj.zero e.hom = AddMonObj.zero := by cat_disch) (add_f : CategoryStruct.comp AddMonObj.add e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) AddMonObj.add := by cat_disch) : (mkIso e zero_f add_f).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Mon.mkIso_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M N : Mon C} (e : M.X ≅ N.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) : (mkIso e one_f mul_f).inv.hom = e.inv

@[implicit_reducible]

instance CategoryTheory.Mon.uniqueHomFromTrivial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) : Unique (trivial C ⟶ A)

Equations

• A.uniqueHomFromTrivial = { default := { hom := CategoryTheory.MonObj.one, isMonHom_hom := ⋯ }, uniq := ⋯ }

@[implicit_reducible]

instance CategoryTheory.AddMon.uniqueHomFromTrivial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) : Unique (trivial C ⟶ A)

Equations

• A.uniqueHomFromTrivial = { default := { hom := CategoryTheory.AddMonObj.zero, isAddMonHom_hom := ⋯ }, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Mon.uniqueHomFromTrivial_default_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) : default.hom = MonObj.one

@[simp]

theorem CategoryTheory.AddMon.uniqueHomFromTrivial_default_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) : default.hom = AddMonObj.zero

instance CategoryTheory.Mon.instHasInitial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Limits.HasInitial (Mon C)

instance CategoryTheory.AddMon.instHasInitial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Limits.HasInitial (AddMon C)

@[implicit_reducible]

instance CategoryTheory.Mon.monMonoidalStruct {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : MonoidalCategoryStruct (Mon C)

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMon.monMonoidalStruct {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : MonoidalCategoryStruct (AddMon C)

Equations

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

@[simp]

theorem CategoryTheory.AddMon.monMonoidalStruct_tensorObj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : AddMon C) : (MonoidalCategoryStruct.tensorObj M N).X = MonoidalCategoryStruct.tensorObj M.X N.X

@[simp]

theorem CategoryTheory.Mon.monMonoidalStruct_tensorObj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : Mon C) : (MonoidalCategoryStruct.tensorObj M N).X = MonoidalCategoryStruct.tensorObj M.X N.X

@[simp]

theorem CategoryTheory.Mon.monMonoidalStruct_tensorHom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : Mon C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (MonoidalCategoryStruct.tensorHom f g).hom = MonoidalCategoryStruct.tensorHom f.hom g.hom

@[simp]

theorem CategoryTheory.AddMon.monMonoidalStruct_tensorHom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : AddMon C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (MonoidalCategoryStruct.tensorHom f g).hom = MonoidalCategoryStruct.tensorHom f.hom g.hom

@[simp]

theorem CategoryTheory.Mon.tensorUnit_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (MonoidalCategoryStruct.tensorUnit (Mon C)).X = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.AddMon.tensorAddUnit_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (MonoidalCategoryStruct.tensorUnit (AddMon C)).X = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.Mon.tensorUnit_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : MonObj.one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.AddMon.tensorAddUnit_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : AddMonObj.zero = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.tensorUnit_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : MonObj.mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem CategoryTheory.AddMon.tensorAddUnit_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : AddMonObj.add = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem CategoryTheory.Mon.tensorObj_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Mon C) : MonObj.one = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one)

@[simp]

theorem CategoryTheory.AddMon.tensorObj_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : AddMon C) : AddMonObj.zero = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom AddMonObj.zero AddMonObj.zero)

@[simp]

theorem CategoryTheory.Mon.tensorObj_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Mon C) : MonObj.mul = CategoryStruct.comp (MonoidalCategory.tensorμ X.X Y.X X.X Y.X) (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)

@[simp]

theorem CategoryTheory.AddMon.tensorObj_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : AddMon C) : AddMonObj.add = CategoryStruct.comp (MonoidalCategory.tensorμ X.X Y.X X.X Y.X) (MonoidalCategoryStruct.tensorHom AddMonObj.add AddMonObj.add)

@[simp]

theorem CategoryTheory.Mon.whiskerLeft_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y : Mon C} (f : X ⟶ Y) (Z : Mon C) : (MonoidalCategoryStruct.whiskerRight f Z).hom = MonoidalCategoryStruct.whiskerRight f.hom Z.X

@[simp]

theorem CategoryTheory.AddMon.whiskerLeft_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y : AddMon C} (f : X ⟶ Y) (Z : AddMon C) : (MonoidalCategoryStruct.whiskerRight f Z).hom = MonoidalCategoryStruct.whiskerRight f.hom Z.X

@[simp]

theorem CategoryTheory.Mon.whiskerRight_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Mon C) {Y Z : Mon C} (f : Y ⟶ Z) : (MonoidalCategoryStruct.whiskerLeft X f).hom = MonoidalCategoryStruct.whiskerLeft X.X f.hom

@[simp]

theorem CategoryTheory.AddMon.whiskerRight_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : AddMon C) {Y Z : AddMon C} (f : Y ⟶ Z) : (MonoidalCategoryStruct.whiskerLeft X f).hom = MonoidalCategoryStruct.whiskerLeft X.X f.hom

@[simp]

theorem CategoryTheory.Mon.leftUnitor_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Mon C) : (MonoidalCategoryStruct.leftUnitor X).hom.hom = (MonoidalCategoryStruct.leftUnitor X.X).hom

@[simp]

theorem CategoryTheory.AddMon.leftUnitor_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : AddMon C) : (MonoidalCategoryStruct.leftUnitor X).hom.hom = (MonoidalCategoryStruct.leftUnitor X.X).hom

@[simp]

theorem CategoryTheory.Mon.leftUnitor_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Mon C) : (MonoidalCategoryStruct.leftUnitor X).inv.hom = (MonoidalCategoryStruct.leftUnitor X.X).inv

@[simp]

theorem CategoryTheory.AddMon.leftUnitor_neg_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : AddMon C) : (MonoidalCategoryStruct.leftUnitor X).inv.hom = (MonoidalCategoryStruct.leftUnitor X.X).inv

@[simp]

theorem CategoryTheory.Mon.rightUnitor_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Mon C) : (MonoidalCategoryStruct.rightUnitor X).hom.hom = (MonoidalCategoryStruct.rightUnitor X.X).hom

@[simp]

theorem CategoryTheory.AddMon.rightUnitor_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : AddMon C) : (MonoidalCategoryStruct.rightUnitor X).hom.hom = (MonoidalCategoryStruct.rightUnitor X.X).hom

@[simp]

theorem CategoryTheory.Mon.rightUnitor_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : Mon C) : (MonoidalCategoryStruct.rightUnitor X).inv.hom = (MonoidalCategoryStruct.rightUnitor X.X).inv

@[simp]

theorem CategoryTheory.AddMon.rightUnitor_neg_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : AddMon C) : (MonoidalCategoryStruct.rightUnitor X).inv.hom = (MonoidalCategoryStruct.rightUnitor X.X).inv

@[simp]

theorem CategoryTheory.Mon.associator_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y Z : Mon C) : (MonoidalCategoryStruct.associator X Y Z).hom.hom = (MonoidalCategoryStruct.associator X.X Y.X Z.X).hom

@[simp]

theorem CategoryTheory.AddMon.associator_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y Z : AddMon C) : (MonoidalCategoryStruct.associator X Y Z).hom.hom = (MonoidalCategoryStruct.associator X.X Y.X Z.X).hom

@[simp]

theorem CategoryTheory.Mon.associator_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y Z : Mon C) : (MonoidalCategoryStruct.associator X Y Z).inv.hom = (MonoidalCategoryStruct.associator X.X Y.X Z.X).inv

@[simp]

theorem CategoryTheory.AddMon.associator_neg_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y Z : AddMon C) : (MonoidalCategoryStruct.associator X Y Z).inv.hom = (MonoidalCategoryStruct.associator X.X Y.X Z.X).inv

@[simp]

theorem CategoryTheory.Mon.tensor_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : Mon C) : MonObj.one = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one)

@[simp]

theorem CategoryTheory.AddMon.tensor_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : AddMon C) : AddMonObj.zero = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom AddMonObj.zero AddMonObj.zero)

@[simp]

theorem CategoryTheory.Mon.tensor_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : Mon C) : MonObj.mul = CategoryStruct.comp (MonoidalCategory.tensorμ M.X N.X M.X N.X) (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)

@[simp]

theorem CategoryTheory.AddMon.tensor_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M N : AddMon C) : AddMonObj.add = CategoryStruct.comp (MonoidalCategory.tensorμ M.X N.X M.X N.X) (MonoidalCategoryStruct.tensorHom AddMonObj.add AddMonObj.add)

@[implicit_reducible]

instance CategoryTheory.Mon.monMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : MonoidalCategory (Mon C)

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMon.monMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : MonoidalCategory (AddMon C)

Equations

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

@[implicit_reducible]

instance CategoryTheory.Mon.instMonObjTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] : MonObj (MonoidalCategoryStruct.tensorObj M N)

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMon.instAddMonObjTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [AddMonObj M] [AddMonObj N] : AddMonObj (MonoidalCategoryStruct.tensorObj M N)

Equations

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

theorem CategoryTheory.Mon.one_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] : MonObj.one = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one)

theorem CategoryTheory.Mon.mul_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [MonObj M] [MonObj N] : MonObj.mul = CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)

theorem CategoryTheory.AddMon.add_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [AddMonObj M] [AddMonObj N] : AddMonObj.add = CategoryStruct.comp (MonoidalCategory.tensorμ M N M N) (MonoidalCategoryStruct.tensorHom AddMonObj.add AddMonObj.add)

theorem CategoryTheory.AddMon.zero_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [AddMonObj M] [AddMonObj N] : AddMonObj.zero = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom AddMonObj.zero AddMonObj.zero)

@[implicit_reducible]

instance CategoryTheory.Mon.instMonoidalForget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (forget C).Monoidal

The forgetful functor from Mon C to C is monoidal when C is monoidal.

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMon.instMonoidalForget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (forget C).Monoidal

Equations

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

@[simp]

theorem CategoryTheory.Mon.forget_ε (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Functor.LaxMonoidal.ε (forget C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.AddMon.forget_ε (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Functor.LaxMonoidal.ε (forget C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.forget_η (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Functor.OplaxMonoidal.η (forget C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.AddMon.forget_η (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Functor.OplaxMonoidal.η (forget C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Mon.forget_μ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Mon C) : Functor.LaxMonoidal.μ (forget C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X Y.X)

@[simp]

theorem CategoryTheory.AddMon.forget_μ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : AddMon C) : Functor.LaxMonoidal.μ (forget C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X Y.X)

@[simp]

theorem CategoryTheory.Mon.forget_δ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : Mon C) : Functor.OplaxMonoidal.δ (forget C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X Y.X)

@[simp]

theorem CategoryTheory.AddMon.forget_δ (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X Y : AddMon C) : Functor.OplaxMonoidal.δ (forget C) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X Y.X)

We next show that if C is symmetric, then Mon C is braided, and indeed symmetric.

Note that Mon C is not braided in general when C is only braided.

The more interesting construction is the 2-category of monoids in C, bimodules between the monoids, and intertwiners between the bimodules.

When C is braided, that is a monoidal 2-category.

theorem CategoryTheory.MonObj.mul_braiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (X Y : C) [MonObj X] [MonObj Y] : CategoryStruct.comp mul (β_ X Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (β_ X Y).hom (β_ X Y).hom) mul

theorem CategoryTheory.AddMonObj.add_braiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (X Y : C) [AddMonObj X] [AddMonObj Y] : CategoryStruct.comp add (β_ X Y).hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (β_ X Y).hom (β_ X Y).hom) add

instance CategoryTheory.MonObj.instIsMonHomHomBraiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] {X Y : C} [MonObj X] [MonObj Y] : IsMonHom (β_ X Y).hom

instance CategoryTheory.AddMonObj.instIsAddMonHomHomBraiding {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] {X Y : C} [AddMonObj X] [AddMonObj Y] : IsAddMonHom (β_ X Y).hom

@[implicit_reducible]

instance CategoryTheory.Mon.instSymmetricCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] : SymmetricCategory (Mon C)

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMon.instSymmetricCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] : SymmetricCategory (AddMon C)

Equations

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

@[simp]

theorem CategoryTheory.Mon.braiding_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (M N : Mon C) : (β_ M N).hom.hom = (β_ M.X N.X).hom

@[simp]

theorem CategoryTheory.AddMon.braiding_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (M N : AddMon C) : (β_ M N).hom.hom = (β_ M.X N.X).hom

@[simp]

theorem CategoryTheory.Mon.braiding_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (M N : Mon C) : (β_ M N).inv.hom = (β_ M.X N.X).inv

@[simp]

theorem CategoryTheory.AddMon.braiding_neg_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] (M N : AddMon C) : (β_ M N).inv.hom = (β_ M.X N.X).inv

@[reducible, inline]

abbrev CategoryTheory.Functor.monObjObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] : MonObj (F.obj X)

The image of a monoid object under a lax monoidal functor is a monoid object.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Functor.addMonObjObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [AddMonObj X] : AddMonObj (F.obj X)

The image of an additive monoid object under a lax monoidal functor is an additive monoid object.

Equations

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

@[simp]

theorem CategoryTheory.Functor.obj.η_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] : MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)

@[simp]

theorem CategoryTheory.Functor.obj.ζ_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [AddMonObj X] : AddMonObj.zero = CategoryStruct.comp (LaxMonoidal.ε F) (F.map AddMonObj.zero)

theorem CategoryTheory.Functor.obj.η_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp MonObj.one h = CategoryStruct.comp (LaxMonoidal.ε F) (CategoryStruct.comp (F.map MonObj.one) h)

theorem CategoryTheory.Functor.obj.ζ_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [AddMonObj X] {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp AddMonObj.zero h = CategoryStruct.comp (LaxMonoidal.ε F) (CategoryStruct.comp (F.map AddMonObj.zero) h)

@[simp]

theorem CategoryTheory.Functor.obj.μ_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] : MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F X X) (F.map MonObj.mul)

@[simp]

theorem CategoryTheory.Functor.obj.σ_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [AddMonObj X] : AddMonObj.add = CategoryStruct.comp (LaxMonoidal.μ F X X) (F.map AddMonObj.add)

theorem CategoryTheory.Functor.obj.μ_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [MonObj X] {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp MonObj.mul h = CategoryStruct.comp (LaxMonoidal.μ F X X) (CategoryStruct.comp (F.map MonObj.mul) h)

theorem CategoryTheory.Functor.obj.σ_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X : C) [AddMonObj X] {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp AddMonObj.add h = CategoryStruct.comp (LaxMonoidal.μ F X X) (CategoryStruct.comp (F.map AddMonObj.add) h)

instance CategoryTheory.Functor.map.instIsMonHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X Y : C) [MonObj X] [MonObj Y] (f : X ⟶ Y) [IsMonHom f] : IsMonHom (F.map f)

instance CategoryTheory.Functor.map.instIsAddMonHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] (X Y : C) [AddMonObj X] [AddMonObj Y] (f : X ⟶ Y) [IsAddMonHom f] : IsAddMonHom (F.map f)

def CategoryTheory.Functor.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : Functor (Mon C) (Mon D)

A lax monoidal functor takes monoid objects to monoid objects.

That is, a lax monoidal functor F : C ⥤ D induces a functor Mon C ⥤ Mon D.

Equations

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

def CategoryTheory.Functor.mapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] : Functor (AddMon C) (AddMon D)

A lax monoidal functor takes additive monoid objects to additive monoid objects.

That is, a lax monoidal functor F : C ⥤ D induces a functor AddMon C ⥤ AddMon D.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapMon_obj_mon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (A : Mon C) : MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map MonObj.mul)

@[simp]

theorem CategoryTheory.Functor.mapMon_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (A : Mon C) : (F.mapMon.obj A).X = F.obj A.X

@[simp]

theorem CategoryTheory.Functor.mapMon_obj_mon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (A : Mon C) : MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)

@[simp]

theorem CategoryTheory.Functor.mapAddMon_obj_addMon_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (A : AddMon C) : AddMonObj.zero = CategoryStruct.comp (LaxMonoidal.ε F) (F.map AddMonObj.zero)

@[simp]

theorem CategoryTheory.Functor.mapAddMon_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (A : AddMon C) : (F.mapAddMon.obj A).X = F.obj A.X

@[simp]

theorem CategoryTheory.Functor.mapAddMon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X✝ Y✝ : AddMon C} (f : X✝ ⟶ Y✝) : (F.mapAddMon.map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapAddMon_obj_addMon_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] (A : AddMon C) : AddMonObj.add = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map AddMonObj.add)

@[simp]

theorem CategoryTheory.Functor.mapMon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [F.LaxMonoidal] {X✝ Y✝ : Mon C} (f : X✝ ⟶ Y✝) : (F.mapMon.map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.id_mapMon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) : MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one

@[simp]

theorem CategoryTheory.Functor.id_mapAddMon_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : AddMon C) : AddMonObj.zero = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) AddMonObj.zero

@[simp]

theorem CategoryTheory.Functor.id_mapMon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) : MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X X.X)) MonObj.mul

@[simp]

theorem CategoryTheory.Functor.id_mapAddMon_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : AddMon C) : AddMonObj.add = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj X.X X.X)) AddMonObj.add

@[simp]

theorem CategoryTheory.Functor.comp_mapMon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : Mon C) : MonObj.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map MonObj.one)

@[simp]

theorem CategoryTheory.Functor.comp_mapAddMon_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : AddMon C) : AddMonObj.zero = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map AddMonObj.zero)

@[simp]

theorem CategoryTheory.Functor.comp_mapMon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : Mon C) : MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) X.X X.X) ((F.comp G).map MonObj.mul)

@[simp]

theorem CategoryTheory.Functor.comp_mapAddMon_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : AddMon C) : AddMonObj.add = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) X.X X.X) ((F.comp G).map AddMonObj.add)

def CategoryTheory.Functor.mapMonIdIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (Functor.id C).mapMon ≅ Functor.id (Mon C)

The identity functor is also the identity on monoid objects.

Equations

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

def CategoryTheory.Functor.mapAddMonIdIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : (Functor.id C).mapAddMon ≅ Functor.id (AddMon C)

The identity functor is also the identity on additive monoid objects.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapMonIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) : (mapMonIdIso.hom.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Functor.mapMonIdIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) : (mapMonIdIso.inv.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Functor.mapAddMonIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : AddMon C) : (mapAddMonIdIso.hom.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Functor.mapAddMonIdIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : AddMon C) : (mapAddMonIdIso.inv.app X).hom = CategoryStruct.id X.X

def CategoryTheory.Functor.mapMonCompIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] : (F.comp G).mapMon ≅ F.mapMon.comp G.mapMon

The composition functor is also the composition on monoid objects.

Equations

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

def CategoryTheory.Functor.mapAddMonCompIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] : (F.comp G).mapAddMon ≅ F.mapAddMon.comp G.mapAddMon

The composition functor is also the composition on additive monoid objects.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapMonCompIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : Mon C) : (mapMonCompIso.hom.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

@[simp]

theorem CategoryTheory.Functor.mapAddMonCompIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : AddMon C) : (mapAddMonCompIso.hom.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

@[simp]

theorem CategoryTheory.Functor.mapAddMonCompIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : AddMon C) : (mapAddMonCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

@[simp]

theorem CategoryTheory.Functor.mapMonCompIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [MonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.LaxMonoidal] [G.LaxMonoidal] (X : Mon C) : (mapMonCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

instance CategoryTheory.Functor.Faithful.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] [F.Faithful] : F.mapMon.Faithful

instance CategoryTheory.Functor.Faithful.mapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] [F.Faithful] : F.mapAddMon.Faithful

def CategoryTheory.Functor.mapMonNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [NatTrans.IsMonoidal f] : F.mapMon ⟶ F'.mapMon

Natural transformations between functors lift to monoid objects.

Equations

• CategoryTheory.Functor.mapMonNatTrans f = { app := fun (X : CategoryTheory.Mon C) => CategoryTheory.Mon.Hom.mk' (f.app X.X) ⋯ ⋯, naturality := ⋯ }

def CategoryTheory.Functor.mapAddMonNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [NatTrans.IsMonoidal f] : F.mapAddMon ⟶ F'.mapAddMon

Natural transformations between functors lift to additive monoid objects.

Equations

• CategoryTheory.Functor.mapAddMonNatTrans f = { app := fun (X : CategoryTheory.AddMon C) => CategoryTheory.AddMon.Hom.mk' (f.app X.X) ⋯ ⋯, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapAddMonNatTrans_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [NatTrans.IsMonoidal f] (X : AddMon C) : ((mapAddMonNatTrans f).app X).hom = f.app X.X

@[simp]

theorem CategoryTheory.Functor.mapMonNatTrans_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (f : F ⟶ F') [NatTrans.IsMonoidal f] (X : Mon C) : ((mapMonNatTrans f).app X).hom = f.app X.X

def CategoryTheory.Functor.mapMonNatIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] : F.mapMon ≅ F'.mapMon

Natural isomorphisms between functors lift to monoid objects.

Equations

• CategoryTheory.Functor.mapMonNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Mon C) => CategoryTheory.Mon.mkIso (e.app X.X) ⋯ ⋯) ⋯

def CategoryTheory.Functor.mapAddMonNatIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] : F.mapAddMon ≅ F'.mapAddMon

Natural isomorphisms between functors lift to additive monoid objects.

Equations

• CategoryTheory.Functor.mapAddMonNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.AddMon C) => CategoryTheory.AddMon.mkIso (e.app X.X) ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.mapMonNatIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : Mon C) : ((mapMonNatIso e).inv.app X).hom = e.inv.app X.X

@[simp]

theorem CategoryTheory.Functor.mapAddMonNatIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : AddMon C) : ((mapAddMonNatIso e).hom.app X).hom = e.hom.app X.X

@[simp]

theorem CategoryTheory.Functor.mapAddMonNatIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : AddMon C) : ((mapAddMonNatIso e).inv.app X).hom = e.inv.app X.X

@[simp]

theorem CategoryTheory.Functor.mapMonNatIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' : Functor C D} [F.LaxMonoidal] [F'.LaxMonoidal] (e : F ≅ F') [NatTrans.IsMonoidal e.hom] (X : Mon C) : ((mapMonNatIso e).hom.app X).hom = e.hom.app X.X

instance CategoryTheory.Functor.instIsMonHomε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] : IsMonHom (LaxMonoidal.ε F)

instance CategoryTheory.Functor.instIsAddMonHomε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.LaxMonoidal] : IsAddMonHom (LaxMonoidal.ε F)

@[reducible, inline]

abbrev CategoryTheory.Functor.FullyFaithful.monObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [MonObj (F.obj X)] : MonObj X

Pullback a monoid object along a fully faithful oplax monoidal functor.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Functor.FullyFaithful.addMonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [AddMonObj (F.obj X)] : AddMonObj X

Pullback an additive monoid object along a fully faithful oplax monoidal functor.

Equations

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

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.monObj_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [MonObj (F.obj X)] : MonObj.mul = hF.preimage (CategoryStruct.comp (OplaxMonoidal.δ F X X) MonObj.mul)

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.addMonObj_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [AddMonObj (F.obj X)] : AddMonObj.zero = hF.preimage (CategoryStruct.comp (OplaxMonoidal.η F) AddMonObj.zero)

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.monObj_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [MonObj (F.obj X)] : MonObj.one = hF.preimage (CategoryStruct.comp (OplaxMonoidal.η F) MonObj.one)

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.addMonObj_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C) [AddMonObj (F.obj X)] : AddMonObj.add = hF.preimage (CategoryStruct.comp (OplaxMonoidal.δ F X X) AddMonObj.add)

instance CategoryTheory.Functor.Full.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] [F.Full] [F.Faithful] : F.mapMon.Full

instance CategoryTheory.Functor.Full.mapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] [F.Full] [F.Faithful] : F.mapAddMon.Full

instance CategoryTheory.Functor.FullyFaithful.isAddMonHom_preimage {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : C} [AddMonObj X] [AddMonObj Y] (f : F.obj X ⟶ F.obj Y) [IsAddMonHom f] : IsAddMonHom (hF.preimage f)

instance CategoryTheory.Functor.FullyFaithful.isMonHom_preimage {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : C} [MonObj X] [MonObj Y] (f : F.obj X ⟶ F.obj Y) [IsMonHom f] : IsMonHom (hF.preimage f)

def CategoryTheory.Functor.FullyFaithful.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) : F.mapMon.FullyFaithful

If F : C ⥤ D is a fully faithful monoidal functor, then F.mapMon : Mon C ⥤ Mon D is fully faithful too.

Equations

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

def CategoryTheory.Functor.FullyFaithful.mapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) : F.mapAddMon.FullyFaithful

If F : C ⥤ D is a fully faithful monoidal functor, then F.mapAddMon : AddMon C ⥤ AddMon D is fully faithful too.

Equations

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

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : Mon C} (f : F.mapMon.obj X ⟶ F.mapMon.obj Y) : (hF.mapMon.preimage f).hom = hF.preimage f.hom

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mapAddMon_preimage_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) {X Y : AddMon C} (f : F.mapAddMon.obj X ⟶ F.mapAddMon.obj Y) : (hF.mapAddMon.preimage f).hom = hF.preimage f.hom

@[simp]

theorem CategoryTheory.Functor.essImage_mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {M : Mon D} : F.mapMon.essImage M ↔ F.essImage M.X

The essential image of a fully faithful functor between cartesian-monoidal categories is the same on monoid objects as on objects.

@[simp]

theorem CategoryTheory.Functor.essImage_mapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [F.Monoidal] [F.Full] [F.Faithful] {M : AddMon D} : F.mapAddMon.essImage M ↔ F.essImage M.X

The essential image of a fully faithful functor between cartesian-monoidal categories is the same on additive monoid objects as on objects.

instance CategoryTheory.Functor.instIsMonHomμ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.LaxBraided] (M N : C) [MonObj M] [MonObj N] : IsMonHom (LaxMonoidal.μ F M N)

instance CategoryTheory.Functor.instIsAddMonHomμ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.LaxBraided] (M N : C) [AddMonObj M] [AddMonObj N] : IsAddMonHom (LaxMonoidal.μ F M N)

@[implicit_reducible]

instance CategoryTheory.Functor.instLaxMonoidalMonMapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.LaxBraided] : F.mapMon.LaxMonoidal

Equations

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

@[implicit_reducible]

instance CategoryTheory.Functor.instLaxMonoidalMonMapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.LaxBraided] : F.mapAddMon.LaxMonoidal

Equations

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

@[implicit_reducible]

instance CategoryTheory.Functor.instMonoidalMonMapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.Braided] : F.mapMon.Monoidal

Equations

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

@[implicit_reducible]

instance CategoryTheory.Functor.instMonoidalMonMapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] [F.Braided] : F.mapAddMon.Monoidal

Equations

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

@[implicit_reducible]

instance CategoryTheory.Functor.instLaxBraidedMonMapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [SymmetricCategory C] [SymmetricCategory D] [F.LaxBraided] : F.mapMon.LaxBraided

Equations

• CategoryTheory.Functor.instLaxBraidedMonMapMon = { toLaxMonoidal := F.instLaxMonoidalMonMapMon, braided := ⋯ }

@[implicit_reducible]

instance CategoryTheory.Functor.instLaxBraidedMonMapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [SymmetricCategory C] [SymmetricCategory D] [F.LaxBraided] : F.mapAddMon.LaxBraided

Equations

• CategoryTheory.Functor.instLaxBraidedMonMapAddMon = { toLaxMonoidal := F.instLaxMonoidalMonMapAddMon, braided := ⋯ }

@[implicit_reducible]

instance CategoryTheory.Functor.instBraidedMonMapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [SymmetricCategory C] [SymmetricCategory D] [F.Braided] : F.mapMon.Braided

Equations

• CategoryTheory.Functor.instBraidedMonMapMon = { toMonoidal := F.instMonoidalMonMapMon, braided := ⋯ }

@[implicit_reducible]

instance CategoryTheory.Functor.instBraidedMonMapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} [SymmetricCategory C] [SymmetricCategory D] [F.Braided] : F.mapAddMon.Braided

Equations

• CategoryTheory.Functor.instBraidedMonMapAddMon = { toMonoidal := F.instMonoidalMonMapAddMon, braided := ⋯ }

def CategoryTheory.Functor.mapMonFunctor (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] : Functor (LaxMonoidalFunctor C D) (Functor (Mon C) (Mon D))

mapMon is functorial in the lax monoidal functor.

Equations

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

def CategoryTheory.Functor.mapAddMonFunctor (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] : Functor (LaxMonoidalFunctor C D) (Functor (AddMon C) (AddMon D))

mapAddMon is functorial in the lax monoidal functor.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapMonFunctor_map_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] {X✝ Y✝ : LaxMonoidalFunctor C D} (α : X✝ ⟶ Y✝) (A : Mon C) : (((mapMonFunctor C D).map α).app A).hom = α.hom.app A.X

@[simp]

theorem CategoryTheory.Functor.mapMonFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] (F : LaxMonoidalFunctor C D) : (mapMonFunctor C D).obj F = F.mapMon

@[simp]

theorem CategoryTheory.Functor.mapAddMonFunctor_map_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] {X✝ Y✝ : LaxMonoidalFunctor C D} (α : X✝ ⟶ Y✝) (A : AddMon C) : (((mapAddMonFunctor C D).map α).app A).hom = α.hom.app A.X

@[simp]

theorem CategoryTheory.Functor.mapAddMonFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory D] (F : LaxMonoidalFunctor C D) : (mapAddMonFunctor C D).obj F = F.mapAddMon

def CategoryTheory.Adjunction.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : F.mapMon ⊣ G.mapMon

An adjunction of monoidal functors lifts to an adjunction of their lifts to monoid objects.

Equations

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

def CategoryTheory.Adjunction.mapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : F.mapAddMon ⊣ G.mapAddMon

An adjunction of monoidal functors lifts to an adjunction of their lifts to additive monoid objects.

Equations

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

@[simp]

theorem CategoryTheory.Adjunction.mapMon_unit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : a.mapMon.unit = CategoryStruct.comp Functor.mapMonIdIso.inv (CategoryStruct.comp (Functor.mapMonNatTrans a.unit) Functor.mapMonCompIso.hom)

@[simp]

theorem CategoryTheory.Adjunction.mapAddMon_unit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : a.mapAddMon.unit = CategoryStruct.comp Functor.mapAddMonIdIso.inv (CategoryStruct.comp (Functor.mapAddMonNatTrans a.unit) Functor.mapAddMonCompIso.hom)

@[simp]

theorem CategoryTheory.Adjunction.mapMon_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : a.mapMon.counit = CategoryStruct.comp Functor.mapMonCompIso.inv (CategoryStruct.comp (Functor.mapMonNatTrans a.counit) Functor.mapMonIdIso.hom)

@[simp]

theorem CategoryTheory.Adjunction.mapAddMon_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal] : a.mapAddMon.counit = CategoryStruct.comp Functor.mapAddMonCompIso.inv (CategoryStruct.comp (Functor.mapAddMonNatTrans a.counit) Functor.mapAddMonIdIso.hom)

def CategoryTheory.Equivalence.mapMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : Mon C ≌ Mon D

An equivalence of categories lifts to an equivalence of their monoid objects.

Equations

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

def CategoryTheory.Equivalence.mapAddMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : AddMon C ≌ AddMon D

An equivalence of categories lifts to an equivalence of their additive monoid objects.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.mapMon_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapMon.functor = e.functor.mapMon

@[simp]

theorem CategoryTheory.Equivalence.mapAddMon_functor {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapAddMon.functor = e.functor.mapAddMon

@[simp]

theorem CategoryTheory.Equivalence.mapMon_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapMon.unitIso = Functor.mapMonIdIso.symm ≪≫ Functor.mapMonNatIso e.unitIso ≪≫ Functor.mapMonCompIso

@[simp]

theorem CategoryTheory.Equivalence.mapAddMon_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapAddMon.inverse = e.inverse.mapAddMon

@[simp]

theorem CategoryTheory.Equivalence.mapMon_inverse {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapMon.inverse = e.inverse.mapMon

@[simp]

theorem CategoryTheory.Equivalence.mapAddMon_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapAddMon.counitIso = Functor.mapAddMonCompIso.symm ≪≫ Functor.mapAddMonNatIso e.counitIso ≪≫ Functor.mapAddMonIdIso

@[simp]

theorem CategoryTheory.Equivalence.mapAddMon_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapAddMon.unitIso = Functor.mapAddMonIdIso.symm ≪≫ Functor.mapAddMonNatIso e.unitIso ≪≫ Functor.mapAddMonCompIso

@[simp]

theorem CategoryTheory.Equivalence.mapMon_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] : e.mapMon.counitIso = Functor.mapMonCompIso.symm ≪≫ Functor.mapMonNatIso e.counitIso ≪≫ Functor.mapMonIdIso

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (Mon C)

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

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

def CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (AddMon C)

Implementation of AddMon.equivLaxMonoidalFunctorPUnit.

Equations

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

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C} (α : X✝ ⟶ Y✝) : (laxMonoidalToMon C).map α = ((Functor.mapMonFunctor (Discrete PUnit.{w + 1}) C).map α).app (trivial (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) : (laxMonoidalToMon C).obj F = F.mapMon.obj (trivial (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) : (laxMonoidalToAddMon C).obj F = F.mapAddMon.obj (trivial (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon_map (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C} (α : X✝ ⟶ Y✝) : (laxMonoidalToAddMon C).map α = ((Functor.mapAddMonFunctor (Discrete PUnit.{w + 1}) C).map α).app (trivial (Discrete PUnit.{w + 1}))

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) : Functor (Discrete PUnit.{w + 1}) C

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

• CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A = (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{?u.17 + 1})).obj A.X

def CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) : Functor (Discrete PUnit.{w + 1}) C

Implementation of AddMon.equivLaxMonoidalFunctorPUnit.

Equations

• CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A = (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{?u.17 + 1})).obj A.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_map {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) {X✝ Y✝ : Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) : (monToLaxMonoidalObj A).map x✝ = CategoryStruct.id A.X

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) (x✝ : Discrete PUnit.{w + 1}) : (addMonToLaxMonoidalObj A).obj x✝ = A.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) (x✝ : Discrete PUnit.{w + 1}) : (monToLaxMonoidalObj A).obj x✝ = A.X

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_map {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) {X✝ Y✝ : Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) : (addMonToLaxMonoidalObj A).map x✝ = CategoryStruct.id A.X

@[implicit_reducible]

instance CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) : (monToLaxMonoidalObj A).LaxMonoidal

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) : (addMonToLaxMonoidalObj A).LaxMonoidal

Equations

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

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) : Functor.LaxMonoidal.ε (monToLaxMonoidalObj A) = MonObj.one

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) : Functor.LaxMonoidal.ε (addMonToLaxMonoidalObj A) = AddMonObj.zero

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) (X Y : Discrete PUnit.{u_1 + 1}) : Functor.LaxMonoidal.μ (monToLaxMonoidalObj A) X Y = MonObj.mul

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) (X Y : Discrete PUnit.{u_1 + 1}) : Functor.LaxMonoidal.μ (addMonToLaxMonoidalObj A) X Y = AddMonObj.add

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (Mon C) (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C)

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

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

def CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor (AddMon C) (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C)

Implementation of AddMon.equivLaxMonoidalFunctorPUnit.

Equations

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

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) : (addMonToLaxMonoidal C).obj A = LaxMonoidalFunctor.of (addMonToLaxMonoidalObj A)

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : Mon C} (f : X✝ ⟶ Y✝) (x✝ : Discrete PUnit.{w + 1}) : ((monToLaxMonoidal C).map f).hom.app x✝ = f.hom

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_map_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : AddMon C} (f : X✝ ⟶ Y✝) (x✝ : Discrete PUnit.{w + 1}) : ((addMonToLaxMonoidal C).map f).hom.app x✝ = f.hom

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) : (monToLaxMonoidal C).obj A = LaxMonoidalFunctor.of (monToLaxMonoidalObj A)

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor.id (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) ≅ (laxMonoidalToMon C).comp (monToLaxMonoidal C)

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

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

def CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : Functor.id (LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) ≅ (laxMonoidalToAddMon C).comp (addMonToLaxMonoidal C)

Implementation of AddMon.equivLaxMonoidalFunctorPUnit.

Equations

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

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) : ((unitIso C).hom.app X).hom.app X✝ = CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) : ((unitIso C).inv.app X).hom.app X✝ = CategoryStruct.id (X.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1})))

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso_inv_app_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) : ((addUnitIso C).inv.app X).hom.app X✝ = CategoryStruct.id (X.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1})))

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso_hom_app_hom_app (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) : ((addUnitIso C).hom.app X).hom.app X✝ = CategoryStruct.id (X.obj X✝)

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) : (((monToLaxMonoidal C).comp (laxMonoidalToMon C)).obj F).X ≅ ((Functor.id (Mon C)).obj F).X

Auxiliary definition for counitIso.

Equations

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

def CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : AddMon C) : (((addMonToLaxMonoidal C).comp (laxMonoidalToAddMon C)).obj F).X ≅ ((Functor.id (AddMon C)).obj F).X

Auxiliary definition for counitIso.

Equations

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

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) : (counitIsoAux C F).inv = CategoryStruct.id F.X

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : AddMon C) : (counitIsoAux C F).inv = CategoryStruct.id F.X

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : AddMon C) : (counitIsoAux C F).hom = CategoryStruct.id F.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) : (counitIsoAux C F).hom = CategoryStruct.id F.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) : MonObj.one = CategoryStruct.comp MonObj.one (CategoryStruct.id F.X)

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_laxMonoidalToAddMon_obj_zero (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : AddMon C) : AddMonObj.zero = CategoryStruct.comp AddMonObj.zero (CategoryStruct.id F.X)

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) : MonObj.mul = CategoryStruct.comp MonObj.mul (CategoryStruct.id F.X)

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_laxMonoidalToAddMon_obj_add (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : AddMon C) : AddMonObj.add = CategoryStruct.comp AddMonObj.add (CategoryStruct.id F.X)

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : Mon C) : IsMonHom (counitIsoAux C F).hom

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.isAddMonHom_counitIsoAux (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (F : AddMon C) : IsAddMonHom (counitIsoAux C F).hom

def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : (monToLaxMonoidal C).comp (laxMonoidalToMon C) ≅ Functor.id (Mon C)

Implementation of Mon.equivLaxMonoidalFunctorPUnit.

Equations

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

def CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] : (addMonToLaxMonoidal C).comp (laxMonoidalToAddMon C) ≅ Functor.id (AddMon C)

Implementation of AddMon.equivLaxMonoidalFunctorPUnit.

Equations

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

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) : ((counitIso C).inv.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : AddMon C) : ((counitIso C).hom.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : AddMon C) : ((counitIso C).inv.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) : ((counitIso C).hom.app X).hom = CategoryStruct.id X.X

def CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C ≌ Mon C

Monoid objects in C are "just" lax monoidal functors from the trivial monoidal category to C.

Equations

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

def CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C ≌ AddMon C

Additive monoid objects in C are "just" lax monoidal functors from the trivial monoidal category to C.

Equations

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

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) (x✝ x✝¹ : Discrete PUnit.{w + 1}) : Functor.LaxMonoidal.μ (EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A) x✝ x✝¹ = AddMonObj.add

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C} (α : X✝ ⟶ Y✝) : (equivLaxMonoidalFunctorPUnit.functor.map α).hom = α.hom.app (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) : (equivLaxMonoidalFunctorPUnit.counitIso.inv.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_map {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) {X✝ Y✝ : Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) : (equivLaxMonoidalFunctorPUnit.inverse.obj A).map x✝ = CategoryStruct.id A.X

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_addMon_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) : AddMonObj.add = Functor.LaxMonoidal.μ F.toFunctor (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1})) (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : Mon C) : (equivLaxMonoidalFunctorPUnit.counitIso.hom.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) : Functor.LaxMonoidal.ε (EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) = MonObj.one

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C} (α : X✝ ⟶ Y✝) : (equivLaxMonoidalFunctorPUnit.functor.map α).hom = α.hom.app (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_addMon_zero {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) : AddMonObj.zero = Functor.LaxMonoidal.ε F.toFunctor

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : AddMon C) : (equivLaxMonoidalFunctorPUnit.counitIso.hom.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) : (equivLaxMonoidalFunctorPUnit.unitIso.inv.app X).hom.app X✝ = CategoryStruct.id (X.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1})))

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_counitIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : AddMon C) : (equivLaxMonoidalFunctorPUnit.counitIso.inv.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_map {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) {X✝ Y✝ : Discrete PUnit.{w + 1}} (x✝ : X✝ ⟶ Y✝) : (equivLaxMonoidalFunctorPUnit.inverse.obj A).map x✝ = CategoryStruct.id A.X

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) : (equivLaxMonoidalFunctorPUnit.functor.obj F).X = F.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_functor_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) : (equivLaxMonoidalFunctorPUnit.functor.obj F).X = F.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) : MonObj.one = Functor.LaxMonoidal.ε F.toFunctor

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) : (equivLaxMonoidalFunctorPUnit.unitIso.hom.app X).hom.app X✝ = CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : AddMon C} (f : X✝ ⟶ Y✝) (x✝ : Discrete PUnit.{w + 1}) : (equivLaxMonoidalFunctorPUnit.inverse.map f).hom.app x✝ = f.hom

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor_obj_mon_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (F : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) : MonObj.mul = Functor.LaxMonoidal.μ F.toFunctor (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1})) (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1}))

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_hom_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) : (equivLaxMonoidalFunctorPUnit.unitIso.hom.app X).hom.app X✝ = CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) (x✝ x✝¹ : Discrete PUnit.{w + 1}) : Functor.LaxMonoidal.μ (EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A) x✝ x✝¹ = MonObj.mul

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) (x✝ : Discrete PUnit.{w + 1}) : (equivLaxMonoidalFunctorPUnit.inverse.obj A).obj x✝ = A.X

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso_inv_app_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (X : LaxMonoidalFunctor (Discrete PUnit.{w + 1}) C) (X✝ : Discrete PUnit.{w + 1}) : (equivLaxMonoidalFunctorPUnit.unitIso.inv.app X).hom.app X✝ = CategoryStruct.id (X.obj (MonoidalCategoryStruct.tensorUnit (Discrete PUnit.{w + 1})))

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_map_hom_app {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {X✝ Y✝ : Mon C} (f : X✝ ⟶ Y✝) (x✝ : Discrete PUnit.{w + 1}) : (equivLaxMonoidalFunctorPUnit.inverse.map f).hom.app x✝ = f.hom

@[simp]

theorem CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : AddMon C) : Functor.LaxMonoidal.ε (EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A) = AddMonObj.zero

@[simp]

theorem CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : Mon C) (x✝ : Discrete PUnit.{w + 1}) : (equivLaxMonoidalFunctorPUnit.inverse.obj A).obj x✝ = A.X

class CategoryTheory.IsCommAddMonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) [AddMonObj X] : Prop

Predicate for an additive monoid object to be commutative.

• add_comm : CategoryStruct.comp (β_ X X).hom AddMonObj.add = AddMonObj.add

class CategoryTheory.IsCommMonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) [MonObj X] : Prop

Predicate for a monoid object to be commutative.

• mul_comm : CategoryStruct.comp (β_ X X).hom MonObj.mul = MonObj.mul

@[simp]

theorem CategoryTheory.IsCommMonObj.mul_comm_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {inst✝² : BraidedCategory C} (X : C) {inst✝³ : MonObj X} [self : IsCommMonObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (β_ X X).hom (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp MonObj.mul h

@[simp]

theorem CategoryTheory.IsCommMonObj.mul_comm' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] : CategoryStruct.comp (β_ M M).inv MonObj.mul = MonObj.mul

@[simp]

theorem CategoryTheory.IsCommAddMonObj.add_comm' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] [BraidedCategory C] [IsCommAddMonObj M] : CategoryStruct.comp (β_ M M).inv AddMonObj.add = AddMonObj.add

@[simp]

theorem CategoryTheory.IsCommMonObj.mul_comm'_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (β_ M M).inv (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp MonObj.mul h

@[simp]

theorem CategoryTheory.IsCommAddMonObj.add_comm'_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] [BraidedCategory C] [IsCommAddMonObj M] {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (β_ M M).inv (CategoryStruct.comp AddMonObj.add h) = CategoryStruct.comp AddMonObj.add h

instance CategoryTheory.IsCommMonObj.instTensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : IsCommMonObj (MonoidalCategoryStruct.tensorUnit C)

instance CategoryTheory.IsCommAddMonObj.instTensorAddUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : IsCommAddMonObj (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.MonObj.mul_mul_mul_comm {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] : CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) mul

@[simp]

theorem CategoryTheory.AddMonObj.add_add_add_comm {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] [BraidedCategory C] [IsCommAddMonObj M] : CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom add add) add) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom add add) add

@[simp]

theorem CategoryTheory.AddMonObj.add_add_add_comm_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] [BraidedCategory C] [IsCommAddMonObj M] {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom add add) (CategoryStruct.comp add h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom add add) (CategoryStruct.comp add h)

@[simp]

theorem CategoryTheory.MonObj.mul_mul_mul_comm_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) (CategoryStruct.comp mul h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) (CategoryStruct.comp mul h)

@[simp]

theorem CategoryTheory.MonObj.mul_mul_mul_comm' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] : CategoryStruct.comp (MonoidalCategory.tensorδ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) mul) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) mul

@[simp]

theorem CategoryTheory.AddMonObj.add_add_add_comm' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] [BraidedCategory C] [IsCommAddMonObj M] : CategoryStruct.comp (MonoidalCategory.tensorδ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom add add) add) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom add add) add

@[simp]

theorem CategoryTheory.AddMonObj.add_add_add_comm'_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] [BraidedCategory C] [IsCommAddMonObj M] {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategory.tensorδ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom add add) (CategoryStruct.comp add h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom add add) (CategoryStruct.comp add h)

@[simp]

theorem CategoryTheory.MonObj.mul_mul_mul_comm'_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] [BraidedCategory C] [IsCommMonObj M] {Z : C} (h : M ⟶ Z) : CategoryStruct.comp (MonoidalCategory.tensorδ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) (CategoryStruct.comp mul h)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom mul mul) (CategoryStruct.comp mul h)

instance CategoryTheory.instIsCommMonObjTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] {M N : C} [MonObj M] [MonObj N] [IsCommMonObj M] [IsCommMonObj N] : IsCommMonObj (MonoidalCategoryStruct.tensorObj M N)

instance CategoryTheory.instIsCommAddMonObjTensorObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [SymmetricCategory C] {M N : C} [AddMonObj M] [AddMonObj N] [IsCommAddMonObj M] [IsCommAddMonObj N] : IsCommAddMonObj (MonoidalCategoryStruct.tensorObj M N)