The realization of an odd twist is a parity shift

The Γ-module of the free module R ⊗ 1-bar on the odd line is the parity shift of the Γ-module of R itself: twisting by the odd line exchanges the two components of ρ, and the exchange is compatible with all four graded action blocks.

The two components of the identification are the parity swaps RS.rhoEvenOdd and RS.rhoOddOdd of RS.RhoTwist, and no sign enters. Both swaps have the same shape, s ≫ (· ▷ 1-bar) ≫ cap for a source identification s, where RS.OddLine.cap contracts the two twisting legs of (Z ⊗ 1-bar) ⊗ 1-bar against the square trivialisation. The cap is natural in the capped object (RS.OddLine.cap_naturality) and compatible with the associator (RS.OddLine.cap_tensor), and those two facts alone give the one sliding lemma of the file, RS.free_cap_slide: capping the free action of a scalar is convolution by that scalar, up to the associator of the three sources. Each of the four action compatibilities is that lemma conjugated by the very coherence isomorphisms that identify the sources in RS.gammaAlgebra.

Capping the two twisting legs

def RS.OddLine.cap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (Z : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Z L.obj) L.obj ⟶ Z

The odd cap: contract the two twisting legs of a doubly twisted object against the square trivialisation of the odd line.

Equations

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

theorem RS.OddLine.cap_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (Z : D) : L.cap Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z L.obj L.obj).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z L.sq.hom) (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom)

The odd cap unfolded.

theorem RS.OddLine.cap_naturality {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) {Z Z' : D} (f : Z ⟶ Z') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj) L.obj) (L.cap Z') = CategoryTheory.CategoryStruct.comp (L.cap Z) f

The odd cap is natural in the capped object: a morphism whiskered by the two legs passes through the contraction.

theorem RS.OddLine.cap_tensor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (A B : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator A B L.obj).inv L.obj) (L.cap (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (CategoryTheory.MonoidalCategoryStruct.tensorObj B L.obj) L.obj).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (L.cap B))

The odd cap is compatible with the associator: capping a tensor product is capping the right-hand factor inside the left-hand one.

The two parity swaps, capped

theorem RS.rhoEvenOdd_eq_cap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (Z : D) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Z L.obj) : (rhoEvenOdd L Z) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj) (L.cap Z))

The even parity swap is a whiskering followed by the cap.

theorem RS.rhoOddOdd_eq_cap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (Z : D) (g : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Z L.obj) : (rhoOddOdd L Z) g = CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g L.obj) (L.cap Z))

The odd parity swap is a whiskering followed by the cap.

The sliding lemma

theorem RS.free_cap_slide {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] {W X : D} (a : W ⟶ R) (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R L.obj) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R L.obj).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul L.obj))) L.obj) (L.cap R) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator W X L.obj).hom (gmul a (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight m L.obj) (L.cap R)))

The sliding lemma: the free action of a scalar on the free module of the odd line, capped, is the convolution product by that scalar, up to the associator of the three sources. This is μ sliding past an associator and the square trivialisation, and it is the whole content of the parity shift.

theorem RS.free_cap_slide' {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] {W X U V V' : D} (a : W ⟶ R) (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R L.obj) (s₁ : U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W X) (p : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj U L.obj) (q : V' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X L.obj) (s₂ : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W V') {Φ : (U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R L.obj) → (V ⟶ R)} {Ψ : (X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R L.obj) → (V' ⟶ R)} (hΦ : ∀ (f : U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R L.obj), Φ f = CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj) (L.cap R))) (hΨ : ∀ (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R L.obj), Ψ f = CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f L.obj) (L.cap R))) (h : CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight s₁ L.obj) (CategoryTheory.MonoidalCategoryStruct.associator W X L.obj).hom) = CategoryTheory.CategoryStruct.comp s₂ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W q)) : Φ (CategoryTheory.CategoryStruct.comp s₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a m) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R L.obj).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul L.obj)))) = CategoryTheory.CategoryStruct.comp s₂ (gmul a (Ψ m))

The transported sliding lemma: for any two parity swaps Φ and Ψ presented as a source identification followed by the cap, and any coherence identity between the two ways of reassociating the chosen sources, the swap of a free action is the transported convolution product against the swap. The four action compatibilities of RS.gammaShiftHom are the four instances of this.

The parity shift of the Γ-module

noncomputable def RS.gammaShiftHom {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 ⟶ (gammaModule D L R R).shift

The parity swap is a morphism of Γ-modules: the two parity swaps of RS.RhoTwist intertwine the four action blocks of the Γ-module of the free module on the odd line with the four relabelled blocks of the parity shift of the Γ-module of R.

Equations

• RS.gammaShiftHom L R = { evenMap := ↑(RS.rhoEvenOdd L R), oddMap := ↑(RS.rhoOddOdd L R), map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }

noncomputable def RS.gammaShiftIso {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 ≅ (gammaModule D L R R).shift

The realization of an odd twist is the parity shift of the realization: the Γ-module of the free R-module on the odd line is the parity shift of the Γ-module of R.

Equations

• RS.gammaShiftIso L R = RS.SuperCommAlgebra.Mod.isoOfComponents (RS.gammaShiftHom L R) ⋯ ⋯