The fibre functor is symmetric monoidal

Deligne's ω is base change to the algebra followed by realization, and its monoidal comparison RS.fibreMu is, on the generators of the tensor product of super modules, nothing but the free-module shuffle evaluated at a pair of morphisms. The three coherence laws of a lax monoidal functor therefore reduce, family by family, to the three coherence laws of the shuffle recorded in RS.FreeModShuffleCoh.

The reduction is uniform. Each generator family names a morphism s out of the intended source into a tensor product of the two sources involved, and the comparison sends a pair (m, n) to s ≫ (m ⊗ₘ n) ≫ freeModShuffle. Associativity at a family is then the associativity of the shuffle conjugated by the coherence identity relating the four s's of that family — exactly the identity that already appears in the corresponding associativity axiom of RS.gammaModule. Unitality and the braiding law are the same computation one factor shorter.

Two signs appear, and both are forced by the target rather than by the fibre functor:

• the Koszul sign of rightUnitorHom_evenMap_tmulOO in the odd-odd family of the right unitor;
• the Koszul sign of braidingHom_evenMap_tmulOO in the odd-odd family of the braiding.

In both places the sign is supplied by RS.OddLine.braid_neg: the self-braiding of the odd line is −1, so the source identification L.sq.inv picks up exactly that sign when the two odd generators are exchanged. No sign is left over.

The functor is packaged as CategoryTheory.Functor.LaxMonoidal and CategoryTheory.Functor.LaxBraided. Invertibility of fibreMu is a separate matter and is not assumed here, so the strong notions Functor.Monoidal and Functor.Braided are not instantiated.

Splitting a tensor of composites

theorem RS.tensorHom_comp_fst {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B C X Y : D} (f : A ⟶ B) (g : B ⟶ X) (p : C ⟶ Y) : CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f C) (CategoryTheory.MonoidalCategoryStruct.tensorHom g p)

A composite in the first factor, split off on the left.

theorem RS.tensorHom_comp_snd {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B C X Y : D} (m : A ⟶ X) (f : B ⟶ C) (g : C ⟶ Y) : CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) (CategoryTheory.MonoidalCategoryStruct.tensorHom m g)

A composite in the second factor, split off on the left.

theorem RS.tensorHom_comp_fst' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B C X Y : D} (f : A ⟶ B) (g : B ⟶ X) (p : C ⟶ Y) : CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f p) (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Y)

A composite in the first factor, split off on the right.

theorem RS.tensorHom_comp_snd' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {A B C X Y : D} (m : A ⟶ X) (f : B ⟶ C) (g : C ⟶ Y) : CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m f) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g)

A composite in the second factor, split off on the right.

The coherence of the shuffle at arbitrary sources

theorem RS.freeModShuffle_assoc_at {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] {A B C T T' T'' : D} (s₁ : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj T' C) (s₂ : T' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A B) (s₃ : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A T'') (s₄ : T'' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B C) (h : CategoryTheory.CategoryStruct.comp s₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight s₂ C) (CategoryTheory.MonoidalCategoryStruct.associator A B C).hom) = CategoryTheory.CategoryStruct.comp s₃ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A s₄)) {V W Z : D} (m : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : B ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) (p : C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R Z) : CategoryTheory.CategoryStruct.comp s₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp s₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))) p) (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 s₃ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp s₄ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom n p) (freeModShuffle R W Z)))) (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorObj W Z)))

Associativity of the shuffle at arbitrary sources. Given a coherence identity between the two ways of reassociating the chosen sources, the two ways of shuffling three morphisms agree.

theorem RS.freeModShuffle_assoc_at' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] {A B C T T' T'' : D} (s₁ : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj T' C) (s₂ : T' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A B) (s₃ : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj A T'') (s₄ : T'' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj B C) (h : CategoryTheory.CategoryStruct.comp s₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight s₂ C) (CategoryTheory.MonoidalCategoryStruct.associator A B C).hom) = CategoryTheory.CategoryStruct.comp s₃ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A s₄)) {V W Z : D} (m : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : B ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) (p : C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp s₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))) p) (freeModShuffle R (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) Z))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.associator V W Z).hom) = CategoryTheory.CategoryStruct.comp s₃ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp s₄ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom n p) (freeModShuffle R W Z)))) (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorObj W Z)))

RS.freeModShuffle_assoc_at, bracketed as realization of the reassociation of the generators produces it.

theorem RS.freeModShuffle_unit_left' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] (V : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj R V)) (CategoryTheory.CategoryStruct.comp (freeModShuffle R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)

Left unitality of the shuffle, with the trailing reassociation of the generators cancelled.

theorem RS.freeModShuffle_unit_left_at {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] {X Y T : D} (s : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) {V : D} (x : X ⟶ R) (m : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) : CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp x (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv) m) (CategoryTheory.CategoryStruct.comp (freeModShuffle R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom))) = CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom x m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))

Left unitality of the shuffle at arbitrary sources: filling the first slot with the unit comparison leaves the action of the free module.

theorem RS.freeModShuffle_unit_left_at' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] {X Y T : D} (s : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) {V : D} (x : X ⟶ R) (m : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp x (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv) m) (freeModShuffle R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom) = CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom x m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))

RS.freeModShuffle_unit_left_at, bracketed as realization of the left unitor of the generators produces it.

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) (CategoryTheory.CategoryStruct.comp (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom)) = 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))

Right unitality of the shuffle, with the trailing reassociation of the generators cancelled.

theorem RS.freeModShuffle_unit_right_at {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {X Y T : D} (s : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) {V : D} (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (x : Y ⟶ R) : CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp x (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)) (CategoryTheory.CategoryStruct.comp (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom))) = CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom x m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V))))

Right unitality of the shuffle at arbitrary sources: filling the second slot with the unit comparison leaves the action of the free module, the two sources having been exchanged.

theorem RS.freeModShuffle_unit_right_at' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {X Y T : D} (s : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) {V : D} (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (x : Y ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp x (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)) (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom) = CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom x m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V))))

RS.freeModShuffle_unit_right_at, bracketed as realization of the right unitor of the generators produces it.

theorem RS.freeModShuffle_braiding_at {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {X Y T : D} (s : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) {V W : D} (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (CategoryTheory.CategoryStruct.comp (freeModShuffle R V W) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (β_ V W).hom))) = CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom n m) (freeModShuffle R W V)))

The shuffle commutes with the braiding, at arbitrary sources.

theorem RS.freeModShuffle_braiding_at' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {X Y T : D} (s : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) {V W : D} (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (β_ V W).hom) = CategoryTheory.CategoryStruct.comp s (CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom n m) (freeModShuffle R W V)))

RS.freeModShuffle_braiding_at, bracketed as realization of the braiding of the generators produces it.

The braiding on the four sources

theorem RS.leftUnitorInv_braiding_ee {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv

The even-even source is fixed by the braiding.

theorem RS.leftUnitorInv_braiding_eo {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj).hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv

The braiding exchanges the even-odd and odd-even sources.

theorem RS.rightUnitorInv_braiding_oe {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv (β_ L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv

The braiding exchanges the odd-even and even-odd sources.

The four families of the unitor and the braiding

theorem RS.freeModShuffle_unit_right_ee {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V : D) (m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp x (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)) (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom x m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))

Right unitality at the even-even family.

theorem RS.freeModShuffle_unit_right_oo {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V : D) (m : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (u : L.obj ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp u (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)) (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom) = -CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom u m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))

Right unitality at the odd-odd family; the Koszul sign of the right unitor appears here, and nowhere else.

theorem RS.freeModShuffle_unit_right_eo {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V : D) (m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (u : L.obj ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp u (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)) (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom u m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))

Right unitality at the even-odd family.

theorem RS.freeModShuffle_unit_right_oe {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V : D) (m : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m (CategoryTheory.CategoryStruct.comp x (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv)) (freeModShuffle R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom x m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)))

Right unitality at the odd-even family.

theorem RS.freeModShuffle_braiding_ee {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) (m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (β_ V W).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom n m) (freeModShuffle R W V))

The braiding at the even-even family.

theorem RS.freeModShuffle_braiding_oo {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) (m : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (β_ V W).hom) = -CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom n m) (freeModShuffle R W V))

The braiding at the odd-odd family; the Koszul sign of the Koszul swap appears here, and nowhere else.

theorem RS.freeModShuffle_braiding_eo {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) (m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (β_ V W).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom n m) (freeModShuffle R W V))

The braiding at the even-odd family.

theorem RS.freeModShuffle_braiding_oe {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) (m : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (β_ V W).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom n m) (freeModShuffle R W V))

The braiding at the odd-even family.

The fibre functor and its comparison data

noncomputable def RS.fibreOver {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] : CategoryTheory.Functor D (gammaAlgebra D L R).Mod

The fibre functor over an algebra: base change to the algebra followed by realization.

Equations

• RS.fibreOver L R = (RS.freeModFunctor R).comp (RS.gammaModuleFunctor L R)

theorem RS.gammaFunMap_freeModMap_evenMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {V W : D} (f : V ⟶ W) (m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ (freeMod R V).X) : (gammaFunMap L R (freeModMap R f)).evenMap m = CategoryTheory.CategoryStruct.comp m (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f)

Realization of a base-changed morphism, in even degree.

theorem RS.gammaFunMap_freeModMap_oddMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {V W : D} (f : V ⟶ W) (m : L.obj ⟶ (freeMod R V).X) : (gammaFunMap L R (freeModMap R f)).oddMap m = CategoryTheory.CategoryStruct.comp m (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f)

Realization of a base-changed morphism, in odd degree.

Associativity

theorem RS.fibreMu_associativity {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W Z : D) : CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom (fibreMu L R V W) (CategoryTheory.CategoryStruct.id (gammaModule D L R (freeMod R Z).X))) (CategoryTheory.CategoryStruct.comp (fibreMu L R (CategoryTheory.MonoidalCategoryStruct.tensorObj V W) Z) (gammaFunMap L R (freeModMap R (CategoryTheory.MonoidalCategoryStruct.associator V W Z).hom))) = CategoryTheory.CategoryStruct.comp ((gammaModule D L R (freeMod R V).X).assocHom (gammaModule D L R (freeMod R W).X) (gammaModule D L R (freeMod R Z).X)) (CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom (CategoryTheory.CategoryStruct.id (gammaModule D L R (freeMod R V).X)) (fibreMu L R W Z)) (fibreMu L R V (CategoryTheory.MonoidalCategoryStruct.tensorObj W Z)))

Associativity of the monoidal comparison of the fibre functor: the two ways of comparing a threefold tensor product agree, up to the associator of the super modules and the reassociation of the three objects.

Unitality

theorem RS.fibreMu_left_unitality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V : D) : (gammaModule D L R (freeMod R V).X).leftUnitorHom = CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom (fibreEps L R) (CategoryTheory.CategoryStruct.id (gammaModule D L R (freeMod R V).X))) (CategoryTheory.CategoryStruct.comp (fibreMu L R (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) V) (gammaFunMap L R (freeModMap R (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom)))

Left unitality of the monoidal comparison of the fibre functor: the unit comparison in the first slot is the left unitor of the super modules. No sign appears.

theorem RS.fibreMu_right_unitality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V : D) : (gammaModule D L R (freeMod R V).X).rightUnitorHom = CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom (CategoryTheory.CategoryStruct.id (gammaModule D L R (freeMod R V).X)) (fibreEps L R)) (CategoryTheory.CategoryStruct.comp (fibreMu L R V (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (gammaFunMap L R (freeModMap R (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom)))

Right unitality of the monoidal comparison of the fibre functor: the unit comparison in the second slot is the right unitor of the super modules. The Koszul sign of the odd-odd block of the right unitor is RS.freeModShuffle_unit_right_oo, and it is supplied by RS.oddLine_sq_inv_braiding.

Compatibility with the braiding

theorem RS.fibreMu_braided {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) : CategoryTheory.CategoryStruct.comp ((gammaModule D L R (freeMod R V).X).braidingHom (gammaModule D L R (freeMod R W).X)) (fibreMu L R W V) = CategoryTheory.CategoryStruct.comp (fibreMu L R V W) (gammaFunMap L R (freeModMap R (β_ V W).hom))

The monoidal comparison of the fibre functor commutes with the braiding: swapping the two factors of the super-module tensor product and comparing agrees with comparing and swapping the two objects. The Koszul sign of the odd-odd block of the Koszul swap is RS.freeModShuffle_braiding_oo, and it is again supplied by RS.oddLine_sq_inv_braiding.

The lax monoidal and lax braided structures

@[instance_reducible]

noncomputable instance RS.fibreOverLaxMonoidal {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] : (fibreOver L R).LaxMonoidal

The fibre functor is lax monoidal, with unit RS.fibreEps and tensorator RS.fibreMu.

Equations

• RS.fibreOverLaxMonoidal L R = CategoryTheory.Functor.LaxMonoidal.ofTensorHom (RS.fibreEps L R) (RS.fibreMu L R) ⋯ ⋯ ⋯ ⋯

theorem RS.fibreOver_ε {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] : CategoryTheory.Functor.LaxMonoidal.ε (fibreOver L R) = fibreEps L R

The unit of the lax monoidal structure.

theorem RS.fibreOver_μ {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (V W : D) : CategoryTheory.Functor.LaxMonoidal.μ (fibreOver L R) V W = fibreMu L R V W

The tensorator of the lax monoidal structure.

@[instance_reducible]

noncomputable instance RS.fibreOverLaxBraided {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] : (fibreOver L R).LaxBraided

The fibre functor is lax braided: its tensorator commutes with the two symmetries.

Equations

• RS.fibreOverLaxBraided L R = { toLaxMonoidal := RS.fibreOverLaxMonoidal L R, braided := ⋯ }