The Key Lemma conclusion, in Deligne's insertion form

The conclusion of record for Deligne 2.8, per the source: a nonzero commutative algebra under the base together with module insertions of the module and its dual, multiplying the copair element to the unit. This is the data from which the direct factor 1_B ∣ M_B is rebuilt by the algebra structure (the consumer's reconstruction), stated without any base-changed module category.

The earlier element form (SplittingAlgebra in KeyLemma.lean) is superseded: it does not retain the individual insertions that the 2.9 dévissage consumes. The witness algebra is the full ℤ-graded splitting algebra, of which the balanced chain chainB is the degree-zero part — the unit lives in degree zero, so the nonvanishing argument is unaffected; the insertions live in degrees ±1.

structure RS.SplittingData {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : Type (max u v)

The conclusion of the Key Lemma (Deligne 2.8), in the insertion form of the source: a commutative algebra B under A, nonzero in the unit-detection sense, with module insertions v of M and u of M' whose product carries the copair element to the unit of B. The insertions are linear over the base through the structure morphism, and their product on the relative tensor is packaged as the descended map pairMul with its defining equation.

• carrier : D

  The underlying object of the splitting algebra.

• monObj : CategoryTheory.MonObj self.carrier

  The monoid structure.

• comm : CategoryTheory.IsCommMonObj self.carrier

  Commutativity.

• ofBase : A ⟶ self.carrier

  The structure morphism from the base algebra.

• ofBase_monHom : CategoryTheory.IsMonHom self.ofBase

  The structure morphism is a monoid map.

• unit_ne_zero : CategoryTheory.MonObj.one ≠ 0

  The algebra is nonzero: its unit does not vanish.

• ins : M.X ⟶ self.carrier

  The insertion of the module.

• ins' : M'.X ⟶ self.carrier

  The insertion of the dual module.

• ins_linear : CategoryTheory.CategoryStruct.comp (actLeft A M.X) self.ins = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A self.ins) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.ofBase self.carrier) CategoryTheory.MonObj.mul)

  The insertion of the module is linear over the base, through the structure morphism.

• ins'_linear : CategoryTheory.CategoryStruct.comp (actLeft A M'.X) self.ins' = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A self.ins') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.ofBase self.carrier) CategoryTheory.MonObj.mul)

  The insertion of the dual module is linear over the base, through the structure morphism.

• pairMul : modTensor A M M' ⟶ self.carrier

  The product of the insertions, descended to the relative tensor.

• pairMul_def : CategoryTheory.CategoryStruct.comp (modTensorπ A M M') self.pairMul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom self.ins self.ins') CategoryTheory.MonObj.mul

  Defining equation of the descended product of the insertions.

• delta_eq : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp d.copair self.pairMul) = CategoryTheory.MonObj.one

  The section identity: the product of the insertions carries the copair element to the unit.

def RS.KeyLemmaDataStatement {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] [CategoryTheory.Linear ℂ 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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : Prop

The Key Lemma statement of record (Deligne 2.8, the consumed direction): a duality datum with the zigzag laws, over a nonzero base whose symmetric powers of the module never vanish, admits splitting data.

Equations

• RS.KeyLemmaDataStatement A d = (RS.ModZigzagDatum A d → CategoryTheory.MonObj.one ≠ 0 → (∀ (n : ℕ), ¬CategoryTheory.Limits.IsZero (RS.symPow A M.X n)) → Nonempty (RS.SplittingData A d))