Tensoring by the odd line swaps parity

The odd line is self-dual, so tensoring by it is an equivalence on Hom-spaces: points of a twisted object are odd elements of the object. Concretely, 𝟙 ⟶ M ⊗ L and L ⟶ M are the same ℂ-module, the passage between them being capping the twisting leg against the square trivialisation. Both directions are visibly ℂ-linear, composition and whiskering being bilinear, and the two round trips are the two triangle identities of the self-duality.

The mirror form, with the twist on the left, is obtained from this one by transporting along the braiding.

theorem RS.OddLine.coevaluation_whiskerRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) {M : D} (g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj ⟶ M) : CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv g) L.obj) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.sq.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) L.obj L.obj).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight g L.obj)))

Feeding the coevaluation into a map out of 𝟙 ⊗ L is the same as feeding it in on the other side: the unitors and the associator absorb the difference.

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

Tensoring by the odd line swaps parity: points of a twisted object are odd elements of the object.

Equations

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

@[simp]

theorem RS.oddParitySwap_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) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M L.obj) : (oddParitySwap L M) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f 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)))

@[simp]

theorem RS.oddParitySwap_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) (M : D) (g : L.obj ⟶ M) : (oddParitySwap L M).symm g = CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight g L.obj)

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

Tensoring by the odd line swaps parity, with the twist on the left. Transporting along the braiding reduces this to the right-handed form.

Equations

• RS.oddParitySwapLeft L M = CategoryTheory.Linear.homCongr ℂ (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (β_ L.obj M) ≪≫ₗ RS.oddParitySwap L M

@[simp]

theorem RS.oddParitySwapLeft_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) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj M) : (oddParitySwapLeft L M) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor L.obj).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp f (β_ L.obj M).hom) 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)))

@[simp]

theorem RS.oddParitySwapLeft_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) (M : D) (g : L.obj ⟶ M) : (oddParitySwapLeft L M).symm g = CategoryTheory.CategoryStruct.comp L.sq.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g L.obj) (β_ L.obj M).inv)