Braidings for Day convolution

In this file, we show that if C is a braided monoidal category and V also a braided monoidal category, then the Day convolution monoidal structure on C ⥤ V is also braided monoidal. We prove it by constructing an explicit braiding isomorphism whenever sufficient Day convolutions exist, and we prove that it satisfies the forward and reverse hexagon identities.

Furthermore, we show that when both C and V are symmetric monoidal categories, then the Day convolution monoidal structure is symmetric as well.

def CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution G F] : externalProduct F G ⟶ (tensor C).comp (convolution G F)

The natural transformation F ⊠ G ⟶ (tensor C) ⋙ (G ⊛ F) that corepresents the braiding morphism F ⊛ G ⟶ G ⊛ F.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.braidingHomCorepresenting_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution G F] (x✝ : C × C) : (braidingHomCorepresenting F G).app x✝ = CategoryStruct.comp (β_ ((F, G).1.obj x✝.1) ((F, G).2.obj x✝.2)).hom (CategoryStruct.comp ((unit G F).app (x✝.2, x✝.1)) ((convolution G F).map (β_ (x✝.2, x✝.1).1 (x✝.2, x✝.1).2).hom))

def CategoryTheory.MonoidalCategory.DayConvolution.braidingInvCorepresenting {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution F G] : externalProduct G F ⟶ (tensor C).comp (convolution F G)

The natural transformation F ⊠ G ⟶ (tensor C) ⋙ (G ⊛ F) that corepresents the braiding morphism F ⊛ G ⟶ G ⊛ F.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.braidingInvCorepresenting_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution F G] (x✝ : C × C) : (braidingInvCorepresenting F G).app x✝ = CategoryStruct.comp (β_ ((G, F).2.obj x✝.2) ((G, F).1.obj x✝.1)).inv (CategoryStruct.comp ((unit F G).app (x✝.2, x✝.1)) ((convolution F G).map (β_ (x✝.2, x✝.1).2 (x✝.2, x✝.1).1).inv))

def CategoryTheory.MonoidalCategory.DayConvolution.braiding {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution F G] [DayConvolution G F] : convolution F G ≅ convolution G F

The braiding isomorphism for Day convolution.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_app_braiding_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution F G] [DayConvolution G F] (x y : C) : CategoryStruct.comp ((unit F G).app (x, y)) ((braiding F G).hom.app (tensorObj x y)) = CategoryStruct.comp (β_ ((G, F).2.obj (y, x).2) ((G, F).1.obj (y, x).1)).hom (CategoryStruct.comp ((unit G F).app (y, x)) ((convolution G F).map (β_ (y, x).1 (y, x).2).hom))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_app_braiding_hom_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution F G] [DayConvolution G F] (x y : C) {Z : V} (h : (convolution G F).obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((unit F G).app (x, y)) (CategoryStruct.comp ((braiding F G).hom.app (tensorObj x y)) h) = CategoryStruct.comp (β_ (F.obj x) (G.obj y)).hom (CategoryStruct.comp ((unit G F).app (y, x)) (CategoryStruct.comp ((convolution G F).map (β_ y x).hom) h))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_app_braiding_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution F G] [DayConvolution G F] (x y : C) : CategoryStruct.comp ((unit G F).app (x, y)) ((braiding F G).inv.app (tensorObj x y)) = CategoryStruct.comp (β_ ((F, G).1.obj (y, x).1) ((F, G).2.obj (y, x).2)).inv (CategoryStruct.comp ((unit F G).app (y, x)) ((convolution F G).map (β_ (y, x).2 (y, x).1).inv))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_app_braiding_inv_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [DayConvolution F G] [DayConvolution G F] (x y : C) {Z : V} (h : (convolution F G).obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((unit G F).app (x, y)) (CategoryStruct.comp ((braiding F G).inv.app (tensorObj x y)) h) = CategoryStruct.comp (β_ (F.obj y) (G.obj x)).inv (CategoryStruct.comp ((unit F G).app (y, x)) (CategoryStruct.comp ((convolution F G).map (β_ x y).inv) h))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_right {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] {F G : Functor C V} (H : Functor C V) (η : F ⟶ G) [DayConvolution F H] [DayConvolution H F] [DayConvolution G H] [DayConvolution H G] : CategoryStruct.comp (map (CategoryStruct.id H) η) (braiding H G).hom = CategoryStruct.comp (braiding H F).hom (map η (CategoryStruct.id H))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] {F G : Functor C V} (H : Functor C V) (η : F ⟶ G) [DayConvolution F H] [DayConvolution H F] [DayConvolution G H] [DayConvolution H G] {Z : Functor C V} (h : convolution G H ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.id H) η) (CategoryStruct.comp (braiding H G).hom h) = CategoryStruct.comp (braiding H F).hom (CategoryStruct.comp (map η (CategoryStruct.id H)) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_left {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] {F G : Functor C V} (η : F ⟶ G) (H : Functor C V) [DayConvolution F H] [DayConvolution H F] [DayConvolution G H] [DayConvolution H G] : CategoryStruct.comp (map η (CategoryStruct.id H)) (braiding G H).hom = CategoryStruct.comp (braiding F H).hom (map (CategoryStruct.id H) η)

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.braiding_naturality_left_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] {F G : Functor C V} (η : F ⟶ G) (H : Functor C V) [DayConvolution F H] [DayConvolution H F] [DayConvolution G H] [DayConvolution H G] {Z : Functor C V} (h : convolution H G ⟶ Z) : CategoryStruct.comp (map η (CategoryStruct.id H)) (CategoryStruct.comp (braiding G H).hom h) = CategoryStruct.comp (braiding F H).hom (CategoryStruct.comp (map (CategoryStruct.id H) η) h)

theorem CategoryTheory.MonoidalCategory.DayConvolution.hexagon_forward {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] (H : Functor C V) [DayConvolution F G] [DayConvolution G H] [DayConvolution F (convolution G H)] [DayConvolution (convolution F G) H] [DayConvolution H F] [DayConvolution G (convolution H F)] [DayConvolution (convolution G H) F] [DayConvolution G F] [DayConvolution (convolution G F) H] [DayConvolution F H] [DayConvolution G (convolution F H)] : CategoryStruct.comp (associator F G H).hom (CategoryStruct.comp (braiding F (convolution G H)).hom (associator G H F).hom) = CategoryStruct.comp (map (braiding F G).hom (CategoryStruct.id H)) (CategoryStruct.comp (associator G F H).hom (map (CategoryStruct.id G) (braiding F H).hom))

theorem CategoryTheory.MonoidalCategory.DayConvolution.hexagon_reverse {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [BraidedCategory C] [MonoidalCategory V] [BraidedCategory V] (F G : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] (H : Functor C V) [DayConvolution F G] [DayConvolution G H] [DayConvolution F (convolution G H)] [DayConvolution (convolution F G) H] [DayConvolution H (convolution F G)] [DayConvolution H F] [DayConvolution (convolution H F) G] [DayConvolution H G] [DayConvolution F (convolution H G)] [DayConvolution F H] [DayConvolution (convolution F H) G] : CategoryStruct.comp (associator F G H).inv (CategoryStruct.comp (braiding (convolution F G) H).hom (associator H F G).inv) = CategoryStruct.comp (map (CategoryStruct.id F) (braiding G H).hom) (CategoryStruct.comp (associator F H G).inv (map (braiding F H).hom (CategoryStruct.id G)))

theorem CategoryTheory.MonoidalCategory.DayConvolution.symmetry {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [SymmetricCategory C] [MonoidalCategory V] [SymmetricCategory V] (F G : Functor C V) [DayConvolution F G] [DayConvolution G F] : CategoryStruct.comp (braiding F G).hom (braiding G F).hom = CategoryStruct.id (convolution F G)