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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.enrichedTensor.of_prod V p = { pr₁ := p.1, pr₂ := p.2 }
Instances For
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₂)
Instances For
@[simp]
theorem
CategoryTheory.enrichedTensor.to_of_prod
(V : Type u₁)
{C : Type u₂}
{D : Type u₃}
(p : C × D)
:
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 : C}
{b : C}
{c : C}
{d : C}
{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.