External product of diagrams in a monoidal category

In a monoidal category C, given a pair of diagrams K₁ : J₁ ⥤ C and K₂ : J₂ ⥤ C, we introduce the external product K₁ ⊠ K₂ : J₁ × J₂ ⥤ C as the bifunctor (j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂. The notation - ⊠ - is scoped to MonoidalCategory.ExternalProduct.

def CategoryTheory.MonoidalCategory.externalProductBifunctorCurried (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] : Functor (Functor J₁ C) (Functor (Functor J₂ C) (Functor J₁ (Functor J₂ C)))

The (curried version of the) external product bifunctor: given diagrams K₁ : J₁ ⥤ C and K₂ : J₂ ⥤ C, this is the bifunctor j₁ ↦ j₂ ↦ K₁ j₁ ⊗ K₂ j₂.

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_obj_map (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] (X : Functor J₁ C) (X✝ : Functor J₂ C) (X✝¹ : J₁) {X✝² Y✝ : J₂} (f : X✝² ⟶ Y✝) : ((((externalProductBifunctorCurried J₁ J₂ C).obj X).obj X✝).obj X✝¹).map f = whiskerLeft (X.obj X✝¹) (X✝.map f)

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_map_app (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] (X : Functor J₁ C) (X✝ : Functor J₂ C) {X✝¹ Y✝ : J₁} (f : X✝¹ ⟶ Y✝) (X✝² : J₂) : ((((externalProductBifunctorCurried J₁ J₂ C).obj X).obj X✝).map f).app X✝² = whiskerRight (X.map f) (X✝.obj X✝²)

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_obj_obj_obj (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] (X : Functor J₁ C) (X✝ : Functor J₂ C) (X✝¹ : J₁) (X✝² : J₂) : ((((externalProductBifunctorCurried J₁ J₂ C).obj X).obj X✝).obj X✝¹).obj X✝² = tensorObj (X.obj X✝¹) (X✝.obj X✝²)

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_obj_map_app_app (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] (X : Functor J₁ C) {X✝ Y✝ : Functor J₂ C} (f : X✝ ⟶ Y✝) (X✝¹ : J₁) (c : J₂) : ((((externalProductBifunctorCurried J₁ J₂ C).obj X).map f).app X✝¹).app c = whiskerLeft (X.obj X✝¹) (f.app c)

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_map_app_app_app (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] {X✝ Y✝ : Functor J₁ C} (f : X✝ ⟶ Y✝) (X : Functor J₂ C) (c : J₁) (X✝¹ : J₂) : ((((externalProductBifunctorCurried J₁ J₂ C).map f).app X).app c).app X✝¹ = whiskerRight (f.app c) (X.obj X✝¹)

def CategoryTheory.MonoidalCategory.externalProductBifunctor (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] : Functor (Functor J₁ C × Functor J₂ C) (Functor (J₁ × J₂) C)

The external product bifunctor: given diagrams K₁ : J₁ ⥤ C and K₂ : J₂ ⥤ C, this is the bifunctor (j₁, j₂) ↦ K₁ j₁ ⊗ K₂ j₂.

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductBifunctor_obj_obj (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] (X : Functor J₁ C × Functor J₂ C) (X✝ : J₁ × J₂) : ((externalProductBifunctor J₁ J₂ C).obj X).obj X✝ = tensorObj (X.1.obj X✝.1) (X.2.obj X✝.2)

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductBifunctor_obj_map (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] (X : Functor J₁ C × Functor J₂ C) {X✝ Y : J₁ × J₂} (f : X✝ ⟶ Y) : ((externalProductBifunctor J₁ J₂ C).obj X).map f = CategoryStruct.comp (whiskerRight (X.1.map f.1) (X.2.obj X✝.2)) (whiskerLeft (X.1.obj Y.1) (X.2.map f.2))

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductBifunctor_map_app (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] {X Y : Functor J₁ C × Functor J₂ C} (f : X ⟶ Y) (X✝ : J₁ × J₂) : ((externalProductBifunctor J₁ J₂ C).map f).app X✝ = CategoryStruct.comp (whiskerRight (f.1.app X✝.1) (X.2.obj X✝.2)) (whiskerLeft (Y.1.obj X✝.1) (f.2.app X✝.2))

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.externalProduct {J₁ : Type u₁} {J₂ : Type u₂} {C : Type u₃} [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] (F₁ : Functor J₁ C) (F₂ : Functor J₂ C) : Functor (J₁ × J₂) C

An abbreviation for the action of externalProductBifunctor J₁ J₂ C on objects.

def CategoryTheory.MonoidalCategory.ExternalProduct.«term_⊠_» : Lean.TrailingParserDescr

Notation for externalProduct. Do open scoped CategoryTheory.MonoidalCategory.ExternalProduct to bring this notation in scope.

def CategoryTheory.MonoidalCategory.externalProductCompDiagIso (J₁ : Type u₁) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₃, u₃} C] [MonoidalCategory C] : (externalProductBifunctor J₁ J₁ C).comp ((Functor.whiskeringLeft J₁ (J₁ × J₁) C).obj (Functor.diag J₁)) ≅ tensor (Functor J₁ C)

When both diagrams have the same source category, composing the external product with the diagonal gives the pointwise functor tensor product. Note that (externalProductCompDiagIso _ _).app (F₁, F₂) : Functor.diag J₁ ⋙ F₁ ⊠ F₂ ≅ F₁ ⊗ F₂ type checks.

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductCompDiagIso_hom_app_app (J₁ : Type u₁) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₃, u₃} C] [MonoidalCategory C] (X : Functor J₁ C × Functor J₁ C) (X✝ : J₁) : ((externalProductCompDiagIso J₁ C).hom.app X).app X✝ = CategoryStruct.id (tensorObj (X.1.obj X✝) (X.2.obj X✝))

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductCompDiagIso_inv_app_app (J₁ : Type u₁) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₃, u₃} C] [MonoidalCategory C] (X : Functor J₁ C × Functor J₁ C) (X✝ : J₁) : ((externalProductCompDiagIso J₁ C).inv.app X).app X✝ = CategoryStruct.id (tensorObj (X.1.obj X✝) (X.2.obj X✝))

def CategoryTheory.MonoidalCategory.externalProductSwap (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] [BraidedCategory C] : (externalProductBifunctor J₁ J₂ C).comp ((Functor.whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)) ≅ (Prod.swap (Functor J₁ C) (Functor J₂ C)).comp (externalProductBifunctor J₂ J₁ C)

When C is braided, there is an isomorphism Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁, natural in both F₁ and F₂. Note that (externalProductSwap _ _ _).app (F₁, F₂) : Prod.swap _ _ ⋙ F₁ ⊠ F₂ ≅ F₂ ⊠ F₁ type checks.

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductSwap_inv_app_app (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] [BraidedCategory C] (X : Functor J₁ C × Functor J₂ C) (X✝ : J₂ × J₁) : ((externalProductSwap J₁ J₂ C).inv.app X).app X✝ = (β_ (X.1.obj X✝.2) (X.2.obj X✝.1)).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductSwap_hom_app_app (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] [BraidedCategory C] (X : Functor J₁ C × Functor J₂ C) (X✝ : J₂ × J₁) : ((externalProductSwap J₁ J₂ C).hom.app X).app X✝ = (β_ (X.1.obj X✝.2) (X.2.obj X✝.1)).hom

def CategoryTheory.MonoidalCategory.externalProductFlip (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] [BraidedCategory C] : (Functor.postcompose₂.obj (flipFunctor J₁ J₂ C)).obj (externalProductBifunctorCurried J₁ J₂ C) ≅ (externalProductBifunctorCurried J₂ J₁ C).flip

A version of externalProductSwap phrased in terms of the curried functors.

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductFlip_inv_app_app_app_app (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] [BraidedCategory C] (X : Functor J₁ C) (X✝ : Functor J₂ C) (X✝¹ : J₂) (X✝² : J₁) : ((((externalProductFlip J₁ J₂ C).inv.app X).app X✝).app X✝¹).app X✝² = (β_ (X.obj X✝²) (X✝.obj X✝¹)).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.externalProductFlip_hom_app_app_app_app (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] [BraidedCategory C] (X : Functor J₁ C) (X✝ : Functor J₂ C) (X✝¹ : J₂) (X✝² : J₁) : ((((externalProductFlip J₁ J₂ C).hom.app X).app X✝).app X✝¹).app X✝² = (β_ (X.obj X✝²) (X✝.obj X✝¹)).hom

def CategoryTheory.MonoidalCategory.prodCompExternalProduct {J₁ : Type u₁} {J₂ : Type u₂} {C : Type u₃} [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] {I₁ : Type u₃} {I₂ : Type u₄} [Category.{v₃, u₃} I₁] [Category.{v₄, u₄} I₂] (F₁ : Functor I₁ J₁) (G₁ : Functor J₁ C) (F₂ : Functor I₂ J₂) (G₂ : Functor J₂ C) : (F₁.prod F₂).comp (externalProduct G₁ G₂) ≅ externalProduct (F₁.comp G₁) (F₂.comp G₂)

Composing F₁ × F₂ with G₁ ⊠ G₂ is isomorphic to (F₁ ⋙ G₁) ⊠ (F₂ ⋙ G₂).

@[simp]

theorem CategoryTheory.MonoidalCategory.prodCompExternalProduct_inv_app {J₁ : Type u₁} {J₂ : Type u₂} {C : Type u₃} [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] {I₁ : Type u₃} {I₂ : Type u₄} [Category.{v₃, u₃} I₁] [Category.{v₄, u₄} I₂] (F₁ : Functor I₁ J₁) (G₁ : Functor J₁ C) (F₂ : Functor I₂ J₂) (G₂ : Functor J₂ C) (X : I₁ × I₂) : (prodCompExternalProduct F₁ G₁ F₂ G₂).inv.app X = CategoryStruct.id (tensorObj (G₁.obj (F₁.obj X.1)) (G₂.obj (F₂.obj X.2)))

@[simp]

theorem CategoryTheory.MonoidalCategory.prodCompExternalProduct_hom_app {J₁ : Type u₁} {J₂ : Type u₂} {C : Type u₃} [Category.{v₁, u₁} J₁] [Category.{v₂, u₂} J₂] [Category.{v₃, u₃} C] [MonoidalCategory C] {I₁ : Type u₃} {I₂ : Type u₄} [Category.{v₃, u₃} I₁] [Category.{v₄, u₄} I₂] (F₁ : Functor I₁ J₁) (G₁ : Functor J₁ C) (F₂ : Functor I₂ J₂) (G₂ : Functor J₂ C) (X : I₁ × I₂) : (prodCompExternalProduct F₁ G₁ F₂ G₂).hom.app X = CategoryStruct.id (tensorObj (G₁.obj (F₁.obj X.1)) (G₂.obj (F₂.obj X.2)))