Theorems · Inductive type · category theory

CategoryTheory.Abelian.SpectralObject

(C : Type u_1) →
  (ι : Type u_2) →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [CategoryTheory.Category.{u_4, u_2} ι] → [CategoryTheory.Abelian C] → Type (max (max (max u_1 u_2) u_3) u_4)

A spectral object in an abelian category category C indexed by a category ι consists of a family of functors H n : ComposableArrows ι 1 ⥤ C for all n : ℤ, and a functorial long exact sequence ⋯ ⟶ (H n₀).obj (mk₁ f) ⟶ (H n₀).obj (mk₁ (f ≫ g)) ⟶ (H n₀).obj (mk₁ g) ⟶ (H n₁).obj (mk₁ f) ⟶ ⋯ when n₀ + 1 = n₁ and f and g are composable morphisms in ι. (This will be shortened as H^n₀(f) ⟶ H^n₀(f ≫ g) ⟶ H^n₀(g) ⟶ H^n₁(f) in the documentation.)

Defined in

Mathlib.Algebra.Homology.SpectralObject.Basic

Cited by

453 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Abelian