Products and tensor products of enriched categories

If C is enriched in V and D is enriched in W, then C × D is enriched in the product monoidal category V × W: Hom objects, identities and composition are taken componentwise.

When C and D are both enriched in a braided monoidal category V, the tensor product functor MonoidalCategory.tensor V : V × V ⥤ V is monoidal, and transporting the V × V-enrichment of C × D along it gives the tensor product of the two V-categories. Its Hom object from (X, Y) to (X', Y') is (X ⟶[V] X') ⊗ (Y ⟶[V] Y'), its identities are tensor products of identities, and its composition first applies the middle-four interchange MonoidalCategory.tensorμ, which uses the braiding, and then composes in each factor. For categories enriched in cochain complexes the braiding carries the Koszul sign, and this is the tensor product of differential graded categories.

Main definitions

• TauCeti.prodEnrichedCategory: the V × W-enrichment of C × D.
• TauCeti.tensorEnrichedCategory: the V-enrichment of C × D when V is braided.

Main results

• TauCeti.eHom_tensor_eq, TauCeti.eId_tensor_eq and TauCeti.eComp_tensor_eq: Hom objects, identities and composition of the tensor product, in terms of those of the two factors.

References

• G. M. Kelly, Basic concepts of enriched category theory, Section 1.4.
• Mathlib.CategoryTheory.Enriched.Basic, for CategoryTheory.TransportEnrichment, and Mathlib.CategoryTheory.Monoidal.Braided.Basic, for the monoidal structure on the tensor product functor.

@[instance_reducible]

instance TauCeti.prodEnrichedCategory (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] (W : Type u₂) [CategoryTheory.Category.{v₂, u₂} W] [CategoryTheory.MonoidalCategory W] (C : Type u₃) [CategoryTheory.EnrichedCategory V C] (D : Type u₄) [CategoryTheory.EnrichedCategory W D] : CategoryTheory.EnrichedCategory (V × W) (C × D)

The product of a V-category and a W-category is a category enriched in the product monoidal category V × W, with Hom objects, identities and composition taken componentwise.

Equations

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

theorem TauCeti.eHom_prod_eq {V : Type u₁} [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {W : Type u₂} [CategoryTheory.Category.{v₂, u₂} W] [CategoryTheory.MonoidalCategory W] {C : Type u₃} [CategoryTheory.EnrichedCategory V C] {D : Type u₄} [CategoryTheory.EnrichedCategory W D] (X Y : C × D) : (X ⟶[V × W] Y) = (X.1 ⟶[V] Y.1, X.2 ⟶[W] Y.2)

The Hom object of a product of enriched categories is the pair of Hom objects.

theorem TauCeti.eId_prod_eq {V : Type u₁} [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {W : Type u₂} [CategoryTheory.Category.{v₂, u₂} W] [CategoryTheory.MonoidalCategory W] {C : Type u₃} [CategoryTheory.EnrichedCategory V C] {D : Type u₄} [CategoryTheory.EnrichedCategory W D] (X : C × D) : CategoryTheory.eId (V × W) X = (CategoryTheory.eId V X.1, CategoryTheory.eId W X.2)

The identity of an object of a product of enriched categories is the pair of identities.

theorem TauCeti.eComp_prod_eq {V : Type u₁} [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] {W : Type u₂} [CategoryTheory.Category.{v₂, u₂} W] [CategoryTheory.MonoidalCategory W] {C : Type u₃} [CategoryTheory.EnrichedCategory V C] {D : Type u₄} [CategoryTheory.EnrichedCategory W D] (X Y Z : C × D) : CategoryTheory.eComp (V × W) X Y Z = (CategoryTheory.eComp V X.1 Y.1 Z.1, CategoryTheory.eComp W X.2 Y.2 Z.2)

Composition in a product of enriched categories is the pair of compositions.

@[instance_reducible]

instance TauCeti.tensorEnrichedCategory (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u₃) [CategoryTheory.EnrichedCategory V C] (D : Type u₄) [CategoryTheory.EnrichedCategory V D] : CategoryTheory.EnrichedCategory V (C × D)

The tensor product of two categories enriched in a braided monoidal category V. The Hom object from (X, Y) to (X', Y') is (X ⟶[V] X') ⊗ (Y ⟶[V] Y'); identities and composition are described by TauCeti.eId_tensor_eq and TauCeti.eComp_tensor_eq. It is the V × V-enrichment TauCeti.prodEnrichedCategory transported along the monoidal functor MonoidalCategory.tensor V.

Equations

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

theorem TauCeti.eHom_tensor_eq {V : Type u₁} [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u₃} [CategoryTheory.EnrichedCategory V C] {D : Type u₄} [CategoryTheory.EnrichedCategory V D] (X Y : C × D) : (X ⟶[V] Y) = CategoryTheory.MonoidalCategoryStruct.tensorObj (X.1 ⟶[V] Y.1) (X.2 ⟶[V] Y.2)

The Hom object of the tensor product of two enriched categories is the tensor product of the Hom objects of the two factors.

theorem TauCeti.eId_tensor_eq {V : Type u₁} [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u₃} [CategoryTheory.EnrichedCategory V C] {D : Type u₄} [CategoryTheory.EnrichedCategory V D] (X : C × D) : CategoryTheory.eId V X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eId V X.1) (CategoryTheory.eId V X.2))

The identity of an object of the tensor product of two enriched categories is the tensor product of the identities of its two components.

theorem TauCeti.eId_tensor_eq_assoc {V : Type u₁} [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u₃} [CategoryTheory.EnrichedCategory V C] {D : Type u₄} [CategoryTheory.EnrichedCategory V D] (X : C × D) {Z : V} (h : (X ⟶[V] X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eId V X.1) (CategoryTheory.eId V X.2)) h)

The identity of an object of the tensor product of two enriched categories is the tensor product of the identities of its two components.

theorem TauCeti.eComp_tensor_eq {V : Type u₁} [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u₃} [CategoryTheory.EnrichedCategory V C] {D : Type u₄} [CategoryTheory.EnrichedCategory V D] (X Y Z : C × D) : CategoryTheory.eComp V X Y Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (X.1 ⟶[V] Y.1) (X.2 ⟶[V] Y.2) (Y.1 ⟶[V] Z.1) (Y.2 ⟶[V] Z.2)) (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eComp V X.1 Y.1 Z.1) (CategoryTheory.eComp V X.2 Y.2 Z.2))

Composition in the tensor product of two enriched categories: interchange the two middle factors with MonoidalCategory.tensorμ, then compose in each factor.

theorem TauCeti.eComp_tensor_eq_assoc {V : Type u₁} [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u₃} [CategoryTheory.EnrichedCategory V C] {D : Type u₄} [CategoryTheory.EnrichedCategory V D] (X Y Z : C × D) {Z✝ : V} (h : (X ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (X.1 ⟶[V] Y.1) (X.2 ⟶[V] Y.2) (Y.1 ⟶[V] Z.1) (Y.2 ⟶[V] Z.2)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.eComp V X.1 Y.1 Z.1) (CategoryTheory.eComp V X.2 Y.2 Z.2)) h)

Composition in the tensor product of two enriched categories: interchange the two middle factors with MonoidalCategory.tensorμ, then compose in each factor.