Braiding coherence and naturality lemmas

In a braided monoidal category, braiding an object Z past a morphism f : A ⊗ A' ⟶ 𝟙_ C or g : 𝟙_ C ⟶ A ⊗ A' moves Z from one side of the morphism to the other. Splitting the braiding of Z with A ⊗ A' into crossings with A and A' by the hexagon identities, the crossing with one factor can be traded for the inverse crossing with the other factor. These identities are used to move objects past evaluations and coevaluations of exact pairings, for which no rigidity is needed.

This file also records naturality of the re-associated crossing (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom : X ⊗ (Y ⊗ Z) ⟶ Y ⊗ (X ⊗ Z) of the first two factors of a right-bracketed triple with respect to whiskered and tensor-product morphisms, and the unitor identity (λ_ X).hom ▷ 𝟙_ C ≫ (ρ_ X).hom expressed through the braiding β_ X (𝟙_ C) of X past the tensor unit.

It also records that the inverse tensorator δ of a braided functor commutes with the braiding (CategoryTheory.Functor.δ_braiding), the δ-form of Functor.map_braiding.

theorem TauCeti.braiding_whiskerRight_comp_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A A' : C} (Z : C) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A A' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A Z).hom A') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A A').hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A Z A').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ A' Z).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A' Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).inv))))

Braiding A past Z and then applying f : A ⊗ A' ⟶ 𝟙_ C after Z is braiding A' back under Z and then applying f before Z.

theorem TauCeti.braiding_whiskerRight_comp_whiskerLeft_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A A' : C} (Z : C) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A A' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A Z).hom A') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A A').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A Z A').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ A' Z).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A' Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).inv h)))))

Braiding A past Z and then applying f : A ⊗ A' ⟶ 𝟙_ C after Z is braiding A' back under Z and then applying f before Z.

theorem TauCeti.whiskerLeft_braiding_comp_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A A' : C} (Z : C) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A' A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A' (β_ Z A).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A' A Z).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A' Z A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Z A').inv A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A' A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv))))

Braiding Z past A and then applying f : A' ⊗ A ⟶ 𝟙_ C before Z is braiding Z back under A' and then applying f after Z.

theorem TauCeti.whiskerLeft_braiding_comp_whiskerRight_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A A' : C} (Z : C) (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A' A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A' (β_ Z A).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A' A Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A' Z A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Z A').inv A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A' A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv h)))))

Braiding Z past A and then applying f : A' ⊗ A ⟶ 𝟙_ C before Z is braiding Z back under A' and then applying f after Z.

theorem TauCeti.whiskerLeft_comp_braiding_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A A' : C} (Z : C) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A A') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A A').inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Z A).hom A')) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A' Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ Z A').inv) (CategoryTheory.MonoidalCategoryStruct.associator A Z A').inv))))

Applying g : 𝟙_ C ⟶ A ⊗ A' after Z and then braiding Z past A is applying g before Z and then braiding Z back under A'.

theorem TauCeti.whiskerLeft_comp_braiding_whiskerRight_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A A' : C} (Z : C) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A A') {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A Z) A' ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A A').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Z A).hom A') h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A' Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (β_ Z A').inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A Z A').inv h)))))

Applying g : 𝟙_ C ⟶ A ⊗ A' after Z and then braiding Z past A is applying g before Z and then braiding Z back under A'.

theorem TauCeti.whiskerRight_comp_whiskerLeft_braiding {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A A' : C} (Z : C) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A' A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A' A Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A' (β_ A Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A' A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A' Z).inv A) (CategoryTheory.MonoidalCategoryStruct.associator A' Z A).hom))))

Applying g : 𝟙_ C ⟶ A' ⊗ A before Z and then braiding A past Z is applying g after Z and then braiding A' back under Z.

theorem TauCeti.whiskerRight_comp_whiskerLeft_braiding_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A A' : C} (Z : C) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A' A) {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A' (CategoryTheory.MonoidalCategoryStruct.tensorObj Z A) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A' A Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A' (β_ A Z).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z A' A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A' Z).inv A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A' Z A).hom h)))))

Applying g : 𝟙_ C ⟶ A' ⊗ A before Z and then braiding A past Z is applying g after Z and then braiding A' back under Z.

theorem TauCeti.whiskerRight_comp_associator_inv_braiding_associator_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X' Y).hom Z) (CategoryTheory.MonoidalCategoryStruct.associator Y X' Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))))

Whiskering a morphism on the first factor of X ⊗ (Y ⊗ Z) commutes with swapping the first two factors via (α_ _ Y Z).inv ≫ (β_ _ Y).hom ▷ Z ≫ (α_ Y _ Z).hom, moving the morphism onto the middle factor.

theorem TauCeti.whiskerRight_comp_associator_inv_braiding_associator_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X X' : C} (f : X ⟶ X') (Y Z : C) {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X' Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X' Z).hom h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)) h)))

Whiskering a morphism on the first factor of X ⊗ (Y ⊗ Z) commutes with swapping the first two factors via (α_ _ Y Z).inv ≫ (β_ _ Y).hom ▷ Z ≫ (α_ Y _ Z).hom, moving the morphism onto the middle factor.

theorem TauCeti.whiskerLeft_tensorHom_comp_associator_inv_braiding_associator_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) {Y Y' Z Z' : C} (f : Y ⟶ Y') (g : Z ⟶ Z') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y').hom Z') (CategoryTheory.MonoidalCategoryStruct.associator Y' X Z').hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)))))

Whiskering f ⊗ₘ g on the right two factors of X ⊗ (Y ⊗ Z) commutes with swapping the first two factors via (α_ X _ _).inv ≫ (β_ X _).hom ▷ _ ≫ (α_ _ X _).hom, moving f onto the first factor and g onto the third factor.

theorem TauCeti.whiskerLeft_tensorHom_comp_associator_inv_braiding_associator_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) {Y Y' Z Z' : C} (f : Y ⟶ Y') (g : Z ⟶ Z') {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y' (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z') ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y').hom Z') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y' X Z').hom h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)) h))))

Whiskering f ⊗ₘ g on the right two factors of X ⊗ (Y ⊗ Z) commutes with swapping the first two factors via (α_ X _ _).inv ≫ (β_ X _).hom ▷ _ ≫ (α_ _ X _).hom, moving f onto the first factor and g onto the third factor.

theorem TauCeti.leftUnitor_whiskerRight_comp_rightUnitor_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom X) (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)))

Unitors through the braiding with the unit. The two ways of mapping (𝟙_ C ⊗ X) ⊗ 𝟙_ C to X agree: whiskering the left unitor and applying the right unitor, or reassociating, braiding X past the unit, reassociating back, and applying the unitors.

theorem TauCeti.leftUnitor_whiskerRight_comp_rightUnitor_eq_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom h))))

Unitors through the braiding with the unit. The two ways of mapping (𝟙_ C ⊗ X) ⊗ 𝟙_ C to X agree: whiskering the left unitor and applying the right unitor, or reassociating, braiding X past the unit, reassociating back, and applying the unitors.

theorem CategoryTheory.Functor.δ_braiding {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (X Y : C) : CategoryStruct.comp (OplaxMonoidal.δ F X Y) (β_ (F.obj X) (F.obj Y)).hom = CategoryStruct.comp (F.map (β_ X Y).hom) (OplaxMonoidal.δ F Y X)

The inverse tensorator δ of a braided functor intertwines the braiding of the images with the image of the braiding. This is the δ counterpart of Functor.map_braiding.

theorem CategoryTheory.Functor.δ_braiding_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [BraidedCategory C] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (X Y : C) {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj X) ⟶ Z) : CategoryStruct.comp (OplaxMonoidal.δ F X Y) (CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom h) = CategoryStruct.comp (F.map (β_ X Y).hom) (CategoryStruct.comp (OplaxMonoidal.δ F Y X) h)

The inverse tensorator δ of a braided functor intertwines the braiding of the images with the image of the braiding. This is the δ counterpart of Functor.map_braiding.