Documentation

Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj

Pushout-tensor-products and the braiding #

In this file, we introduce a definition Functor.PushoutObjObj.flipTensor which switches the two morphisms involved in pushout-tensor-products in a braided category.

source
def CategoryTheory.Functor.PushoutObjObj.flipTensor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂} (sq : (MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂) :
(MonoidalCategory.curriedTensor C).PushoutObjObj f₂ f₁

In a braided monoidal category, from a Functor.PushoutObjObj structure for the bifunctor curriedTensor and two morphism f₁ and f₂, one may obtain a similar structure for f₂ and f₁.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.PushoutObjObj.flipTensor_inr {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂} (sq : (MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂) :
    sq.flipTensor.inr = CategoryStruct.comp (β_ X₂ Y₁).hom sq.inl
    source
    @[simp]
    theorem CategoryTheory.Functor.PushoutObjObj.flipTensor_pt {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂} (sq : (MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂) :
    sq.flipTensor.pt = sq.pt
    source
    @[simp]
    theorem CategoryTheory.Functor.PushoutObjObj.flipTensor_ι {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂} (sq : (MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂) :
    sq.flipTensor.ι = CategoryStruct.comp sq.ι (β_ Y₂ Y₁).inv
    source
    @[simp]
    theorem CategoryTheory.Functor.PushoutObjObj.flipTensor_inl {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂} (sq : (MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂) :
    sq.flipTensor.inl = CategoryStruct.comp (β_ Y₂ X₁).hom sq.inr