The odd twist of a dévissage state

Twisting the object by the odd line twists the whole state: the remainder and its dual acquire a line factor, their duality datum is the odd twist, and the mixed free part turns each unit summand into a line and each line summand into a unit, so the two counts change places. Twisting twice returns to the original object.

noncomputable def RS.freeMixTwistIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (A : D) [CategoryTheory.MonObj A] (p q : ℕ) : tensorLeftMod A L.obj (freeMod A (L.mix p q)) ≅ freeMod A (L.mix q p)

The twist of the mixed free part: twisting the free module on a mixed sum exchanges the two counts.

Equations

• RS.freeMixTwistIso L A p q = (RS.freeTwistIso A L.obj (L.mix p q)).symm ≪≫ RS.freeModMapIso A (L.twistMixIso p q)

noncomputable def RS.twistState {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (L : OddLine D) {X : D} (st : DevissageState D L X) : DevissageState D L (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj X)

The odd twist of a dévissage state: the counts change places and the remainder gains a line factor.

Equations

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

@[simp]

theorem RS.twistState_units {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (L : OddLine D) {X : D} (st : DevissageState D L X) : (twistState L st).units = st.lines

The twist exchanges the unit count for the line count.

@[simp]

theorem RS.twistState_lines {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (L : OddLine D) {X : D} (st : DevissageState D L X) : (twistState L st).lines = st.units

The twist exchanges the line count for the unit count.

noncomputable def RS.untwistIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] (L : OddLine D) (X : D) : CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj X) ≅ X

Twisting twice is trivial: the square trivialisation undoes the double twist.

Equations

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