The Key Lemma: the universal splitting algebra

Deligne 2.8, the consumed direction: for a dualizable module over a commutative algebra whose symmetric powers do not vanish, there is a nonzero algebra over which the module acquires the unit as a direct factor. The construction is the colimit of the chain of paired symmetric powers, with copair-insertion transitions; its nonvanishing is stage detection for the unit, and the splitting pair is built from the tautological pairing against the multiplication.

The duality of the module is Mod-internal: the pairing and copairing are given as data with zigzag identities stated at the multi-tensor level, where the wide-coequalizer presentation makes them associativity-free.

The form of the conclusion

The conclusion is in element form: a nonzero commutative algebra B under A together with a global point of modTensor A M' M ⊗ B on which the pairing evaluates to the unit of B. This is the section-of-the-evaluation reading of the splitting: the point is exactly the datum needed to produce a B-linear section of the base-changed evaluation by multiplication. A direct splitting of the unit off M_B itself is not the right reading: counting M-letters minus M'-letters grades every morphism constructible from a duality datum, and M_B sits in degree one while B sits in degree zero, so no constructible morphism connects them. The degree-zero object modTensor A M' M ⊗ B is where the splitting genuinely lives.

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

A Mod-internal duality datum for a pair of modules over a monoid object: a descended A-valued pairing and a copairing into the relative tensor, each a module map. The zigzag identities live one level up, through the multi-tensor insertion and contraction constructors, and are packaged separately as ModZigzagDatum.

• pair : modTensor A M' M ⟶ A

  The descended A-valued pairing on the relative tensor.

• copair : A ⟶ modTensor A M M'

  The copairing into the relative tensor.

• pair_linear : CategoryTheory.CategoryStruct.comp (actLeft A (modTensor A M' M)) self.pair = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A self.pair) CategoryTheory.MonObj.mul

  The pairing is a module map for the descended action and the regular action.

• copair_linear : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul self.copair = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A self.copair) (actLeft A (modTensor A M M'))

  The copairing is a module map for the regular action and the descended action.

noncomputable def RS.ModDualityDatum.pairMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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') : modTensorMod A M' M ⟶ regularMod A

The pairing of a duality datum, as a module map into the regular module.

Equations

• RS.ModDualityDatum.pairMod A d = CategoryTheory.Mod.Hom.mk' d.pair ⋯

noncomputable def RS.ModDualityDatum.copairMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory 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') : regularMod A ⟶ modTensorMod A M M'

The copairing of a duality datum, as a module map from the regular module.

Equations

• RS.ModDualityDatum.copairMod A d = CategoryTheory.Mod.Hom.mk' d.copair ⋯

structure RS.ModZigzagDatum {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory 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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : Prop

The zigzag laws of a duality datum. Both triangle identities, stated through the multi-tensor insertion and contraction constructors: inserting the copairing and contracting the pairing across the original factor is the identity, on each side. These are the dimension-free dualizability conditions: the inserted M' is contracted against the original M (and mirrored), never against its own partner — the latter composite is the categorical dimension and carries no information about dualizability.

• zig : zigComposite A d.copair d.pair ⋯ = CategoryTheory.CategoryStruct.id (modMulti A [M])

  The zig triangle: insert on the left, contract the trailing cross pair, on the single-factor multi-tensor at M.

• zag : zagComposite A d.copair d.pair ⋯ = CategoryTheory.CategoryStruct.id (modMulti A [M'])

  The zag triangle: insert on the right, contract the leading cross pair, on the single-factor multi-tensor at M'.

structure RS.SplittingAlgebra {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), packaged for the 2.9 consumer: a commutative algebra B under A, nonzero in the unit-detection sense, together with a global point of modTensor A M' M ⊗ B on which the base-changed evaluation returns the unit of B. Multiplication by the point produces a B-linear section of the evaluation, so the unit of B splits off the base change of modTensor A M' M.

• 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.

• point : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (modTensor A M' M) self.carrier

  The splitting point: a global element of the pairing's source, base-changed to the algebra.

• point_eval : CategoryTheory.CategoryStruct.comp self.point (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight d.pair self.carrier) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.ofBase self.carrier) CategoryTheory.MonObj.mul)) = CategoryTheory.MonObj.one

  The pairing evaluates the point to the unit of the algebra: the section identity.