Documentation

InfinityCosmos.ForMathlib.CategoryTheory.Enriched.MonoidalProdCat

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
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def CategoryTheory.enrichedTensor.of_prod (V : Type u₁) {C : Type u₂} {D : Type u₃} (p : C × D) :
      C ⊗[V] D
      Equations
      Instances For
        def CategoryTheory.enrichedTensor.to_prod (V : Type u₁) {C : Type u₂} {D : Type u₃} (q : C ⊗[V] D) :
        C × D
        Equations
        Instances For
          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.
          Instances For
            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 : CDE) (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')))) :
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For