Coherence of the free-module shuffle #
The shuffle freeModShuffle R V W : (R ⊗ V) ⊗ (R ⊗ W) ⟶ R ⊗ (V ⊗ W)
of RS.freeModTensor obeys the coherence of a monoidal structure.
The four identities recorded here are pure identities of the ambient
braided monoidal category: no coequalizer and no module theory
appears in any of them, and everything is stated in raw
R ⊗ V language.
freeModShuffle_assoc: associativity, against the reassociation of the generators.freeModShuffle_unit_left: filling the first algebra slot with the unit leaves the left action of the free module.freeModShuffle_unit_right: filling the second algebra slot with the unit leaves the braided right action of the free module.freeModShuffle_braiding: the shuffle commutes with the braiding.
The first two need only a monoid R; the third needs R
commutative. The fourth needs the ambient braiding to be a
symmetry: the two legs differ, in a merely braided category, by the
double twist of the leading algebra factor past the second
generator, and that double twist is not the identity. Accordingly
freeModShuffle_braiding is stated over a SymmetricCategory, as
is the interchange identity RS.tensorμ_braiding behind it.
Associativity #
theorem
RS.mul_mul_whiskerRight
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
(R : D)
[CategoryTheory.MonObj R]
{P Q : D}
(g : P ⟶ Q)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul R) P)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul P)
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R g)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator R R R).hom g)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R CategoryTheory.MonObj.mul) Q)
(CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul Q))
Two multiplications, with a reassociation of the generators carried past them.
theorem
RS.mul_mul_whiskerRight_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
(R : D)
[CategoryTheory.MonObj R]
{P Q : D}
(g : P ⟶ Q)
{Z : D}
(h : CategoryTheory.MonoidalCategoryStruct.tensorObj R Q ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul R) P)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul P)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R g) h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator R R R).hom g)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R CategoryTheory.MonObj.mul) Q)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul Q) h))
Two multiplications, with a reassociation of the generators carried past them.
theorem
RS.freeModShuffle_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R : D)
[CategoryTheory.MonObj R]
(V W Z : D)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (freeModShuffle R V W)
(CategoryTheory.MonoidalCategoryStruct.tensorObj R Z))
(CategoryTheory.CategoryStruct.comp (freeModShuffle R (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) Z)
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R
(CategoryTheory.MonoidalCategoryStruct.associator V W Z).hom)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)
(CategoryTheory.MonoidalCategoryStruct.tensorObj R W) (CategoryTheory.MonoidalCategoryStruct.tensorObj R Z)).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)
(freeModShuffle R W Z))
(freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorObj W Z)))
Associativity of the shuffle: shuffling the first two free modules and then the third agrees, up to the reassociation of the generators, with shuffling the last two and then the first.
theorem
RS.freeModShuffle_assoc_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R : D)
[CategoryTheory.MonObj R]
(V W Z : D)
{Z✝ : D}
(h :
CategoryTheory.MonoidalCategoryStruct.tensorObj R
(CategoryTheory.MonoidalCategoryStruct.tensorObj V (CategoryTheory.MonoidalCategoryStruct.tensorObj W Z)) ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (freeModShuffle R V W)
(CategoryTheory.MonoidalCategoryStruct.tensorObj R Z))
(CategoryTheory.CategoryStruct.comp (freeModShuffle R (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) Z)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R
(CategoryTheory.MonoidalCategoryStruct.associator V W Z).hom)
h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)
(CategoryTheory.MonoidalCategoryStruct.tensorObj R W) (CategoryTheory.MonoidalCategoryStruct.tensorObj R Z)).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)
(freeModShuffle R W Z))
(CategoryTheory.CategoryStruct.comp (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorObj W Z)) h))
Associativity of the shuffle: shuffling the first two free modules and then the third agrees, up to the reassociation of the generators, with shuffling the last two and then the first.
Unitality #
theorem
RS.rightUnitor_inv_whiskerRight_tensorμ
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R W : D)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv
(CategoryTheory.MonoidalCategoryStruct.tensorObj R W))
(CategoryTheory.MonoidalCategory.tensorμ R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) R W) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R W).inv
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R R)
(CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv)
Interchanging against a leading unit is a reassociation.
theorem
RS.rightUnitor_inv_whiskerRight_tensorμ_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R W : D)
{Z : D}
(h :
CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj R R)
(CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) W) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv
(CategoryTheory.MonoidalCategoryStruct.tensorObj R W))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) R W) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R W).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R R)
(CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv)
h)
Interchanging against a leading unit is a reassociation.
theorem
RS.freeModShuffle_unit_left
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R : D)
[CategoryTheory.MonObj R]
(W : D)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv
(CategoryTheory.MonoidalCategoryStruct.tensorObj R W))
(freeModShuffle R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) W) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R W).inv
(CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul W))
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv)
Left unitality of the shuffle: filling the first generator slot with the unit turns the shuffle into the left action of the free module, written out.
theorem
RS.freeModShuffle_unit_left_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R : D)
[CategoryTheory.MonObj R]
(W : D)
{Z : D}
(h :
CategoryTheory.MonoidalCategoryStruct.tensorObj R
(CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) W) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv
(CategoryTheory.MonoidalCategoryStruct.tensorObj R W))
(CategoryTheory.CategoryStruct.comp (freeModShuffle R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) W) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R W).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul W)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.leftUnitor W).inv)
h))
Left unitality of the shuffle: filling the first generator slot with the unit turns the shuffle into the left action of the free module, written out.
theorem
RS.whiskerLeft_rightUnitor_inv_tensorμ
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R V : D)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)
(CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)
(CategoryTheory.MonoidalCategory.tensorμ R V R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) = CategoryTheory.CategoryStruct.comp (freeModSlide R V)
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R R)
(CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv)
Interchanging against a trailing unit is the slide.
theorem
RS.whiskerLeft_rightUnitor_inv_tensorμ_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R V : D)
{Z : D}
(h :
CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj R R)
(CategoryTheory.MonoidalCategoryStruct.tensorObj V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)
(CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorμ R V R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) h) = CategoryTheory.CategoryStruct.comp (freeModSlide R V)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R R)
(CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv)
h)
Interchanging against a trailing unit is the slide.
theorem
RS.freeModShuffle_unit_right
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(V : D)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)
(CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)
(freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj R V) R).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv
(CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv)
Right unitality of the shuffle: filling the second generator slot with the unit turns the shuffle into the braided right action of the free module, written out.
theorem
RS.freeModShuffle_unit_right_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory D]
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(V : D)
{Z : D}
(h :
CategoryTheory.MonoidalCategoryStruct.tensorObj R
(CategoryTheory.MonoidalCategoryStruct.tensorObj V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)
(CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)
(CategoryTheory.CategoryStruct.comp (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) h) = CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj R V) R).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R
(CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv)
h)))
Right unitality of the shuffle: filling the second generator slot with the unit turns the shuffle into the braided right action of the free module, written out.
Compatibility with the braiding #
theorem
RS.freeModShuffle_braiding
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(V W : D)
:
CategoryTheory.CategoryStruct.comp
(β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (CategoryTheory.MonoidalCategoryStruct.tensorObj R W)).hom
(freeModShuffle R W V) = CategoryTheory.CategoryStruct.comp (freeModShuffle R V W)
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (β_ V W).hom)
The shuffle commutes with the braiding: swapping the two
free modules and shuffling agrees with shuffling and swapping the
two generators. Commutativity of R swaps the algebra factors;
the symmetry of the ambient braiding untwists the generators.
theorem
RS.freeModShuffle_braiding_assoc
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory D]
(R : D)
[CategoryTheory.MonObj R]
[CategoryTheory.IsCommMonObj R]
(V W : D)
{Z : D}
(h : CategoryTheory.MonoidalCategoryStruct.tensorObj R (CategoryTheory.MonoidalCategoryStruct.tensorObj W V) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (CategoryTheory.MonoidalCategoryStruct.tensorObj R W)).hom
(CategoryTheory.CategoryStruct.comp (freeModShuffle R W V) h) = CategoryTheory.CategoryStruct.comp (freeModShuffle R V W)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (β_ V W).hom) h)
The shuffle commutes with the braiding: swapping the two
free modules and shuffling agrees with shuffling and swapping the
two generators. Commutativity of R swaps the algebra factors;
the symmetry of the ambient braiding untwists the generators.