The Key Lemma, closed over the ind-completion

The splitting data of Deligne's Key Lemma (2.8), assembled from the graded splitting algebra: the carrier is the ℤ-graded chain algebra, the base enters in degree zero, the module and its dual in degrees ±1, the pair product two stages up the degree-zero line, and the section identity is the advancement of the seed. Nonvanishing is the stage-detection argument of the balanced line.

instance RS.tensorLeft_ind_preservesShapeInt {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (X : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)

Tensoring preserves integer-indexed coproducts in the ind-category, by transport from the universe-sized discrete shape.

instance RS.tensorRight_ind_preservesShapeInt {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (X : CategoryTheory.Ind C) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorRight X)

Tensoring preserves integer-indexed coproducts in the ind-category, right-hand version.

theorem RS.keyLemmaData_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Linear ℂ (CategoryTheory.Ind C)] [CategoryTheory.MonoidalLinear ℂ (CategoryTheory.Ind C)] (B : CategoryTheory.Ind C) [CategoryTheory.MonObj B] [CategoryTheory.IsCommMonObj B] (N N' : CategoryTheory.Mod (CategoryTheory.Ind C) B) (d : ModDualityDatum B N N') : KeyLemmaDataStatement B d

The Key Lemma (Deligne 2.8) over the ind-completion: a duality datum with the zigzag laws, over a base whose symmetric powers of the module never vanish, admits splitting data — the graded splitting algebra with its degree-±1 insertions.