Documentation

TauCeti.Algebra.Homology.ShortComplex.Splice

Splicing short exact sequences #

A bi-infinite sequence Zⁿ → Pⁿ → Zⁿ⁺¹ of short complexes gives a cochain complex on the middle terms. Its differential is the projection of one short complex followed by the inclusion of the next. When the short complexes are short exact, the resulting complex is acyclic and its cycles are the first terms of the short complexes. This construction turns successive presentations and copresentations into complete resolutions.

References #

Implementation notes #

The constructor is an exposed abbreviation, like Mathlib's CochainComplex.of: its terms must reduce to the prescribed middle objects for the statements of splice_d, spliceCyclesIso_hom_iCycles, and spliceCyclesIso_inv_f to typecheck. The equality splice_X does not provide this definitional equality; an unexposed constructor would require transporting the morphisms along that equality in these statements.

source
@[reducible, inline]
noncomputable abbrev CochainComplex.splice {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) :
CochainComplex C ℤ

Splice successive short complexes along the specified identifications of their end terms. The objects are their middle terms and the differential is g ≫ e.hom ≫ f.

Instances For
    source
    @[simp]
    theorem CochainComplex.splice_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (n : ℤ) :
    (splice S e).X n = (S n).X₂

    The term in degree n of the spliced complex is the middle term of the n-th short complex.

    source
    theorem CochainComplex.splice_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (n : ℤ) :
    (splice S e).d n (n + 1) = CategoryTheory.CategoryStruct.comp (S n).g (CategoryTheory.CategoryStruct.comp (e n).hom (S (n + 1)).f)

    The differential of the spliced complex is the projection followed by the connecting isomorphism and the next inclusion.

    source
    theorem CochainComplex.acyclic_splice {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (hS : ∀ (n : ℤ), (S n).ShortExact) :
    HomologicalComplex.Acyclic (splice S e)

    Splicing short exact sequences produces an acyclic cochain complex.

    source
    noncomputable def CochainComplex.spliceCyclesIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (hS : ∀ (n : ℤ), (S n).ShortExact) (n : ℤ) :
    (S n).X₁ ≅ HomologicalComplex.cycles (splice S e) n

    The cycles of the spliced complex identify with the first term of each short exact sequence. The isomorphism is oriented from the prescribed cycle object into the categorical cycles.

    Instances For
      source
      @[simp]
      theorem CochainComplex.spliceCyclesIso_hom_iCycles {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (hS : ∀ (n : ℤ), (S n).ShortExact) (n : ℤ) :
      CategoryTheory.CategoryStruct.comp (spliceCyclesIso S e hS n).hom (HomologicalComplex.iCycles (splice S e) n) = (S n).f

      The cycles comparison identifies the given inclusion with the categorical cycle inclusion.

      source
      @[simp]
      theorem CochainComplex.spliceCyclesIso_hom_iCycles_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (hS : ∀ (n : ℤ), (S n).ShortExact) (n : ℤ) {Z : C} (h : (S n).X₂ ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (spliceCyclesIso S e hS n).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (splice S e) n) h) = CategoryTheory.CategoryStruct.comp (S n).f h

      The cycles comparison identifies the given inclusion with the categorical cycle inclusion.

      source
      @[simp]
      theorem CochainComplex.spliceCyclesIso_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (hS : ∀ (n : ℤ), (S n).ShortExact) (n : ℤ) :
      CategoryTheory.CategoryStruct.comp (spliceCyclesIso S e hS n).inv (S n).f = HomologicalComplex.iCycles (splice S e) n

      The inverse cycles comparison recovers the categorical cycle inclusion.

      source
      @[simp]
      theorem CochainComplex.spliceCyclesIso_inv_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (S : ℤ → CategoryTheory.ShortComplex C) (e : (n : ℤ) → (S n).X₃ ≅ (S (n + 1)).X₁) (hS : ∀ (n : ℤ), (S n).ShortExact) (n : ℤ) {Z : C} (h : (S n).X₂ ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (spliceCyclesIso S e hS n).inv (CategoryTheory.CategoryStruct.comp (S n).f h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (splice S e) n) h

      The inverse cycles comparison recovers the categorical cycle inclusion.