Documentation

Mathlib.CategoryTheory.Monoidal.ExternalProduct

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.

source
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₂.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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)
    source
    @[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✝)
    source
    @[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✝)
    source
    @[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)
    source
    @[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✝¹)
    source
    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₂.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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)
      source
      @[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))
      source
      @[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))
      source
      @[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.

      Equations
      Instances For
        source
        def CategoryTheory.MonoidalCategory.ExternalProduct.«term_⊠_» :
        Lean.TrailingParserDescr

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          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 ((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.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[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✝))
            source
            @[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✝))
            source
            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 ((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.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[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
              source
              @[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
              source
              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.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[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
                source
                @[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
                source
                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₂).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[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)))
                  source
                  @[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)))