Linear Ext along a functor

For an R-linear abelian category C and a functor T : D ⥤ C, this file packages

(X, d) ↦ Extⁿ(X, T(d))

as a functor Cᵒᵖ ⥤ D ⥤ ModuleCat R. The derived-category Ext API already provides the groups and their two composition maps; the construction here only records their linear functoriality in a reusable, elaboration-light form.

noncomputable def MagnitudeConjecture.CategoryTheory.linearExtObjAlong {R : Type uR} [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [CategoryTheory.HasExt C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (T : CategoryTheory.Functor D C) (X : C) (n : ℕ) : CategoryTheory.Functor D (ModuleCat R)

For fixed first argument, degree, and T : D ⥤ C, Ext is a linear-module valued functor on D.

noncomputable def MagnitudeConjecture.CategoryTheory.linearExtPrecompAlong {R : Type uR} [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [CategoryTheory.HasExt C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (T : CategoryTheory.Functor D C) (n : ℕ) {X Y : C} (a : Y ⟶ X) : linearExtObjAlong T X n ⟶ linearExtObjAlong T Y n

Precomposition in the first Ext variable, natural in the variable along T.

@[simp]

theorem MagnitudeConjecture.CategoryTheory.linearExtPrecompAlong_id {R : Type uR} [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [CategoryTheory.HasExt C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (T : CategoryTheory.Functor D C) (X : C) (n : ℕ) : linearExtPrecompAlong T n (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (linearExtObjAlong T X n)

@[simp]

theorem MagnitudeConjecture.CategoryTheory.linearExtPrecompAlong_comp {R : Type uR} [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [CategoryTheory.HasExt C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (T : CategoryTheory.Functor D C) (n : ℕ) {X Y Z : C} (a : Y ⟶ X) (b : Z ⟶ Y) : linearExtPrecompAlong T n (CategoryTheory.CategoryStruct.comp b a) = CategoryTheory.CategoryStruct.comp (linearExtPrecompAlong T n a) (linearExtPrecompAlong T n b)

noncomputable def MagnitudeConjecture.CategoryTheory.linearExtAlong {R : Type uR} [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [CategoryTheory.HasExt C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (T : CategoryTheory.Functor D C) (n : ℕ) : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor D (ModuleCat R))

The linear Ext bifunctor after restricting its second variable along T.