The realization of a left odd twist is a parity shift

Twisting a module N over a commutative monoid object R by the odd line on the left produces 1-bar ⊗ N, and its Γ-module is the parity shift of the Γ-module of N. This is the mirror of RS.gammaShiftIso, which twists the regular module on the right.

The two identifications are again a source identification followed by a contraction, but the contraction is now the left cap RS.OddLine.capL, which folds the two leading odd legs of 1-bar ⊗ (1-bar ⊗ Z) against the square trivialisation. The left cap is natural in the capped object (RS.OddLine.capL_naturality), it commutes with carrying a further object past the two odd legs (RS.OddLine.capL_braidPast), and the tensor–hom bijection of the self-duality of the odd line makes it invertible (RS.OddLine.capLEquiv). Those three facts give the single sliding lemma RS.left_cap_slide, of which the four action compatibilities are instances.

Unlike the right-handed twist, a sign is unavoidable here: the scalar has to be carried past the free odd leg, and in the two odd-scalar blocks that carrying is the self-braiding of the odd line, which is −1. The sign is absorbed once and for all into the odd component RS.gammaTwistLeftOdd.

Carrying an object past a context

theorem RS.braidPast_symm {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A V T : D) : (braidPast A V T).inv = (braidPast V A T).hom

Carrying an object past a context is inverse to carrying it back: over a symmetric base the two directions are inverse isomorphisms.

theorem RS.braidPast_tensorUnit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (A Z : D) : CategoryTheory.CategoryStruct.comp (braidPast A (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) Z).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj A Z)).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom

Carrying an object past the unit is the unit coherence.

Capping the two leading odd legs

def RS.OddLine.capL {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 L.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Z) ⟶ Z

The left odd cap: contract the two leading 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.capL_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (Z : D) : L.capL Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator L.obj L.obj Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight L.sq.hom Z) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Z).hom)

The left odd cap unfolded.

theorem RS.OddLine.capL_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.whiskerLeft L.obj (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj f)) (L.capL Z') = CategoryTheory.CategoryStruct.comp (L.capL Z) f

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

theorem RS.OddLine.capL_braidPast {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (A Z : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj (braidPast A L.obj Z).hom) (L.capL (CategoryTheory.MonoidalCategoryStruct.tensorObj A Z)) = CategoryTheory.CategoryStruct.comp (braidPast L.obj A (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Z)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (L.capL Z))

The left odd cap commutes with carrying an object past the two odd legs: capping after the carry is carrying after the cap.

The sliding lemma

theorem RS.left_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] (N : D) [CategoryTheory.ModObj R N] {W X : D} (a : W ⟶ R) (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a m) (actAcross R L.obj N))) (L.capL N) = CategoryTheory.CategoryStruct.comp (braidPast L.obj W X).hom (gact a (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj m) (L.capL N)))

The sliding lemma: the action on a left twist by the odd line, capped, is the convolution action of the scalar on the capped module element, up to carrying the odd leg past the scalar. This is the whole content of the left parity shift.

theorem RS.left_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] (N : D) [CategoryTheory.ModObj R N] {W X U V V' : D} (a : W ⟶ R) (m : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj N) (s₁ : U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W X) (p : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj U) (q : V' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj X) (s₂ : V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj W V') {Φ : (U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj N) → (V ⟶ N)} {Ψ : (X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj N) → (V' ⟶ N)} (hΦ : ∀ (f : U ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj N), Φ f = CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj f) (L.capL N))) (hΨ : ∀ (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj N), Ψ f = CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj f) (L.capL N))) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj R (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj N) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj N) (hact : act = actAcross R L.obj N) (h : CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj s₁) (braidPast L.obj W X).hom) = CategoryTheory.CategoryStruct.comp s₂ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W q)) : Φ (CategoryTheory.CategoryStruct.comp s₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a m) act)) = CategoryTheory.CategoryStruct.comp s₂ (gact a (Ψ m))

The transported sliding lemma: for any two contractions Φ and Ψ presented as a source identification followed by the left cap, and any coherence identity between the two ways of reassociating the chosen sources, the contraction of a twisted action is the transported convolution action against the contraction. The four action compatibilities of RS.gammaTwistLeftHom are the four instances of this.

The two contractions are isomorphisms

noncomputable def RS.OddLine.capLEquiv {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) (Y Z : D) : (Y ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Z) ≃ₗ[ℂ] CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Y ⟶ Z

Lowering along the left cap is a ℂ-linear isomorphism: it is the tensor–hom bijection of the self-duality of the odd line.

Equations

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

noncomputable def RS.gammaTwistLeftEven {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) (Z : D) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Z) ≃ₗ[ℂ] L.obj ⟶ Z

The even component: points of a left twist by the odd line are odd elements of the module.

Equations

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

theorem RS.gammaTwistLeftEven_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) (Z : D) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Z) : ↑(gammaTwistLeftEven L Z) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj f) (L.capL Z))

noncomputable def RS.gammaTwistLeftOdd {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) (Z : D) : (L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Z) ≃ₗ[ℂ] CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z

The odd component: odd elements of a left twist by the odd line are points of the module. The sign is the self-braiding of the odd line, and it is what makes the odd blocks of the twist match the shifted blocks of the module.

Equations

• RS.gammaTwistLeftOdd L Z = L.capLEquiv L.obj Z ≪≫ₗ CategoryTheory.Linear.homCongr ℂ L.sq (CategoryTheory.Iso.refl Z) ≪≫ₗ LinearEquiv.neg ℂ

theorem RS.gammaTwistLeftOdd_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) (Z : D) (g : L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Z) : ↑(gammaTwistLeftOdd L Z) g = CategoryTheory.CategoryStruct.comp (-L.sq.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L.obj g) (L.capL Z))

The parity shift of the Γ-module

noncomputable def RS.gammaTwistLeftHom {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] (N : CategoryTheory.Mod D R) : gammaModule D L R (tensorLeftMod R L.obj N).X ⟶ (gammaModule D L R N.X).shift

The two contractions form a morphism of Γ-modules: they intertwine the four action blocks of the Γ-module of the left twist with the four relabelled blocks of the parity shift of the Γ-module of the module.

Equations

• RS.gammaTwistLeftHom L R N = { evenMap := ↑(RS.gammaTwistLeftEven L N.X), oddMap := ↑(RS.gammaTwistLeftOdd L N.X), map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }