The dévissage state of the trichotomy

The recursion state of Deligne's 2.9, direction (ii) ⇒ (i): a nonzero commutative base algebra, counts of split-off unit and line factors, and a dualizable remainder module, together with a decomposition of the base change of the object as the mixed free part plus the remainder. Each step of the dévissage either splits a further unit factor off the remainder (through the Key Lemma), splits a line factor (through the sign-twisted mirror), or exits with the remainder already zero.

structure RS.DevissageState (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) : Type (max u v)

The dévissage state: a nonzero commutative base, the counts of unit and line factors already split off, a dualizable remainder with its zigzag laws, and the decomposition of the base change of the object.

• base : D

  The current base algebra.

• monObj : CategoryTheory.MonObj self.base

  Its monoid structure.

• comm : CategoryTheory.IsCommMonObj self.base

  Commutativity.

• unit_ne_zero : CategoryTheory.MonObj.one ≠ 0

  The base is nonzero: its unit does not vanish.

• units : ℕ

  The number of unit factors split off.

• lines : ℕ

  The number of line factors split off.

• rest : CategoryTheory.Mod D self.base

  The remainder module.

• restDual : CategoryTheory.Mod D self.base

  The dual of the remainder.

• datum : ModDualityDatum self.base self.rest self.restDual

  The duality datum of the remainder.

• zigzag : ModZigzagDatum self.base self.datum

  The zigzag laws of the duality datum.

• decomp : Nonempty (freeMod self.base X ≅ modBiprod self.base (freeMod self.base (L.mix self.units self.lines)) self.rest)

  The base change of the object decomposes as the mixed free part plus the remainder.

def RS.DevissageStepA (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)] [CategoryTheory.Linear ℂ D] (L : OddLine D) (X : D) : Prop

Case (a) of the dévissage: when every symmetric power of the remainder survives, a further unit factor splits off.

Equations

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

def RS.DevissageStepB (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)] [CategoryTheory.Linear ℂ D] (L : OddLine D) (X : D) : Prop

Case (b): when every alternating power of the remainder survives, a further line factor splits off.

Equations

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

def RS.DevissageExit (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) : Prop

The exit: a state whose remainder has died witnesses the local mixed decomposition.

Equations

• RS.DevissageExit D L X = ∀ (st : RS.DevissageState D L X), CategoryTheory.Limits.IsZero st.rest.X → L.LocallyMixed X

theorem RS.devissageExit (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) : DevissageExit D L X

The exit holds: the decomposition collapses onto its mixed free part once the remainder dies.

def RS.DevissageTrichotomy (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)] [CategoryTheory.Linear ℂ D] (L : OddLine D) (X : D) : Prop

The trichotomy: over any state, either every symmetric power of the remainder survives, or every alternating power survives, or the remainder has died.

Equations

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

theorem RS.devissage_run (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)] [CategoryTheory.Linear ℂ D] (L : OddLine D) (X : D) (hA : DevissageStepA D L X) (hB : DevissageStepB D L X) (hT : DevissageTrichotomy D L X) (hE : DevissageExit D L X) (bound : ℕ) (hBound : ∀ (st : DevissageState D L X), st.units + st.lines ≤ bound) (st₀ : DevissageState D L X) : L.LocallyMixed X

The dévissage runs to completion: given the two step constructions, the trichotomy, the exit, and a uniform bound on the number of split-off factors, every state leads to the local mixed decomposition.