The comparison map at the regular module

The regular module is the unit of the relative tensor product, and its realization is the Γ-algebra viewed over itself, that is, the unit of the tensor product of super modules. Under those two identifications the comparison map of Deligne's (2.11.1) is literally a unitor, so it is an isomorphism whenever one of the two arguments is the regular module.

The Koszul sign carried by the right unitor of super modules is exactly the self-braiding of the odd line: pushing a scalar past a module element on the odd-odd block braids L past L, which is −1.

The regular module on the left

theorem RS.gpair_unitLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (N : CategoryTheory.Mod D R) {X Y : D} (a : X ⟶ R) (m : Y ⟶ N.X) : CategoryTheory.CategoryStruct.comp (gpair a m) (modTensorUnitLeftMod R N).hom.hom = gact a m

Pairing against the regular module and collapsing is the convolution action.

theorem RS.gpair_unitLeft' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (N : CategoryTheory.Mod D R) {W X Y : D} (s : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (a : X ⟶ R) (m : Y ⟶ N.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (gpair a m)) (modTensorUnitLeftMod R N).hom.hom = CategoryTheory.CategoryStruct.comp s (gact a m)

The reindexed form of RS.gpair_unitLeft.

theorem RS.gammaPairComparison_unitLeft {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (N : CategoryTheory.Mod D R) : CategoryTheory.CategoryStruct.comp (gammaPairComparison L R (regularMod R) N) ((gammaModuleFunctor L R).map (modTensorUnitLeftMod R N).hom) = (gammaModule D L R N.X).leftUnitorHom

The comparison map at the regular module on the left is the left unitor.

The regular module on the right

theorem RS.gpair_unitRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M : CategoryTheory.Mod D R) {X Y : D} (m : X ⟶ M.X) (a : Y ⟶ R) : CategoryTheory.CategoryStruct.comp (gpair m a) (modTensorUnitRightMod R M).hom.hom = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (gact a m)

Pairing with the regular module on the right and collapsing is the convolution action after a braiding.

theorem RS.gpair_unitRight' {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M : CategoryTheory.Mod D R) {W X Y : D} (s : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) (t : W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) (hst : CategoryTheory.CategoryStruct.comp s (β_ X Y).hom = t) (m : X ⟶ M.X) (a : Y ⟶ R) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (gpair m a)) (modTensorUnitRightMod R M).hom.hom = CategoryTheory.CategoryStruct.comp t (gact a m)

The reindexed form of RS.gpair_unitRight.

theorem RS.gammaPairComparison_unitRight {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M : CategoryTheory.Mod D R) : CategoryTheory.CategoryStruct.comp (gammaPairComparison L R M (regularMod R)) ((gammaModuleFunctor L R).map (modTensorUnitRightMod R M).hom) = (gammaModule D L R M.X).rightUnitorHom

The comparison map at the regular module on the right is the right unitor, Koszul sign and all: the sign is the self-braiding of the odd line.

Invertibility

noncomputable def RS.gammaPairIsoUnitLeft {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (N : CategoryTheory.Mod D R) : ((gammaModuleFunctor L R).obj (regularMod R)).tensor ((gammaModuleFunctor L R).obj N) ≅ (gammaModuleFunctor L R).obj (modTensorMod R (regularMod R) N)

The comparison isomorphism at the regular module on the left.

Equations

• RS.gammaPairIsoUnitLeft L R N = (RS.gammaModule D L R N.X).leftUnitor ≪≫ ((RS.gammaModuleFunctor L R).mapIso (RS.modTensorUnitLeftMod R N)).symm

theorem RS.gammaPairIsoUnitLeft_hom {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (N : CategoryTheory.Mod D R) : (gammaPairIsoUnitLeft L R N).hom = gammaPairComparison L R (regularMod R) N

instance RS.isIso_gammaPairComparison_unitLeft {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (N : CategoryTheory.Mod D R) : CategoryTheory.IsIso (gammaPairComparison L R (regularMod R) N)

The comparison map is an isomorphism when the left argument is the regular module.

noncomputable def RS.gammaPairIsoUnitRight {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M : CategoryTheory.Mod D R) : ((gammaModuleFunctor L R).obj M).tensor ((gammaModuleFunctor L R).obj (regularMod R)) ≅ (gammaModuleFunctor L R).obj (modTensorMod R M (regularMod R))

The comparison isomorphism at the regular module on the right.

Equations

• RS.gammaPairIsoUnitRight L R M = (RS.gammaModule D L R M.X).rightUnitor ≪≫ ((RS.gammaModuleFunctor L R).mapIso (RS.modTensorUnitRightMod R M)).symm

theorem RS.gammaPairIsoUnitRight_hom {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M : CategoryTheory.Mod D R) : (gammaPairIsoUnitRight L R M).hom = gammaPairComparison L R M (regularMod R)

instance RS.isIso_gammaPairComparison_unitRight {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft X)] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] (M : CategoryTheory.Mod D R) : CategoryTheory.IsIso (gammaPairComparison L R M (regularMod R))

The comparison map is an isomorphism when the right argument is the regular module.