Theorems · Theorem · category theory

CategoryTheory.Functor.PushoutObjObj.flipTensor_inl

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂}
  (sq : (CategoryTheory.MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂),
  sq.flipTensor.inl = CategoryTheory.CategoryStruct.comp (β_ Y₂ X₁).hom sq.inr

Defined in

Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategory