Documentation

TauCeti.CategoryTheory.GrothendieckGroup.Derived

Abelian K₀ and the bounded derived category #

For an essentially small abelian category A whose bounded derived category is essentially small, this file proves that the canonical additive homomorphism

K₀(A) ⟶ K₀(Dᵇ(A)),

sending [X] to the class of the complex with X in degree zero, is an isomorphism. A short exact sequence in A gives a distinguished triangle between the corresponding degree-zero complexes, so the map is well defined.

The inverse sends the class of a bounded complex X to the alternating sum ∑ n, (-1)ⁿ [Hⁿ X] of its cohomology classes. Consequently, the comparison identifies a bounded complex in triangulated K₀ with the alternating sum of its cohomology objects placed in degree zero.

Main definitions #

Main results #

Mathlib infrastructure #

The degree-zero embedding DerivedCategory.singleFunctor, the distinguished triangle ShortComplex.ShortExact.singleTriangle, the long exact cohomology sequence DerivedCategory.HomologySequence and the representation of bounded objects by bounded complexes DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE are from Mathlib's derived-category API.

References #

Bounded derived category infrastructure #

source
theorem TauCeti.TriangulatedK0.of_singleFunctor_shortExact {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] {S : CategoryTheory.ShortComplex A} (hS : S.ShortExact) :
of ((DerivedCategory.Bounded.singleFunctor A 0).obj S.X₂) = of ((DerivedCategory.Bounded.singleFunctor A 0).obj S.X₁) + of ((DerivedCategory.Bounded.singleFunctor A 0).obj S.X₃)

A short exact sequence gives a distinguished triangle in the bounded derived category, so its degree-zero objects satisfy the triangulated K₀ relation.

The alternating class of the cohomology #

source
theorem TauCeti.AbelianK0.sum_negOnePow_of_homology_of_distTriang {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] {T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory A)} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) {s : Finset ℤ} (h₁ : ∀ n ∉ s, CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor A n).obj T.obj₁)) (h₃ : ∀ n ∉ s, CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor A n).obj T.obj₃)) :
∑ n ∈ s, ↑n.negOnePow • of ((DerivedCategory.homologyFunctor A n).obj T.obj₂) = ∑ n ∈ s, ↑n.negOnePow • of ((DerivedCategory.homologyFunctor A n).obj T.obj₁) + ∑ n ∈ s, ↑n.negOnePow • of ((DerivedCategory.homologyFunctor A n).obj T.obj₃)

The alternating class of the cohomology is additive on distinguished triangles. For a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ in the derived category and a finite set s of degrees outside which the cohomology of X and Z vanishes, ∑ n ∈ s, (-1)ⁿ [Hⁿ Y] = ∑ n ∈ s, (-1)ⁿ [Hⁿ X] + ∑ n ∈ s, (-1)ⁿ [Hⁿ Z] in abelian K₀.

The comparison equivalence #

source
noncomputable def TauCeti.AbelianK0.toBoundedDerivedK0 {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] :
AbelianK0 A →+ TriangulatedK0 (DerivedCategory.Bounded A)

The canonical homomorphism from abelian K₀ to the triangulated K₀ of the bounded derived category. It sends the class of an object to the class of the complex concentrated in degree zero.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AbelianK0.toBoundedDerivedK0_of {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] (X : A) :
    toBoundedDerivedK0 (of X) = TriangulatedK0.of ((DerivedCategory.Bounded.singleFunctor A 0).obj X)

    The canonical map to derived K₀ sends an object class to the class of its degree-zero complex.

    source
    noncomputable def TauCeti.AbelianK0.boundedDerivedK0Equiv (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] :
    AbelianK0 A ≃+ TriangulatedK0 (DerivedCategory.Bounded A)

    Abelian K₀ is triangulated K₀ of the bounded derived category. The class of an object goes to the class of that object placed in degree zero, and in the inverse direction the class of a bounded complex goes to the alternating sum of the classes of its cohomology objects.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.AbelianK0.boundedDerivedK0Equiv_toAddMonoidHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] :
      ↑(boundedDerivedK0Equiv A) = toBoundedDerivedK0

      The forward map of TauCeti.AbelianK0.boundedDerivedK0Equiv is TauCeti.AbelianK0.toBoundedDerivedK0.

      source
      @[simp]
      theorem TauCeti.AbelianK0.boundedDerivedK0Equiv_of {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] (X : A) :
      (boundedDerivedK0Equiv A) (of X) = TriangulatedK0.of ((DerivedCategory.Bounded.singleFunctor A 0).obj X)

      TauCeti.AbelianK0.boundedDerivedK0Equiv sends the class of an object to the class of that object placed in degree zero.

      source
      @[simp]
      theorem TauCeti.AbelianK0.boundedDerivedK0Equiv_symm_of_singleFunctor {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] (X : A) :
      (boundedDerivedK0Equiv A).symm (TriangulatedK0.of ((DerivedCategory.Bounded.singleFunctor A 0).obj X)) = of X

      The inverse comparison sends a degree-zero complex to its class in abelian K₀.

      source
      theorem TauCeti.AbelianK0.boundedDerivedK0Equiv_symm_of {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] (X : DerivedCategory.Bounded A) {s : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor A n).obj X.obj)) :
      (boundedDerivedK0Equiv A).symm (TriangulatedK0.of X) = ∑ n ∈ s, ↑n.negOnePow • of ((DerivedCategory.homologyFunctor A n).obj X.obj)

      The inverse of TauCeti.AbelianK0.boundedDerivedK0Equiv sends the class of a bounded complex to the alternating sum of the classes of its cohomology objects, summed over any finite set of degrees outside which the cohomology vanishes.

      source
      theorem TauCeti.TriangulatedK0.of_eq_sum_homology {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] [HasDerivedCategory A] [CategoryTheory.EssentiallySmall.{w'', w', max u v} (DerivedCategory.Bounded A)] (X : DerivedCategory.Bounded A) {s : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor A n).obj X.obj)) :
      of X = ∑ n ∈ s, ↑n.negOnePow • of ((DerivedCategory.Bounded.singleFunctor A 0).obj ((DerivedCategory.homologyFunctor A n).obj X.obj))

      The class of a bounded complex in triangulated K₀ of the bounded derived category is the alternating sum of the classes of its cohomology objects, each placed in degree zero. The sum runs over any finite set of degrees outside which the cohomology vanishes.