Abelian subcategories of triangulated categories

Let ι : A ⥤ C be a fully faithful additive functor where A is an additive category and C is a triangulated category. We show that A is an abelian category if the following conditions are satisfied:

• For any object X and Y in A, there is no nonzero morphism ι.obj X ⟶ (ι.obj Y)⟦n⟧ when n < 0.
• Any morphism f₁ : X₁ ⟶ X₂ in A is admissible, i.e. when we complete ι.obj f₁ in a distinguished triangle ι.obj X₁ ⟶ ι.obj X₂ ⟶ X₃ ⟶ (ι.obj X₁)⟦1⟧, there exists objects K and Q, and a distinguished triangle (ι.obj K)⟦1⟧ ⟶ X₃ ⟶ (ι.obj Q) ⟶ ....

References

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

theorem CategoryTheory.Triangulated.AbelianSubcategory.eq_zero_of_hom_shift_pos {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X Y : A} {n : ℤ} (f : (shiftFunctor C n).obj (ι.obj X) ⟶ ι.obj Y) (hn : 0 < n) : f = 0

noncomputable def CategoryTheory.Triangulated.AbelianSubcategory.ιK {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [HasShift C ℤ] [Category.{v_2, u_2} A] {ι : Functor A C} {X₁ : A} {X₃ : C} (f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)) {K : A} (α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [ι.Full] : K ⟶ X₁

The inclusion of the kernel.

Equations

• CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α = (ι.comp (CategoryTheory.shiftFunctor C 1)).preimage (CategoryTheory.CategoryStruct.comp α f₃)

noncomputable def CategoryTheory.Triangulated.AbelianSubcategory.πQ {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} A] {ι : Functor A C} {X₂ : A} {X₃ : C} (f₂ : ι.obj X₂ ⟶ X₃) {Q : A} (β : X₃ ⟶ ι.obj Q) [ι.Full] : X₂ ⟶ Q

The projection to the cokernel.

Equations

• CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β = ι.preimage (CategoryTheory.CategoryStruct.comp f₂ β)

@[simp]

theorem CategoryTheory.Triangulated.AbelianSubcategory.shift_ι_map_ιK {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [HasShift C ℤ] [Category.{v_2, u_2} A] {ι : Functor A C} {X₁ : A} {X₃ : C} (f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)) {K : A} (α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [ι.Full] : (shiftFunctor C 1).map (ι.map (ιK f₃ α)) = CategoryStruct.comp α f₃

theorem CategoryTheory.Triangulated.AbelianSubcategory.shift_ι_map_ιK_assoc {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [HasShift C ℤ] [Category.{v_2, u_2} A] {ι : Functor A C} {X₁ : A} {X₃ : C} (f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)) {K : A} (α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [ι.Full] {Z : C} (h : (shiftFunctor C 1).obj (ι.obj X₁) ⟶ Z) : CategoryStruct.comp ((shiftFunctor C 1).map (ι.map (ιK f₃ α))) h = CategoryStruct.comp α (CategoryStruct.comp f₃ h)

@[simp]

theorem CategoryTheory.Triangulated.AbelianSubcategory.ι_map_πQ {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} A] {ι : Functor A C} {X₂ : A} {X₃ : C} (f₂ : ι.obj X₂ ⟶ X₃) {Q : A} (β : X₃ ⟶ ι.obj Q) [ι.Full] : ι.map (πQ f₂ β) = CategoryStruct.comp f₂ β

theorem CategoryTheory.Triangulated.AbelianSubcategory.ι_map_πQ_assoc {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} A] {ι : Functor A C} {X₂ : A} {X₃ : C} (f₂ : ι.obj X₂ ⟶ X₃) {Q : A} (β : X₃ ⟶ ι.obj Q) [ι.Full] {Z : C} (h : ι.obj Q ⟶ Z) : CategoryStruct.comp (ι.map (πQ f₂ β)) h = CategoryStruct.comp f₂ (CategoryStruct.comp β h)

theorem CategoryTheory.Triangulated.AbelianSubcategory.ιK_mor₁ {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K : A} (α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [ι.Full] [Preadditive A] [ι.Faithful] : CategoryStruct.comp (ιK f₃ α) f₁ = 0

theorem CategoryTheory.Triangulated.AbelianSubcategory.ιK_mor₁_assoc {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K : A} (α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [ι.Full] [Preadditive A] [ι.Faithful] {Z : A} (h : X₂ ⟶ Z) : CategoryStruct.comp (ιK f₃ α) (CategoryStruct.comp f₁ h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Triangulated.AbelianSubcategory.mor₁_πQ {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {Q : A} (β : X₃ ⟶ ι.obj Q) [ι.Full] [Preadditive A] [ι.Faithful] : CategoryStruct.comp f₁ (πQ f₂ β) = 0

theorem CategoryTheory.Triangulated.AbelianSubcategory.mor₁_πQ_assoc {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {Q : A} (β : X₃ ⟶ ι.obj Q) [ι.Full] [Preadditive A] [ι.Faithful] {Z : A} (h : Q ⟶ Z) : CategoryStruct.comp f₁ (CategoryStruct.comp (πQ f₂ β) h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Triangulated.AbelianSubcategory.mono_ιK {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K Q : A} {α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q} {γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))} (hT' : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [ι.Full] [Preadditive A] [ι.Faithful] : Mono (ιK f₃ α)

theorem CategoryTheory.Triangulated.AbelianSubcategory.epi_πQ {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K Q : A} {α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q} {γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))} (hT' : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [ι.Full] [Preadditive A] [ι.Faithful] : Epi (πQ f₂ β)

theorem CategoryTheory.Triangulated.AbelianSubcategory.exists_lift_ιK {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K Q : A} {α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q} {γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))} (hT' : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [ι.Full] [Preadditive A] [ι.Faithful] {B : A} (x₁ : B ⟶ X₁) (hx₁ : CategoryStruct.comp x₁ f₁ = 0) : ∃ (k : B ⟶ K), CategoryStruct.comp k (ιK f₃ α) = x₁

noncomputable def CategoryTheory.Triangulated.AbelianSubcategory.isLimitKernelFork {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K Q : A} {α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q} {γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))} (hT' : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [ι.Full] [Preadditive A] [ι.Faithful] : Limits.IsLimit (Limits.KernelFork.ofι (ιK f₃ α) ⋯)

ιK is a kernel.

Equations

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

theorem CategoryTheory.Triangulated.AbelianSubcategory.exists_desc_πQ {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K Q : A} {α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q} {γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))} (hT' : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [ι.Full] [Preadditive A] [ι.Faithful] {B : A} (x₂ : X₂ ⟶ B) (hx₂ : CategoryStruct.comp f₁ x₂ = 0) : ∃ (k : Q ⟶ B), CategoryStruct.comp (πQ f₂ β) k = x₂

noncomputable def CategoryTheory.Triangulated.AbelianSubcategory.isColimitCokernelCofork {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K Q : A} {α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q} {γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))} (hT' : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [ι.Full] [Preadditive A] [ι.Faithful] : Limits.IsColimit (Limits.CokernelCofork.ofπ (πQ f₂ β) ⋯)

πQ is a cokernel.

Equations

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

theorem CategoryTheory.Triangulated.AbelianSubcategory.hasKernel {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K Q : A} {α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q} {γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))} (hT' : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [ι.Full] [Preadditive A] [ι.Faithful] : Limits.HasKernel f₁

theorem CategoryTheory.Triangulated.AbelianSubcategory.hasCokernel {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃} {f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)} (hT : Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ Pretriangulated.distinguishedTriangles) {K Q : A} {α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q} {γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))} (hT' : Pretriangulated.Triangle.mk α β γ ∈ Pretriangulated.distinguishedTriangles) [ι.Full] [Preadditive A] [ι.Faithful] : Limits.HasCokernel f₁

def CategoryTheory.Triangulated.AbelianSubcategory.admissibleMorphism {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] (ι : Functor A C) : MorphismProperty A

Given a functor ι : A ⥤ C from a preadditive category to a triangulated category, a morphism X₁ ⟶ X₂ in A is admissible if, when we complete ι.obj f₁ in a distinguished triangle ι.obj X₁ ⟶ ι.obj X₂ ⟶ X₃ ⟶ (ι.obj X₁)⟦1⟧, there exists objects K and Q, and a distinguished triangle (ι.obj K)⟦1⟧ ⟶ X₃ ⟶ (ι.obj Q) ⟶ ....

Equations

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

theorem CategoryTheory.Triangulated.AbelianSubcategory.hasKernel_of_admissibleMorphism {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) [Preadditive A] [ι.Full] [ι.Faithful] {X₁ X₂ : A} (f₁ : X₁ ⟶ X₂) (hf₁ : admissibleMorphism ι f₁) : Limits.HasKernel f₁

theorem CategoryTheory.Triangulated.AbelianSubcategory.hasCokernel_of_admissibleMorphism {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) [Preadditive A] [ι.Full] [ι.Faithful] {X₁ X₂ : A} (f₁ : X₁ ⟶ X₂) (hf₁ : admissibleMorphism ι f₁) : Limits.HasCokernel f₁

noncomputable def CategoryTheory.Triangulated.AbelianSubcategory.isLimitKernelForkOfDistTriang {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) [Preadditive A] [ι.Full] [ι.Faithful] [Limits.HasFiniteProducts A] [ι.Additive] {X₁ X₂ X₃ : A} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)) (hT : Pretriangulated.Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ Pretriangulated.distinguishedTriangles) : Limits.IsLimit (Limits.KernelFork.ofι f₁ ⋯)

If ι.obj X₁ ⟶ ι.obj X₂ ⟶ ι.obj X₃ ⟶ ... is a distinguished triangle, then X₁ is a kernel of X₂ ⟶ X₃.

Equations

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

noncomputable def CategoryTheory.Triangulated.AbelianSubcategory.isColimitCokernelCoforkOfDistTriang {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) [Preadditive A] [ι.Full] [ι.Faithful] [Limits.HasFiniteProducts A] [ι.Additive] {X₁ X₂ X₃ : A} (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)) (hT : Pretriangulated.Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ Pretriangulated.distinguishedTriangles) : Limits.IsColimit (Limits.CokernelCofork.ofπ f₂ ⋯)

If ι.obj X₁ ⟶ ι.obj X₂ ⟶ ι.obj X₃ ⟶ ... is a distinguished triangle, then X₃ is a cokernel of X₁ ⟶ X₂.

Equations

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

theorem CategoryTheory.Triangulated.AbelianSubcategory.exists_distinguished_triangle_of_epi {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] {ι : Functor A C} (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) [Preadditive A] [ι.Full] [ι.Faithful] [ι.Additive] (hA : admissibleMorphism ι = ⊤) {X₂ X₃ : A} (π : X₂ ⟶ X₃) [Epi π] : ∃ (X₁ : A) (i : X₁ ⟶ X₂) (δ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)), Pretriangulated.Triangle.mk (ι.map i) (ι.map π) δ ∈ Pretriangulated.distinguishedTriangles

noncomputable def CategoryTheory.Triangulated.AbelianSubcategory.abelian {C : Type u_1} {A : Type u_2} [Category.{v_1, u_1} C] [Limits.HasZeroObject C] [Preadditive C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Category.{v_2, u_2} A] (ι : Functor A C) (hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) [Preadditive A] [ι.Full] [ι.Faithful] [Limits.HasFiniteProducts A] [ι.Additive] (hA : admissibleMorphism ι = ⊤) [IsTriangulated C] : Abelian A

Let ι : A ⥤ C be a fully faithful additive functor where A is an additive category and C is a triangulated category. The category A is abelian if the following conditions are satisfied:

• For any object X and Y in A, there is no nonzero morphism ι.obj X ⟶ (ι.obj Y)⟦n⟧ when n < 0.
• Any morphism f₁ : X₁ ⟶ X₂ in A is admissible, i.e. when we complete ι.obj f₁ in a distinguished triangle ι.obj X₁ ⟶ ι.obj X₂ ⟶ X₃ ⟶ (ι.obj X₁)⟦1⟧, there exists objects K and Q, and a distinguished triangle (ι.obj K)⟦1⟧ ⟶ X₃ ⟶ (ι.obj Q) ⟶ ....

Equations

• CategoryTheory.Triangulated.AbelianSubcategory.abelian ι hι hA = CategoryTheory.Abelian.mk' ⋯