Theorems · Theorem · category theory

CategoryTheory.HalfBraiding.mk.inj

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {X : C}
  {β :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X}
  {monoidal :
    autoParam
      (∀ (U U' : C),
        (β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam}
  {naturality :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β U').hom =
          CategoryTheory.CategoryStruct.comp (β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam}
  {β_1 :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X}
  {monoidal_1 :
    autoParam
      (∀ (U U' : C),
        (β_1 (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_1 U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β_1 U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam}
  {naturality_1 :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_1 U').hom =
          CategoryTheory.CategoryStruct.comp (β_1 U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam},
  { β := β, monoidal := monoidal, naturality := naturality } =
      { β := β_1, monoidal := monoidal_1, naturality := naturality_1 } →
    β = β_1

Defined in

Mathlib.CategoryTheory.Monoidal.Center

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms