Theorems · Definition · category theory

CategoryTheory.Functor.PushoutObjObj.flipTensor

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {X₁ Y₁ X₂ Y₂ : C} →
          {f₁ : X₁ ⟶ Y₁} →
            {f₂ : X₂ ⟶ Y₂} →
              (CategoryTheory.MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂ →
                (CategoryTheory.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₁.

Defined in

Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj

Cited by

8 results in Mathlib

Foundations

Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategory