Exact families of functors

Let F : K ⥤ (X ⥤ Y) be a family of functors from X to Y, parametrized by a triangulated category K. The target functor category carries the pointwise shift, so the global coherence for such a family is exactly Mathlib's ordinary F.CommShift ℤ. Its shift isomorphism is already natural in E : X and already satisfies the zero and addition laws.

Functor.ExactFamily extends that canonical structure by pointwise triangulatedness. Its mapTriangle construction fixes a triangle in K and produces the source-natural triangle in Y; pointwise distinguishedness is then a theorem. Fourier--Mukai kernel families are a principal consumer, but no kernel vocabulary belongs here.

For an actual bifunctor, Functor.ExactBifunctor is the stronger canonical root. It uses Mathlib's CommShift₂Int, including the Koszul compatibility between shifts in the two variables, and asks for triangulatedness in both slots. Explicit adapters assemble its partial shift comparisons into ordinary CommShift structures on the two functor-valued families; they are definitions rather than global instances, so they introduce no instance diamond.

structure CategoryTheory.Functor.ExactFamily {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] (F : Functor K (Functor X Y)) extends F.CommShift ℤ : Type (max (max uK uX) vY)

An exact functor-valued family.

Exactness is checked after evaluation, but all evaluated shift structures are the components of one source-natural family comparison.

• commShiftIso (a : ℤ) : (shiftFunctor K a).comp F ≅ F.comp (shiftFunctor (Functor X Y) a)
• commShiftIso_zero : commShiftIso F 0 = isoZero F ℤ
• commShiftIso_add (a b : ℤ) : commShiftIso F (a + b) = isoAdd (commShiftIso F a) (commShiftIso F b)
• triangulated (E : X) : (F.comp ((evaluation X Y).obj E)).IsTriangulated

  Every evaluated functor preserves distinguished triangles.

@[reducible]

noncomputable def CategoryTheory.Functor.ExactFamily.evaluationCommShift {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (E : X) : (F.comp ((evaluation X Y).obj E)).CommShift ℤ

Evaluate an exact family at one source object, with its chosen shift coherence exposed as a definition for local instance installation.

Equations

• h.evaluationCommShift E = CategoryTheory.Functor.CommShift.comp F ((CategoryTheory.evaluation X Y).obj E)

theorem CategoryTheory.Functor.ExactFamily.evaluationCommShift_iso_hom_app {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (E : X) (n : ℤ) (A : K) : (commShiftIso (F.comp ((evaluation X Y).obj E)) n).hom.app A = ((commShiftIso F n).hom.app A).app E

The shift comparison of an exact family, after evaluation, is the corresponding component of its global CommShift comparison.

noncomputable def CategoryTheory.Functor.ExactFamily.mapTriangle {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (T : Pretriangulated.Triangle K) : Functor X (Pretriangulated.Triangle Y)

The image of a triangle under an exact family, natural in the source object of the functors in the family.

Equations

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

@[simp]

theorem CategoryTheory.Functor.ExactFamily.mapTriangle_obj_obj₁ {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (T : Pretriangulated.Triangle K) (E : X) : ((h.mapTriangle T).obj E).obj₁ = (F.obj T.obj₁).obj E

@[simp]

theorem CategoryTheory.Functor.ExactFamily.mapTriangle_obj_obj₂ {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (T : Pretriangulated.Triangle K) (E : X) : ((h.mapTriangle T).obj E).obj₂ = (F.obj T.obj₂).obj E

@[simp]

theorem CategoryTheory.Functor.ExactFamily.mapTriangle_obj_obj₃ {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (T : Pretriangulated.Triangle K) (E : X) : ((h.mapTriangle T).obj E).obj₃ = (F.obj T.obj₃).obj E

theorem CategoryTheory.Functor.ExactFamily.mapTriangle_obj {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (T : Pretriangulated.Triangle K) (E : X) : (h.mapTriangle T).obj E = (F.comp ((evaluation X Y).obj E)).mapTriangle.obj T

Evaluation of the source-natural image triangle agrees with Mathlib's ordinary mapTriangle for the evaluated functor.

theorem CategoryTheory.Functor.ExactFamily.mapTriangle_obj_distinguished {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (T : Pretriangulated.Triangle K) (hT : T ∈ Pretriangulated.distinguishedTriangles) (E : X) : (h.mapTriangle T).obj E ∈ Pretriangulated.distinguishedTriangles

An exact family sends a distinguished parameter triangle to a triangle which is distinguished at every source object.

@[reducible, inline]

abbrev CategoryTheory.Functor.ExactFamily.distinguishedTriangleProperty {Y : Type uY} [Category.{vY, uY} Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] : ObjectProperty (Pretriangulated.Triangle Y)

The object property of being a distinguished triangle in the target.

Equations

• CategoryTheory.Functor.ExactFamily.distinguishedTriangleProperty = CategoryTheory.Pretriangulated.distinguishedTriangles

noncomputable def CategoryTheory.Functor.ExactFamily.mapDistinguishedTriangle {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (T : Pretriangulated.Triangle K) (hT : T ∈ Pretriangulated.distinguishedTriangles) : Functor X distinguishedTriangleProperty.FullSubcategory

A distinguished parameter triangle gives a source-indexed family valued in the full subcategory of distinguished target triangles.

Equations

• h.mapDistinguishedTriangle T hT = CategoryTheory.Functor.ExactFamily.distinguishedTriangleProperty.lift (h.mapTriangle T) ⋯

@[simp]

theorem CategoryTheory.Functor.ExactFamily.mapDistinguishedTriangle_obj_val {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {F : Functor K (Functor X Y)} (h : F.ExactFamily) (T : Pretriangulated.Triangle K) (hT : T ∈ Pretriangulated.distinguishedTriangles) (E : X) : ((h.mapDistinguishedTriangle T hT).obj E).obj = (h.mapTriangle T).obj E

structure CategoryTheory.Functor.ExactBifunctor {K : Type uK} {Y : Type uY} [Category.{vK, uK} K] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {K' : Type uK'} [Category.{vK', uK'} K'] [Limits.HasZeroObject K'] [HasShift K' ℤ] [Preadditive K'] [∀ (n : ℤ), (shiftFunctor K' n).Additive] [Pretriangulated K'] (F : Functor K (Functor K' Y)) extends F.CommShift₂ CategoryTheory.CommShift₂Setup.int : Type (max (max uK uK') vY)

A bifunctor exact in both variables, with one coherent choice of shift comparisons.

The CommShift₂Int parent is stronger than separately choosing a CommShift instance in each slot: it also records naturality in the other variable and the Koszul-sign compatibility between shifting the two inputs. The two triangulatedness fields then say that both partial functors preserve distinguished triangles.

• commShiftObj (X₁ : K) : (F.obj X₁).CommShift ℤ
• commShift_map {X₁ Y₁ : K} (f : X₁ ⟶ Y₁) : NatTrans.CommShift (F.map f) ℤ
• commShiftFlipObj (X₂ : K') : (F.flip.obj X₂).CommShift ℤ
• commShift_flip_map {X₂ Y₂ : K'} (g : X₂ ⟶ Y₂) : NatTrans.CommShift (F.flip.map g) ℤ
• comm (X₁ : K) (X₂ : K') (m n : ℤ) : CategoryStruct.comp ((commShiftIso (F.obj ((shiftFunctor K m).obj X₁)) n).hom.app X₂) ((shiftFunctor Y n).map ((commShiftIso (F.flip.obj X₂) m).hom.app X₁)) = CategoryStruct.comp ((commShiftIso (F.flip.obj ((shiftFunctor K' n).obj X₂)) m).hom.app X₁) (CategoryStruct.comp ((shiftFunctor Y m).map ((commShiftIso (F.obj X₁) n).hom.app X₂)) (CategoryStruct.comp (shiftComm ((F.obj X₁).obj X₂) m n).inv ((↑(CommShift₂Setup.int.ε m n)).app ((shiftFunctor Y n).obj ((shiftFunctor Y m).obj ((F.obj X₁).obj X₂))))))
• firstTriangulated (B : K') : (F.flip.obj B).IsTriangulated

  Exactness in the first variable, after fixing the second.

• secondTriangulated (A : K) : (F.obj A).IsTriangulated

  Exactness in the second variable, after fixing the first.

noncomputable def CategoryTheory.Functor.ExactBifunctor.firstFamily {K : Type uK} {Y : Type uY} [Category.{vK, uK} K] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {K' : Type uK'} [Category.{vK', uK'} K'] [Limits.HasZeroObject K'] [HasShift K' ℤ] [Preadditive K'] [∀ (n : ℤ), (shiftFunctor K' n).Additive] [Pretriangulated K'] {F : Functor K (Functor K' Y)} (h : F.ExactBifunctor) : F.ExactFamily

Forget to the exact family obtained by varying the first variable.

Here K is the parameter category and objects of K' index the evaluated partial functors K ⥤ Y.

Equations

• h.firstFamily = { toCommShift := CategoryTheory.Functor.CommShift₂.firstFamilyCommShift CategoryTheory.CommShift₂Setup.int, triangulated := ⋯ }

noncomputable def CategoryTheory.Functor.ExactBifunctor.secondFamily {K : Type uK} {Y : Type uY} [Category.{vK, uK} K] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {K' : Type uK'} [Category.{vK', uK'} K'] [Limits.HasZeroObject K'] [HasShift K' ℤ] [Preadditive K'] [∀ (n : ℤ), (shiftFunctor K' n).Additive] [Pretriangulated K'] {F : Functor K (Functor K' Y)} (h : F.ExactBifunctor) : F.flip.ExactFamily

Forget to the exact family obtained by varying the second variable.

Equations

• h.secondFamily = { toCommShift := CategoryTheory.Functor.CommShift₂.secondFamilyCommShift CategoryTheory.CommShift₂Setup.int, triangulated := ⋯ }

@[reducible]

def CategoryTheory.Functor.ExactBifunctor.firstCommShift {K : Type uK} {Y : Type uY} [Category.{vK, uK} K] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {K' : Type uK'} [Category.{vK', uK'} K'] [Limits.HasZeroObject K'] [HasShift K' ℤ] [Preadditive K'] [∀ (n : ℤ), (shiftFunctor K' n).Additive] [Pretriangulated K'] {F : Functor K (Functor K' Y)} (h : F.ExactBifunctor) (B : K') : (F.flip.obj B).CommShift ℤ

The first-variable partial functor with the shift structure selected by the bifunctor root.

Equations

• h.firstCommShift B = CategoryTheory.Functor.CommShift₂.commShiftFlipObj CategoryTheory.CommShift₂Setup.int B

@[reducible]

def CategoryTheory.Functor.ExactBifunctor.secondCommShift {K : Type uK} {Y : Type uY} [Category.{vK, uK} K] [Category.{vY, uY} Y] [Limits.HasZeroObject K] [HasShift K ℤ] [Preadditive K] [∀ (n : ℤ), (shiftFunctor K n).Additive] [Pretriangulated K] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {K' : Type uK'} [Category.{vK', uK'} K'] [Limits.HasZeroObject K'] [HasShift K' ℤ] [Preadditive K'] [∀ (n : ℤ), (shiftFunctor K' n).Additive] [Pretriangulated K'] {F : Functor K (Functor K' Y)} (h : F.ExactBifunctor) (A : K) : (F.obj A).CommShift ℤ

The second-variable partial functor with the shift structure selected by the bifunctor root.

Equations

• h.secondCommShift A = CategoryTheory.Functor.CommShift₂.commShiftObj CategoryTheory.CommShift₂Setup.int A

noncomputable def CategoryTheory.Functor.ExactBifunctor.lift₂ {Y : Type uY} [Category.{vY, uY} Y] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] {G : Functor Y (Functor Y Y)} (hG : G.ExactBifunctor) (P : ObjectProperty Y) [P.IsTriangulated] (hP : ∀ (A B : Y), P A → P B → P ((G.obj A).obj B)) : (P.lift₂ G hP).ExactBifunctor

Restrict a closed ambient exact bifunctor to a triangulated full subcategory.

The supplied closure witness is retained explicitly. This definition transports the full CommShift₂Int package (including its Koszul law) through ObjectProperty.lift₂CommShift₂Int, then uses Mathlib's canonical triangulatedness of ObjectProperty.lift in each variable. It deliberately creates no global instance.

Equations

• hG.lift₂ P hP = { toCommShift₂ := P.lift₂CommShift₂Int G hP, firstTriangulated := ⋯, secondTriangulated := ⋯ }