class EGNO.MacLaneStrictness.MonoidalCategory.IsStrict (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : Prop

Definition 1.8.1: A monoidal category is strict if the associator and unitors are identity morphisms, i.e. (X ⊗ Y) ⊗ Z = X ⊗ (Y ⊗ Z), 𝟙_C ⊗ X = X, and X ⊗ 𝟙_C = X on the nose, with the structure isomorphisms equal to the corresponding eqToHom.

• tensorObj_assoc (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z = CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
• tensorUnit_left (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X = X
• tensorUnit_right (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = X
• associator_eqToHom (X Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = CategoryTheory.eqToHom ⋯
• leftUnitor_eqToHom (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = CategoryTheory.eqToHom ⋯
• rightUnitor_eqToHom (X : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = CategoryTheory.eqToHom ⋯

instance EGNO.MacLaneStrictness.endofunctorMonoidalCategory_isStrict (C : Type u) [CategoryTheory.Category.{v, u} C] : MonoidalCategory.IsStrict (CategoryTheory.Functor C C)

The monoidal category of endofunctors of C is strict: tensor product is composition, the unit is the identity functor, and all structure isomorphisms are identities.

theorem EGNO.MacLaneStrictness.skeletal_monoidal_tensorObj_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (hC : CategoryTheory.Skeletal C) (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z = CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)

In a skeletal monoidal category, the associator becomes a literal equality of objects.

theorem EGNO.MacLaneStrictness.skeletal_monoidal_tensorUnit_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (hC : CategoryTheory.Skeletal C) (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X = X

In a skeletal monoidal category, the left unitor becomes a literal equality of objects.

theorem EGNO.MacLaneStrictness.skeletal_monoidal_tensorUnit_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (hC : CategoryTheory.Skeletal C) (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = X

In a skeletal monoidal category, the right unitor becomes a literal equality of objects.

@[reducible, inline]

noncomputable abbrev EGNO.MacLaneStrictness.skeletal_monoidFromMonoidal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (hC : CategoryTheory.Skeletal C) : Monoid C

A skeletal monoidal category yields a monoid structure on the type of its objects.

theorem EGNO.MacLaneStrictness.skeleton_tensorObj_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X Y Z : CategoryTheory.Skeleton C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z = CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)

The skeleton of a monoidal category satisfies strict associativity at the object level.

theorem EGNO.MacLaneStrictness.skeleton_tensorUnit_left (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Skeleton C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Skeleton C)) X = X

The skeleton of a monoidal category satisfies strict left unit equality at the object level.

theorem EGNO.MacLaneStrictness.skeleton_tensorUnit_right (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Skeleton C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Skeleton C)) = X

The skeleton of a monoidal category satisfies strict right unit equality at the object level.

theorem EGNO.MacLaneStrictness.macLane_strictness' (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : ∃ (D : Type u) (x : CategoryTheory.Category.{v, u} D) (x_1 : CategoryTheory.MonoidalCategory D), (∀ (X Y Z : D), CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z = CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) ∧ (∀ (X : D), CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) X = X) ∧ (∀ (X : D), CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) = X) ∧ ∃ (e : C ≌ D), Nonempty e.functor.Monoidal ∧ Nonempty e.inverse.Monoidal

An intermediate version of MacLane's strictness theorem: every monoidal category is monoidally equivalent to a category with strict associativity and unit equalities at the object level, given by its skeleton.

theorem EGNO.MacLaneStrictness.Theorem_1_8_5_MacLane_strictness (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : ∃ (D : Type u) (x : CategoryTheory.Category.{v, u} D) (x_1 : CategoryTheory.MonoidalCategory D) (_ : MonoidalCategory.IsStrict D) (e : C ≌ D), Nonempty e.functor.Monoidal ∧ Nonempty e.inverse.Monoidal

Theorem 1.8.5 (MacLane Strictness): Any monoidal category is monoidally equivalent to a strict monoidal category.

@[implicit_reducible]

instance EGNO.MacLaneStrictness.tensoringRight_monoidal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalCategory.tensoringRight C).Monoidal

The right-tensoring functor C → C ⥤ C, X ↦ • ⊗ X, is naturally a monoidal functor, giving the monoidal embedding of C into its category of endofunctors.