t-exact functors

Given a triangulated functor F : C ⥤ D where both C and D are equipped with t-structures t₁ and t₂, we introduce typeclasses F.LeftTExact t₁ t₂, F.RightTExact t₁ t₂ and F.TExact t₁ t₂ which correspond to the notion of left t-exact, right t-exact and t-exact functors.

References

• Beilinson, Bernstein, Deligne, Gabber, Faisceaux pervers, 1.2

class CategoryTheory.Functor.LeftTExact {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (t₁ : Triangulated.TStructure C) (t₂ : Triangulated.TStructure D) : Prop

A triangulated functor F is left t-exact if X ≥ n implies F.obj X ≥ n. (It suffices to test this for n := 0, see LeftExact.mk.)

• mk' :: (
• isGE_obj (X : C) (n : ℤ) [t₁.IsGE X n] : t₂.IsGE (F.obj X) n
• )

class CategoryTheory.Functor.RightTExact {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (t₁ : Triangulated.TStructure C) (t₂ : Triangulated.TStructure D) : Prop

A triangulated functor F is right t-exact if X ≤ n implies F.obj X ≤ n. (It suffices to test this for n := 0, see RightExact.mk.)

• mk' :: (
• isLE_obj (X : C) (n : ℤ) [t₁.IsLE X n] : t₂.IsLE (F.obj X) n
• )

class CategoryTheory.Functor.TExact {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (t₁ : Triangulated.TStructure C) (t₂ : Triangulated.TStructure D) : Prop

A triangulated functor is t-exact if it is both left and right t-exact.

• rightTExact : F.RightTExact t₁ t₂
• leftTExact : F.LeftTExact t₁ t₂

theorem CategoryTheory.Functor.LeftTExact.mk {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (t₁ : Triangulated.TStructure C) (t₂ : Triangulated.TStructure D) (isGE_obj_zero : ∀ (X : C) [t₁.IsGE X 0], t₂.IsGE (F.obj X) 0) : F.LeftTExact t₁ t₂

Constructor for LeftTExact.

theorem CategoryTheory.Functor.RightTExact.mk {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [HasShift C ℤ] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated C] [Pretriangulated D] (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (t₁ : Triangulated.TStructure C) (t₂ : Triangulated.TStructure D) (isLE_obj_zero : ∀ (X : C) [t₁.IsLE X 0], t₂.IsLE (F.obj X) 0) : F.RightTExact t₁ t₂

Constructor for RightTExact.