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) : to_prod V (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) : of_prod V (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₁) [Category.{v₁, u₁} V] [MonoidalCategory V] (C : Type u₂) [EnrichedCategory V C] {a b c d e : C} : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (eComp V a b c) (eComp V c d e)) (eComp V a c e) = CategoryStruct.comp (MonoidalCategoryStruct.associator (a ⟶[V] b) (b ⟶[V] c) (MonoidalCategoryStruct.tensorObj (c ⟶[V] d) (d ⟶[V] e))).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (a ⟶[V] b) (MonoidalCategoryStruct.associator (b ⟶[V] c) (c ⟶[V] d) (d ⟶[V] e)).inv) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (a ⟶[V] b) (MonoidalCategoryStruct.whiskerRight (eComp V b c d) (d ⟶[V] e))) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (a ⟶[V] b) (eComp V b d e)) (eComp V a b e))))

instance CategoryTheory.enrichedTensor.instEnrichedCategory (V : Type u₁) [Category.{v₁, u₁} V] [MonoidalCategory V] (C : Type u₂) [EnrichedCategory V C] (D : Type u₃) [EnrichedCategory V D] [BraidedCategory V] : 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₁) [Category.{v₁, u₁} V] [MonoidalCategory V] (C : Type u₂) [EnrichedCategory V C] (D : Type u₃) [EnrichedCategory V D] [SymmetricCategory V] {E : Type u₄} [EnrichedCategory V E] (F_obj : C → D → E) (F_map_left : (c c' : C) → (d : D) → (c ⟶[V] c') ⟶ F_obj c d ⟶[V] F_obj c' d) (F_map_right : (c : C) → (d d' : D) → (d ⟶[V] d') ⟶ F_obj c d ⟶[V] F_obj c d') (F_id_left : ∀ (c : C) (d : D), CategoryStruct.comp (eId V c) (F_map_left c c d) = eId V (F_obj c d)) (F_id_right : ∀ (c : C) (d : D), CategoryStruct.comp (eId V d) (F_map_right c d d) = eId V (F_obj c d)) (F_comp_left : ∀ (c c' c'' : C) (d : D), CategoryStruct.comp (eComp V c c' c'') (F_map_left c c'' d) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F_map_left c c' d) (F_map_left c' c'' d)) (eComp V (F_obj c d) (F_obj c' d) (F_obj c'' d))) (F_comp_right : ∀ (c : C) (d d' d'' : D), CategoryStruct.comp (eComp V d d' d'') (F_map_right c d d'') = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F_map_right c d d') (F_map_right c d' d'')) (eComp V (F_obj c d) (F_obj c d') (F_obj c d''))) (F_left_right_naturality : ∀ (c c' : C) (d d' : D), CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F_map_left c c' d) (F_map_right c' d d')) (eComp V (F_obj c d) (F_obj c' d) (F_obj c' d')) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F_map_left c c' d') (F_map_right c d d')) (CategoryStruct.comp (β_ (F_obj c d' ⟶[V] F_obj c' d') (F_obj c d ⟶[V] F_obj c d')).hom (eComp V (F_obj c d) (F_obj c d') (F_obj c' d')))) : EnrichedFunctor V (C ⊗[V] D) E

Equations

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