The comparison map at the odd line against itself

The realization of the free module on the odd line is the parity shift of the Γ-algebra, and the parity shift of the algebra is invertible for the tensor product of super modules. Under those two identifications the comparison map of Deligne's (2.11.1) at the odd line against itself is minus the canonical isomorphism, so it is an isomorphism. The sign is the self-braiding of the line and is the same on all four blocks.

The two parity swaps, inverted

theorem RS.rhoOddOdd_apply {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) (M : D) (g : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M L.obj) : (rhoOddOdd L M) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight g L.obj)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M L.obj L.obj).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom))

The odd parity swap, unfolded.

theorem RS.rhoOddOdd_symm_apply {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) (y : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ R) : (rhoOddOdd L R).symm y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight y L.obj)

The odd parity swap, inverted.

The comparison at the odd line against itself

@[reducible, inline]

noncomputable abbrev RS.oddSqMap {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.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] : (gammaModule D L R (freeMod R L.obj).X).tensor (gammaModule D L R (freeMod R L.obj).X) ⟶ (gammaAlgebra D L R).unitMod

The comparison map at the odd line against itself, followed by the two identifications of the target with the algebra.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev RS.oddSqShift {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] : (gammaModule D L R (freeMod R L.obj).X).tensor (gammaModule D L R (freeMod R L.obj).X) ⟶ (gammaAlgebra D L R).unitMod

The identification of the source with the parity shift of the algebra, on both factors.

Equations

• One or more equations did not get rendered due to their size.

Evaluation on the four generator families

The identification

theorem RS.oddSqMap_eq {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.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] : oddSqMap L R = -oddSqShift L R

The comparison map at the odd line against itself is minus the canonical isomorphism. The sign is the self-braiding of the line, and it is the same on all four blocks.

Invertibility

theorem RS.isIso_gammaPairComparison_oddSquare {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.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] : CategoryTheory.IsIso (gammaPairComparison L R (freeMod R L.obj) (freeMod R L.obj))

The comparison map of (2.11.1) at the odd line against itself is an isomorphism.