The monoidal comparison of the fibre functor

Deligne's ω sends an object to the realization of its free module, so its monoidal comparison is the comparison map of (2.11.1) at two free modules, followed by the identification of the relative tensor of two free modules with the free module of the tensor product. On the generators of the tensor product of super modules the composite has a completely explicit form: tensor the two morphisms and shuffle. No coequalizer survives in that formula, which is what makes the coherence of ω a computation in the ambient category alone.

noncomputable def RS.fibreMu {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) : (gammaModule D L R (freeMod R V).X).tensor (gammaModule D L R (freeMod R W).X) ⟶ gammaModule D L R (freeMod R (CategoryTheory.MonoidalCategoryStruct.tensorObj V W)).X

The monoidal comparison of the fibre functor.

Equations

• RS.fibreMu L R V W = CategoryTheory.CategoryStruct.comp (RS.gammaPairComparison L R (RS.freeMod R V) (RS.freeMod R W)) (RS.gammaFunMap L R (RS.freeModTensorIso R V W).hom)

@[simp]

theorem RS.fibreMu_evenMap_tmulEE {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) (m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : (fibreMu L R V W).evenMap ((((gammaModule D L R (freeMod R V).X).tmulEE (gammaModule D L R (freeMod R W).X)) m) n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))

The monoidal comparison on even-even generators.

@[simp]

theorem RS.fibreMu_evenMap_tmulOO {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) (m : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : (fibreMu L R V W).evenMap ((((gammaModule D L R (freeMod R V).X).tmulOO (gammaModule D L R (freeMod R W).X)) m) n) = CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))

The monoidal comparison on odd-odd generators.

@[simp]

theorem RS.fibreMu_oddMap_tmulEO {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) (m : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : (fibreMu L R V W).oddMap ((((gammaModule D L R (freeMod R V).X).tmulEO (gammaModule D L R (freeMod R W).X)) m) n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))

The monoidal comparison on even-odd generators.

@[simp]

theorem RS.fibreMu_oddMap_tmulOE {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) (m : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (n : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) : (fibreMu L R V W).oddMap ((((gammaModule D L R (freeMod R V).X).tmulOE (gammaModule D L R (freeMod R W).X)) m) n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom m n) (freeModShuffle R V W))

The monoidal comparison on odd-even generators.

theorem RS.isIso_fibreMu {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) (h : CategoryTheory.IsIso (gammaPairComparison L R (freeMod R V) (freeMod R W))) : CategoryTheory.IsIso (fibreMu L R V W)

The monoidal comparison is invertible as soon as the comparison map of (2.11.1) is.