Documentation

TauCeti.CategoryTheory.Exact.Resolution.ProjectiveResolution

Finite resolutions in abelian categories are projective resolutions #

For the canonical exact structure of an abelian category, the conflations of a finite resolution

K₁ ↪ Q₀ ↠ X,   K₂ ↪ Q₁ ↠ K₁,   …,   Kₙ ↪ Qₙ₋₁ ↠ Kₙ₋₁

are short exact sequences, so the spliced complex 0 ⟶ Kₙ ⟶ Qₙ₋₁ ⟶ ⋯ ⟶ Q₀ is exact in positive degrees and its augmentation Q₀ ⟶ X is an epimorphism with kernel the image of Q₁ ⟶ Q₀. When the resolving terms are projective, this is a projective resolution of X in Mathlib's sense, bounded by the length of the resolution. This makes the recursive data produced by dimension shifting usable with Mathlib's comparison theory of projective resolutions, which only sees chain complexes.

Conversely, a projective resolution in Mathlib's sense whose term in degree n + 1 vanishes is, by TauCeti.ExactStructure.FiniteResolution.ofChainComplex, a finite resolution by projective objects of length n, so the Euler-class and resolution-theorem API of finite resolutions applies to it.

Main definitions #

Main results #

source
instance TauCeti.ExactStructure.FiniteResolution.epi_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} (r : (abelian C).FiniteResolution P X) :
CategoryTheory.Epi r.aug

The augmentation of a finite resolution in an abelian category is an epimorphism.

source
theorem TauCeti.ExactStructure.FiniteResolution.exact_d_zero_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} (r : (abelian C).FiniteResolution P X) :
{ X₁ := r.term (0 + 1), X₂ := r.term 0, X₃ := X, f := r.d 0, g := r.aug, zero := ⋯ }.Exact

The augmented complex of a finite resolution in an abelian category is exact at its degree-zero term: the kernel of the augmentation is the image of the first differential.

source
theorem TauCeti.ExactStructure.FiniteResolution.exact_d_succ_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} (r : (abelian C).FiniteResolution P X) (n : ℕ) :
{ X₁ := r.term (n + 1 + 1), X₂ := r.term (n + 1), X₃ := r.term n, f := r.d (n + 1), g := r.d n, zero := ⋯ }.Exact

The complex of a finite resolution in an abelian category is exact in every positive degree.

source
theorem TauCeti.ExactStructure.FiniteResolution.exactAt_toChainComplex_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} {X : C} (r : (abelian C).FiniteResolution P X) (n : ℕ) :
HomologicalComplex.ExactAt r.toChainComplex (n + 1)

The complex of a finite resolution in an abelian category is exact in every positive degree, in the vocabulary of homological complexes.

source
noncomputable def TauCeti.ExactStructure.FiniteResolution.toProjectiveResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} (hP : P ≤ CategoryTheory.isProjective C) {X : C} (r : (abelian C).FiniteResolution P X) :
CategoryTheory.ProjectiveResolution X

A finite resolution by projective objects in an abelian category is a projective resolution in Mathlib's sense: its complex is the spliced complex of the resolution, which vanishes beyond the length, and the quasi-isomorphism to X is the augmentation.

The proof that the augmentation is a quasi-isomorphism follows that of Mathlib's CategoryTheory.ProjectiveResolution.of in Mathlib/CategoryTheory/Abelian/Projective/Resolution (by Markus Himmel, Kim Morrison, Jakob von Raumer and Joël Riou).

Instances For
    source
    noncomputable def TauCeti.ExactStructure.FiniteResolution.toProjectiveResolutionXIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} (hP : P ≤ CategoryTheory.isProjective C) {X : C} (r : (abelian C).FiniteResolution P X) (n : ℕ) :
    (toProjectiveResolution hP r).complex.X n ≅ r.term n

    The terms of the projective resolution are the terms of the finite resolution.

    Instances For
      source
      theorem TauCeti.ExactStructure.FiniteResolution.isZero_toProjectiveResolution_X_of_length_lt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} (hP : P ≤ CategoryTheory.isProjective C) {X : C} (r : (abelian C).FiniteResolution P X) {n : ℕ} (hn : r.length < n) :
      CategoryTheory.Limits.IsZero ((toProjectiveResolution hP r).complex.X n)

      The projective resolution vanishes above the length of the finite resolution.

      source
      @[simp]
      theorem TauCeti.ExactStructure.FiniteResolution.toProjectiveResolution_complex_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} (hP : P ≤ CategoryTheory.isProjective C) {X : C} (r : (abelian C).FiniteResolution P X) (n : ℕ) :
      (toProjectiveResolution hP r).complex.d (n + 1) n = CategoryTheory.CategoryStruct.comp (toProjectiveResolutionXIso hP r (n + 1)).hom (CategoryTheory.CategoryStruct.comp (r.d n) (toProjectiveResolutionXIso hP r n).inv)

      The differentials of the projective resolution are those of the finite resolution, through the identifications of the terms.

      source
      @[simp]
      theorem TauCeti.ExactStructure.FiniteResolution.toProjectiveResolution_π_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P : CategoryTheory.ObjectProperty C} (hP : P ≤ CategoryTheory.isProjective C) {X : C} (r : (abelian C).FiniteResolution P X) :
      (toProjectiveResolution hP r).π.f 0 = CategoryTheory.CategoryStruct.comp (toProjectiveResolutionXIso hP r 0).hom r.aug

      The augmentation of the projective resolution is that of the finite resolution, through the identification of the degree-zero terms.

      source
      noncomputable def CategoryTheory.ProjectiveResolution.toFiniteResolution {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (R : ProjectiveResolution X) {n : ℕ} (hn : Limits.IsZero (R.complex.X (n + 1))) :
      (TauCeti.ExactStructure.abelian C).FiniteResolution (isProjective C) X

      A projective resolution whose term in degree n + 1 vanishes, as a finite resolution of length n by projective objects for the canonical exact structure. Only that single term needs to vanish: the terms above n + 1 are not constrained.

      Instances For
        source
        @[simp]
        theorem CategoryTheory.ProjectiveResolution.length_toFiniteResolution {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (R : ProjectiveResolution X) {n : ℕ} (hn : Limits.IsZero (R.complex.X (n + 1))) :
        (R.toFiniteResolution hn).length = n

        The finite resolution of a projective resolution with vanishing term in degree n + 1 has length n.

        source
        theorem CategoryTheory.ProjectiveResolution.foldAlternating_toFiniteResolution {C : Type u} [Category.{v, u} C] [Abelian C] {X : C} (R : ProjectiveResolution X) {n : ℕ} (hn : Limits.IsZero (R.complex.X (n + 1))) {A : Type u_1} [AddCommGroup A] (f : (Z : C) → isProjective C Z → A) (hf : ∀ {Y Z : C} (x : Y ≅ Z) (hY : isProjective C Y) (hZ : isProjective C Z), f Y hY = f Z hZ) :
        TauCeti.ExactStructure.FiniteResolution.foldAlternating f (R.toFiniteResolution hn) = ∑ i : Fin (n + 1), (-1) ^ ↑i • f (R.complex.X ↑i) ⋯

        Alternating sums along the finite resolution of a projective resolution with vanishing term in degree n + 1 are the alternating sums over its terms of degree at most n.