The monoidal product of enriched categories

When a monoidal category V is braided, we may define the monoidal product of V-categories C and D, which is a V-category structure on the product type C × D. The "middle-four exchange" map (known as tensor_μ) is required to define the composition morphism.

structure CategoryTheory.enrichedTensor (V : Type u₁) (C : Type u₂) (D : Type u₃) : Type (max u₂ u₃)

The underlying type of the enriched tensor product of categories

• pr₁ : C
• pr₂ : D

def CategoryTheory.enrichedTensor.«term_⊗[_]_» : Lean.TrailingParserDescr

Equations

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

def CategoryTheory.enrichedTensor.of_prod (V : Type u₁) {C : Type u₂} {D : Type u₃} (p : C × D) : C ⊗[V] D

Equations

• CategoryTheory.enrichedTensor.of_prod V p = { pr₁ := p.1, pr₂ := p.2 }

def CategoryTheory.enrichedTensor.to_prod (V : Type u₁) {C : Type u₂} {D : Type u₃} (q : C ⊗[V] D) : C × D

Equations

• CategoryTheory.enrichedTensor.to_prod V q = (q.pr₁, q.pr₂)

@[simp]

theorem CategoryTheory.enrichedTensor.to_of_prod (V : Type u₁) {C : Type u₂} {D : Type u₃} (p : C × D) : CategoryTheory.enrichedTensor.to_prod V (CategoryTheory.enrichedTensor.of_prod V p) = p

@[simp]

theorem CategoryTheory.enrichedTensor.of_to_prod (V : Type u₁) {C : Type u₂} {D : Type u₃} (p : C ⊗[V] D) : CategoryTheory.enrichedTensor.of_prod V (CategoryTheory.enrichedTensor.to_prod V p) = p

def CategoryTheory.enrichedTensor.equivToEnrichedOpposite (V : Type u₁) (C : Type u₂) (D : Type u₃) : C × D ≃ C ⊗[V] D

The type-level equivalence between the product type and the enriched tensor.

Equations

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

theorem CategoryTheory.enrichedTensor.comp_tensor_comp_eq_comp_mid_left_right (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] (C : Type u₂) [CategoryTheory.EnrichedCategory V C] {a b c d e : C} : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.eComp V a b c) (CategoryTheory.eComp V c d e)) (CategoryTheory.eComp V a c e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.EnrichedCategory.Hom a b) (CategoryTheory.EnrichedCategory.Hom b c) (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.EnrichedCategory.Hom c d) (CategoryTheory.EnrichedCategory.Hom d e))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom a b) (CategoryTheory.MonoidalCategory.associator (CategoryTheory.EnrichedCategory.Hom b c) (CategoryTheory.EnrichedCategory.Hom c d) (CategoryTheory.EnrichedCategory.Hom d e)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom a b) (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.eComp V b c d) (CategoryTheory.EnrichedCategory.Hom d e))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom a b) (CategoryTheory.eComp V b d e)) (CategoryTheory.eComp V a b e))))

instance CategoryTheory.enrichedTensor.instEnrichedCategory (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] (C : Type u₂) [CategoryTheory.EnrichedCategory V C] (D : Type u₃) [CategoryTheory.EnrichedCategory V D] [CategoryTheory.BraidedCategory V] : CategoryTheory.EnrichedCategory V (C ⊗[V] D)

Equations

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

def CategoryTheory.enrichedTensor.eBifuncConstr (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] (C : Type u₂) [CategoryTheory.EnrichedCategory V C] (D : Type u₃) [CategoryTheory.EnrichedCategory V D] [CategoryTheory.SymmetricCategory V] {E : Type u₄} [CategoryTheory.EnrichedCategory V E] (F_obj : C → D → E) (F_map_left : (c c' : C) → (d : D) → CategoryTheory.EnrichedCategory.Hom c c' ⟶ CategoryTheory.EnrichedCategory.Hom (F_obj c d) (F_obj c' d)) (F_map_right : (c : C) → (d d' : D) → CategoryTheory.EnrichedCategory.Hom d d' ⟶ CategoryTheory.EnrichedCategory.Hom (F_obj c d) (F_obj c d')) (F_id_left : ∀ (c : C) (d : D), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V c) (F_map_left c c d) = CategoryTheory.eId V (F_obj c d)) (F_id_right : ∀ (c : C) (d : D), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V d) (F_map_right c d d) = CategoryTheory.eId V (F_obj c d)) (F_comp_left : ∀ (c c' c'' : C) (d : D), CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V c c' c'') (F_map_left c c'' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F_map_left c c' d) (F_map_left c' c'' d)) (CategoryTheory.eComp V (F_obj c d) (F_obj c' d) (F_obj c'' d))) (F_comp_right : ∀ (c : C) (d d' d'' : D), CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V d d' d'') (F_map_right c d d'') = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F_map_right c d d') (F_map_right c d' d'')) (CategoryTheory.eComp V (F_obj c d) (F_obj c d') (F_obj c d''))) (F_left_right_naturality : ∀ (c c' : C) (d d' : D), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F_map_left c c' d) (F_map_right c' d d')) (CategoryTheory.eComp V (F_obj c d) (F_obj c' d) (F_obj c' d')) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F_map_left c c' d') (F_map_right c d d')) (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.EnrichedCategory.Hom (F_obj c d') (F_obj c' d')) (CategoryTheory.EnrichedCategory.Hom (F_obj c d) (F_obj c d'))).hom (CategoryTheory.eComp V (F_obj c d) (F_obj c d') (F_obj c' d')))) : CategoryTheory.EnrichedFunctor V (C ⊗[V] D) E

Equations

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