The initial state of the dévissage #
Every object with an exact pairing seeds the dévissage: the base is the tensor unit, no factors are split off, and the remainder is the object itself with its ambient duality.
noncomputable def
RS.devissageInit
{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 Y : D)
[CategoryTheory.ExactPairing X Y]
(h1 : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
:
DevissageState D L X
The initial dévissage state: the trivial base, no split factors, and the object itself as the remainder.
Equations
- One or more equations did not get rendered due to their size.