Naturality of the monoidal comparison of the fibre functor

The free-module shuffle is natural in its two variables, and the monoidal comparison of the fibre functor inherits that naturality directly on the generators of the tensor product of super modules.

theorem RS.freeModShuffle_naturality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (R : D) [CategoryTheory.MonObj R] {V V' W W' : D} (f : V ⟶ V') (g : W ⟶ W') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R g)) (freeModShuffle R V' W') = CategoryTheory.CategoryStruct.comp (freeModShuffle R V W) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))

The free-module shuffle is natural.

theorem RS.fibreMu_naturality {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 V' W W' : D} (f : V ⟶ V') (g : W ⟶ W') : CategoryTheory.CategoryStruct.comp (SuperCommAlgebra.Mod.tensorHom (gammaFunMap L R (freeModMap R f)) (gammaFunMap L R (freeModMap R g))) (fibreMu L R V' W') = CategoryTheory.CategoryStruct.comp (fibreMu L R V W) (gammaFunMap L R (freeModMap R (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)))

The monoidal comparison of the fibre functor is natural.