The local splitting statement

Deligne's 2.10, the consumed form: over a category where the tensor structure is exact, every short exact sequence splits after base change to some nonzero commutative algebra. The splitting is a section of the base-changed epimorphism as module maps over the algebra.

theorem RS.freeModMap_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {V W : D} (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul W))

The action square of the free module on a morphism.

noncomputable def RS.freeModMap {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {V W : D} (f : V ⟶ W) : freeMod A V ⟶ freeMod A W

The free module on a morphism.

Equations

• RS.freeModMap A f = CategoryTheory.Mod.Hom.mk' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) ⋯

def RS.Rappel210Statement {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex D) : S.ShortExact → Prop

The local splitting statement of record (Deligne 2.10, the consumed direction): a short exact sequence acquires a module-level section of its epimorphism after base change to some nonzero commutative algebra.

Equations

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