Exactness of the fibre functor from a base-change section

A short exact sequence of an abelian category does not split, so the splitting hypothesis of RS.fibreFun_shortExact is never available as stated. What Deligne's 2.10 supplies — in the form recorded by RS.Rappel210Statement — is weaker and is exactly what is needed: a section of the epimorphism after base change, that is, a morphism of module objects s : freeMod R S.X₃ ⟶ freeMod R S.X₂ splitting freeModMap R S.g.

This module derives short exactness of the realised sequence from that hypothesis alone. The route is:

• base change is exact, so S.map (tensorLeft R) is short exact whenever S is (RS.shortExact_map_tensorLeft);
• a section of a short exact sequence produces a retraction (Mathlib's ShortComplex.Splitting.ofExactOfSection), and that retraction is again a morphism of module objects — the content of RS.baseChangeRetraction_lin, proved by cancelling the monomorphism R ◁ S.f, past which the intertwining law of the retraction becomes the intertwining law of the complement of (R ◁ S.g) ≫ s, a composite of module maps;
• realisation is a functor and turns sums of module morphisms into sums, so the three splitting identities transport to the super modules, where a split short complex is short exact.

The category of module objects carries no additive structure, so the transported splitting is assembled by hand rather than through ShortComplex.Splitting.map; RS.gammaModuleFunctor_map_add is the one additivity statement this needs, phrased on underlying morphisms.

Exactness of base change is assumed as an instance hypothesis on the ambient category; for Ind C it is supplied by RS.tensorLeft_ind_preservesFiniteLimits and its colimit counterpart.

Intertwining laws in raw tensor form

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

The underlying morphism of a map of free modules intertwines the free actions, in raw tensor form.

theorem RS.lin_of_complement {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (R : D) [CategoryTheory.MonObj R] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] {V W : D} (f : CategoryTheory.MonoidalCategoryStruct.tensorObj R V ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) [CategoryTheory.Mono f] (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul W))) (u : CategoryTheory.MonoidalCategoryStruct.tensorObj R W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R V) (c : CategoryTheory.MonoidalCategoryStruct.tensorObj R W ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R W) (hc : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul W)) c = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R c) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul W))) (hid : CategoryTheory.CategoryStruct.comp u f + c = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj R W)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R W).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul W)) u = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R u) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul V))

The complement of a module endomorphism is a module map. Let f be a monomorphism intertwining the free actions, let c be an endomorphism intertwining them, and let u satisfy u ≫ f + c = 𝟙. Then u intertwines the free actions as well: the law for u is checked after f, where it becomes the law for 𝟙 - c. This is the crux of the whole module.

The retraction produced by a base-change section

theorem RS.shortExact_map_tensorLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) : (S.map (CategoryTheory.MonoidalCategory.tensorLeft R)).ShortExact

Base change of a short exact sequence is short exact. Tensoring is exact, so the whiskered sequence is again short exact.

def RS.baseChangeSectionHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) : CategoryTheory.MonoidalCategoryStruct.tensorObj R S.X₃ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S.X₂

The underlying morphism of a module-level section, in raw tensor form.

Equations

• RS.baseChangeSectionHom R s = s.hom

theorem RS.baseChangeSectionHom_g {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : CategoryTheory.CategoryStruct.comp (baseChangeSectionHom R s) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R S.g) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj R S.X₃)

A module-level section splits the base-changed epimorphism.

noncomputable def RS.baseChangeSplitting {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : (S.map (CategoryTheory.MonoidalCategory.tensorLeft R)).Splitting

The splitting of the base-changed sequence determined by a module-level section of the epimorphism.

Equations

• RS.baseChangeSplitting R hS s hs = CategoryTheory.ShortComplex.Splitting.ofExactOfSection (S.map (CategoryTheory.MonoidalCategory.tensorLeft R)) ⋯ (RS.baseChangeSectionHom R s) ⋯ ⋯

noncomputable def RS.baseChangeRetractionHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : CategoryTheory.MonoidalCategoryStruct.tensorObj R S.X₂ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S.X₁

The retraction of the base-changed sequence, in raw tensor form.

Equations

• RS.baseChangeRetractionHom R hS s hs = (RS.baseChangeSplitting R hS s hs).r

theorem RS.baseChangeRetractionHom_f {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R S.f) (baseChangeRetractionHom R hS s hs) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj R S.X₁)

The retraction retracts the base-changed monomorphism.

theorem RS.baseChangeRetractionHom_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : CategoryTheory.CategoryStruct.comp (baseChangeRetractionHom R hS s hs) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R S.f) + CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R S.g) (baseChangeSectionHom R s) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj R S.X₂)

The retraction and the section are complementary.

theorem RS.baseChangeRetraction_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R S.X₂).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul S.X₂)) (baseChangeRetractionHom R hS s hs) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (baseChangeRetractionHom R hS s hs)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R R S.X₁).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul S.X₁))

The retraction is a morphism of module objects.

noncomputable def RS.baseChangeRetraction {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : freeMod R S.X₂ ⟶ freeMod R S.X₁

The retraction, as a morphism of module objects.

Equations

• RS.baseChangeRetraction R hS s hs = CategoryTheory.Mod.Hom.mk' (RS.baseChangeRetractionHom R hS s hs) ⋯

theorem RS.freeModMap_baseChangeRetraction {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : CategoryTheory.CategoryStruct.comp (freeModMap R S.f) (baseChangeRetraction R hS s hs) = CategoryTheory.CategoryStruct.id (freeMod R S.X₁)

The module retraction retracts the base change of the monomorphism.

theorem RS.baseChangeRetraction_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] (R : D) [CategoryTheory.MonObj R] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : (CategoryTheory.CategoryStruct.comp (baseChangeRetraction R hS s hs) (freeModMap R S.f)).hom + (CategoryTheory.CategoryStruct.comp (freeModMap R S.g) s).hom = (CategoryTheory.CategoryStruct.id (freeMod R S.X₂)).hom

The module retraction and the module section are complementary, read on underlying morphisms.

Transport to the super modules

theorem RS.gammaModuleFunctor_map_add {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] {M N : CategoryTheory.Mod D R} (f g h : M ⟶ N) (hfg : f.hom + g.hom = h.hom) : (gammaModuleFunctor L R).map f + (gammaModuleFunctor L R).map g = (gammaModuleFunctor L R).map h

Realisation turns a sum of module morphisms into a sum. The category of module objects has no additive structure, so the hypothesis is stated on underlying morphisms.

noncomputable def RS.fibreFunSplitting {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : (S.map (fibreFun L R)).Splitting

The splitting of the realised sequence. Its retraction and section are the realisations of the module retraction and of the given module section; the three identities are the images of the corresponding identities in the category of module objects.

Equations

• RS.fibreFunSplitting L R hS s hs = { r := (RS.gammaModuleFunctor L R).map (RS.baseChangeRetraction R hS s hs), s := (RS.gammaModuleFunctor L R).map s, f_r := ⋯, s_g := ⋯, id := ⋯ }

theorem RS.fibreFun_shortExact_of_baseChangeSection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Abelian D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (L : OddLine D) (R : D) [CategoryTheory.MonObj R] [CategoryTheory.IsCommMonObj R] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MonoidalCategory.tensorLeft Z)] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (s : freeMod R S.X₃ ⟶ freeMod R S.X₂) (hs : CategoryTheory.CategoryStruct.comp s (freeModMap R S.g) = CategoryTheory.CategoryStruct.id (freeMod R S.X₃)) : (S.map (fibreFun L R)).ShortExact

The fibre functor carries a short exact sequence with a base-change section to a short exact sequence of super modules. No section in the ambient category is required: a section of the base-changed epimorphism as a map of module objects suffices.