The trichotomy statement

Deligne's Proposition 2.9, the consumed direction: an object killed by some Schur functor is locally a sum of copies of the unit and an odd line. The odd line is an object squaring to the unit with braiding −1; local means after base change to some nonzero commutative algebra.

structure RS.OddLine (D : Type u) [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] : Type (max u v)

An odd line: an object squaring to the unit whose self-braiding is −1.

• obj : D

  The underlying object.

• sq : CategoryTheory.MonoidalCategoryStruct.tensorObj self.obj self.obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

  The square of the line is the unit.

• braid_neg : (β_ self.obj self.obj).hom = -CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj self.obj self.obj)

  The self-braiding of the line is −1.

noncomputable def RS.OddLine.mix {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (p q : ℕ) : D

The mixed sum of p copies of the unit and q copies of the line.

Equations

• L.mix p q = ⨁ fun (i : Fin p ⊕ Fin q) => Sum.elim (fun (x : Fin p) => CategoryTheory.MonoidalCategoryStruct.tensorUnit D) (fun (x : Fin q) => L.obj) i

theorem RS.OddLine.isZero_mix_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) : CategoryTheory.Limits.IsZero (L.mix 0 0)

The empty mixed sum is the zero object.

def RS.OddLine.LocallyMixed {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (L : OddLine D) (X : D) : Prop

Locally mixed: after base change to some nonzero commutative algebra, the object becomes a sum of copies of the unit and the line.

Equations

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

theorem RS.OddLine.isZero_tensor_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (L : OddLine D) (Y : D) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj L.obj Y) ↔ CategoryTheory.Limits.IsZero Y

Tensoring with the odd line reflects vanishing: the square of the line collapses to the unit, so the double twist is the identity up to isomorphism.

def RS.Prop29Statement {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Linear ℂ D] (P : SchurPackage) (L : OddLine D) (X : D) : Prop

The trichotomy statement of record (Deligne 2.9, the consumed direction): an object killed by some Schur functor is locally a mixed sum of the unit and the odd line.

Equations

• RS.Prop29Statement P L X = ((∃ (lam : YoungDiagram), RS.SchurKilled P X lam) → L.LocallyMixed X)