Single objects and short exact triangles in the bounded derived category

The single functors into the derived category lift to its bounded subcategory in every degree. A short exact sequence then gives a distinguished triangle of bounded single objects.

References

• Mathlib's Mathlib/Algebra/Homology/DerivedCategory/Plus.lean, whose lift of the single functors to the bounded-below derived category supplies the pattern used here.

@[reducible, inline]

noncomputable abbrev TauCeti.DerivedCategory.Bounded.singleFunctor (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (n : ℤ) : CategoryTheory.Functor A (DerivedCategory.Bounded A)

The functor sending an object to a complex concentrated in degree n.

noncomputable def TauCeti.DerivedCategory.Bounded.singleFunctors (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] : CategoryTheory.SingleFunctors A (DerivedCategory.Bounded A) ℤ

The single functors into the bounded derived category, with their shift compatibilities.

@[simp]

theorem TauCeti.DerivedCategory.Bounded.singleFunctors_functor {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (n : ℤ) : (singleFunctors A).functor n = singleFunctor A n

The nth bounded single functor is singleFunctor A n.

instance TauCeti.DerivedCategory.Bounded.instAdditiveBoundedSingleFunctor {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] (n : ℤ) : (singleFunctor A n).Additive

The bounded single functors are additive, as the derived single functors are.

@[implicit_reducible]

noncomputable def CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangle {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : Pretriangulated.Triangle (DerivedCategory.Bounded A)

The triangle of bounded single objects associated with a short exact sequence.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangle_obj₂ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangle.obj₂ = (TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangle_obj₁ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangle.obj₁ = (TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangle_mor₃ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangle.mor₃ = ObjectProperty.homMk (CategoryStruct.comp hS.singleδ ((Functor.commShiftIso DerivedCategory.Bounded.ι 1).inv.app ((TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₁)))

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangle_mor₂ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangle.mor₂ = (TauCeti.DerivedCategory.Bounded.singleFunctor A 0).map S.g

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangle_obj₃ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangle.obj₃ = (TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₃

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangle_mor₁ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangle.mor₁ = (TauCeti.DerivedCategory.Bounded.singleFunctor A 0).map S.f

noncomputable def CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangleιIso {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : DerivedCategory.Bounded.ι.mapTriangle.obj hS.boundedSingleTriangle ≅ hS.singleTriangle

Inclusion identifies the bounded single triangle with the derived single triangle.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangleιIso_hom_hom₃ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangleιIso.hom.hom₃ = CategoryStruct.id ((TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₃).obj

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangleιIso_hom_hom₁ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangleιIso.hom.hom₁ = CategoryStruct.id ((TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₁).obj

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangleιIso_inv_hom₁ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangleιIso.inv.hom₁ = CategoryStruct.id ((TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₁).obj

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangleιIso_inv_hom₃ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangleιIso.inv.hom₃ = CategoryStruct.id ((TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₃).obj

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangleιIso_hom_hom₂ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangleιIso.hom.hom₂ = CategoryStruct.id ((TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₂).obj

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangleιIso_inv_hom₂ {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangleιIso.inv.hom₂ = CategoryStruct.id ((TauCeti.DerivedCategory.Bounded.singleFunctor A 0).obj S.X₂).obj

theorem CategoryTheory.ShortComplex.ShortExact.boundedSingleTriangle_distinguished {A : Type u} [Category.{v, u} A] [Abelian A] [HasDerivedCategory A] {S : ShortComplex A} (hS : S.ShortExact) : hS.boundedSingleTriangle ∈ Pretriangulated.distinguishedTriangles

The bounded single triangle of a short exact sequence is distinguished.