Grothendieck classes of bounded exact sequences

This file supplies the abelian-group calculation needed to take the Euler class of a bounded cohomology sequence. For an exact pair X ⟶ Y ⟶ Z, the middle class is the sum of the two image classes. Applying that identity to the three consecutive exact pairs in

… ⟶ Aᵢ ⟶ Bᵢ ⟶ Cᵢ ⟶ Aᵢ₊₁ ⟶ …

and summing with alternating signs gives

χ(B) = χ(A) + χ(C).

The finiteness hypothesis is stated as finite support of the nonzero objects, not merely of their K₀Ab classes. A nonzero object may have zero Grothendieck class, while the proof also has to control the image objects. For bounded cohomology families the stronger objectwise statement is exactly what the usual vanishing bounds provide.

def CategoryTheory.K₀Ab.HasFiniteNonzeroSupport {A : Type u} [Category.{v, u} A] {ι : Type u_1} (X : ι → A) : Prop

An indexed family has finite nonzero support when all but finitely many of its objects are zero objects.

Equations

• CategoryTheory.K₀Ab.HasFiniteNonzeroSupport X = {i : ι | ¬CategoryTheory.Limits.IsZero (X i)}.Finite

theorem CategoryTheory.K₀Ab.of_exact {A : Type u} [Category.{v, u} A] [Abelian A] {S : ShortComplex A} (hS : S.Exact) : of S.X₂ = of (Abelian.image S.f) + of (Abelian.image S.g)

An exact pair decomposes the class of its middle object into the classes of the two images.

noncomputable def CategoryTheory.K₀Ab.eulerClass {A : Type u} [Category.{v, u} A] [Abelian A] (X : ℤ → A) : K₀Ab A

The alternating Grothendieck class of an integer-indexed family. The definition is total; the additivity theorem below uses finite nonzero support.

Equations

• CategoryTheory.K₀Ab.eulerClass X = ∑ᶠ (i : ℤ), ↑i.negOnePow • CategoryTheory.K₀Ab.of (X i)

theorem CategoryTheory.K₀Ab.eulerClass_add_of_exact {A : Type u} [Category.{v, u} A] [Abelian A] {A₀ B C : ℤ → A} (f : (i : ℤ) → A₀ i ⟶ B i) (g : (i : ℤ) → B i ⟶ C i) (δ : (i : ℤ) → C i ⟶ A₀ (i + 1)) (hfg₀ : ∀ (i : ℤ), CategoryStruct.comp (f i) (g i) = 0) (hgδ₀ : ∀ (i : ℤ), CategoryStruct.comp (g i) (δ i) = 0) (hδf₀ : ∀ (i : ℤ), CategoryStruct.comp (δ i) (f (i + 1)) = 0) (hfg : ∀ (i : ℤ), { X₁ := A₀ i, X₂ := B i, X₃ := C i, f := f i, g := g i, zero := ⋯ }.Exact) (hgδ : ∀ (i : ℤ), { X₁ := B i, X₂ := C i, X₃ := A₀ (i + 1), f := g i, g := δ i, zero := ⋯ }.Exact) (hδf : ∀ (i : ℤ), { X₁ := C i, X₂ := A₀ (i + 1), X₃ := B (i + 1), f := δ i, g := f (i + 1), zero := ⋯ }.Exact) (hA : HasFiniteNonzeroSupport A₀) (hB : HasFiniteNonzeroSupport B) (hC : HasFiniteNonzeroSupport C) : eulerClass B = eulerClass A₀ + eulerClass C

The alternating Grothendieck class is additive along a bounded ℤ-indexed long exact sequence

… ⟶ A i ⟶ B i ⟶ C i ⟶ A (i+1) ⟶ ….

There are no endpoint mono/epi hypotheses: the proof telescopes after shifting the integer index.