The realization of a twisted object

Deligne's ρ(M) = (Hom(𝟙, M), Hom(1-bar, M)) is computed on a twist by one of the two generators of ⟨1, 1-bar⟩: twisting by the unit changes nothing, and twisting by the odd line exchanges the two components. These four identifications are the base cases of the computation of ρ on the free modules of 2.11.

noncomputable def RS.rhoEvenUnit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] (M : D) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) ≃ₗ[ℂ] CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ M

The even part of a twist by the unit.

Equations

• RS.rhoEvenUnit M = CategoryTheory.Linear.homCongr ℂ (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor M)

noncomputable def RS.rhoOddUnit {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] (L : OddLine D) (M : D) : (L.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) ≃ₗ[ℂ] L.obj ⟶ M

The odd part of a twist by the unit.

Equations

• RS.rhoOddUnit L M = CategoryTheory.Linear.homCongr ℂ (CategoryTheory.Iso.refl L.obj) (CategoryTheory.MonoidalCategoryStruct.rightUnitor M)

noncomputable def RS.rhoEvenOdd {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

The even part of a twist by the odd line is the odd part of the object.

Equations

• RS.rhoEvenOdd L M = RS.oddParitySwap L M

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

The odd part of a twist by the odd line is the even part of the object.

Equations

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