Documentation

TauCeti.CategoryTheory.Exact.Acyclic

Acyclic complexes over an exact category #

A cochain complex K over an exact category is acyclic when each differential factors as a deflation followed by an inflation, Kⁿ ↠ Zⁿ⁺¹ ↣ Kⁿ⁺¹, such that every sequence Zⁿ ↣ Kⁿ ↠ Zⁿ⁺¹ is a conflation (Bühler, Definition 10.1). For the abelian exact structure these are the exact complexes. Acyclic complexes are the complexes inverted to zero in the derived category of an exact category.

The acyclic complexes contain zero and are closed under isomorphisms of complexes, shifts and direct sums. The main result is Neeman's lemma: the mapping cone of a chain map φ : K ⟶ L between acyclic complexes is acyclic. Write ZₙK ↣ Kⁿ and ZₙL ↣ Lⁿ for the cycles; φ restricts to gₙ : ZₙK ⟶ ZₙL. The cycles Wₙ of the cone are the pushouts of ZₙK ↣ Kⁿ along gₙ, which are extensions of Zₙ₊₁K by ZₙL, and gluing the pullback square at n with the pushout square at n + 1 (TauCeti.ExactStructure.conflation_shortComplex'_of_isPullback_of_isPushout) gives the conflations Wₙ ↣ Kⁿ⁺¹ ⊞ Lⁿ ↠ Wₙ₊₁ of the cone.

Main definitions #

TauCeti.ExactStructure.AcyclicData: a factorization of the differentials of a complex through conflations.
TauCeti.ExactStructure.acyclic: the acyclic complexes of an exact structure, characterized by TauCeti.ExactStructure.acyclic_iff.

Main results #

TauCeti.ExactStructure.acyclic_biprod, and instances for isomorphisms, shifts and zero.
TauCeti.ExactStructure.acyclic_mappingCone: Neeman's lemma, the mapping cone of a chain map between acyclic complexes is acyclic.

References #

Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, https://arxiv.org/abs/0811.1480, Definition 10.1 and Lemma 10.3.
Amnon Neeman, The derived category of an exact category, J. Algebra 135 (1990), 388--394, Lemma 1.1.

structure TauCeti.ExactStructure.AcyclicData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (K : CochainComplex C ℤ) :

Type (max u v)

A witness that a cochain complex K is acyclic for an exact structure E: objects Z n and a factorization K.X n ↠ Z (n + 1) ↣ K.X (n + 1) of each differential such that every Z n ↣ K.X n ↠ Z (n + 1) is a conflation.

Z : ℤ → C
The objects of cycles.
i (n : ℤ) : self.Z n ⟶ K.X n
The inflation of the cycles into the complex.
p (n : ℤ) : K.X n ⟶ self.Z (n + 1)
The deflation onto the next cycles.
zero (n : ℤ) : CategoryTheory.CategoryStruct.comp (self.i n) (self.p n) = 0
conflation (n : ℤ) : E.Conflation { X₁ := self.Z n, X₂ := K.X n, X₃ := self.Z (n + 1), f := self.i n, g := self.p n, zero := ⋯ }
fac (n : ℤ) : CategoryTheory.CategoryStruct.comp (self.p n) (self.i (n + 1)) = K.d n (n + 1)

Instances For

def TauCeti.ExactStructure.acyclic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :

CategoryTheory.ObjectProperty (CochainComplex C ℤ)

A cochain complex is acyclic for an exact structure E when each differential factors as a deflation followed by an inflation, K.X n ↠ Z (n + 1) ↣ K.X (n + 1), such that every sequence Z n ↣ K.X n ↠ Z (n + 1) is a conflation.

Instances For

theorem TauCeti.ExactStructure.acyclic_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (K : CochainComplex C ℤ) :

E.acyclic K ↔ Nonempty (E.AcyclicData K)

A complex is acyclic exactly when it has acyclicity data.

theorem TauCeti.ExactStructure.AcyclicData.acyclic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K : CochainComplex C ℤ} (h : E.AcyclicData K) :

Acyclicity data make a complex acyclic.

noncomputable def TauCeti.ExactStructure.AcyclicData.ofIsZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K : CochainComplex C ℤ} (hK : ∀ (n : ℤ), CategoryTheory.Limits.IsZero (K.X n)) :

E.AcyclicData K

Acyclicity data for a complex all of whose terms are zero.

Instances For

def TauCeti.ExactStructure.AcyclicData.ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K L : CochainComplex C ℤ} (h : E.AcyclicData K) (e : K ≅ L) :

E.AcyclicData L

Acyclicity data transported along an isomorphism of complexes.

Instances For

noncomputable def TauCeti.ExactStructure.AcyclicData.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K L : CochainComplex C ℤ} (h : E.AcyclicData K) (h' : E.AcyclicData L) :

E.AcyclicData (K ⊞ L)

Acyclicity data for a direct sum of two complexes.

Instances For

noncomputable def TauCeti.ExactStructure.AcyclicData.shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K : CochainComplex C ℤ} (h : E.AcyclicData K) (a : ℤ) :

E.AcyclicData (K⟦a⟧)

Acyclicity data for a shift of a complex: the cycles are shifted, and the deflations pick up the sign of the shifted differential.

Instances For

noncomputable def TauCeti.ExactStructure.AcyclicData.descZ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K : CochainComplex C ℤ} (h : E.AcyclicData K) {T : C} (n : ℤ) (k : K.X n ⟶ T) (hk : CategoryTheory.CategoryStruct.comp (h.i n) k = 0) :

h.Z (n + 1) ⟶ T

The morphism out of the cycles Zⁿ⁺¹ induced by a morphism out of Kⁿ killing Zⁿ ↣ Kⁿ.

Instances For

@[simp]

theorem TauCeti.ExactStructure.AcyclicData.p_descZ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K : CochainComplex C ℤ} (h : E.AcyclicData K) {T : C} (n : ℤ) (k : K.X n ⟶ T) (hk : CategoryTheory.CategoryStruct.comp (h.i n) k = 0) :

CategoryTheory.CategoryStruct.comp (h.p n) (h.descZ n k hk) = k

@[simp]

theorem TauCeti.ExactStructure.AcyclicData.p_descZ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K : CochainComplex C ℤ} (h : E.AcyclicData K) {T : C} (n : ℤ) (k : K.X n ⟶ T) (hk : CategoryTheory.CategoryStruct.comp (h.i n) k = 0) {Z : C} (h✝ : T ⟶ Z) :

CategoryTheory.CategoryStruct.comp (h.p n) (CategoryTheory.CategoryStruct.comp (h.descZ n k hk) h✝) = CategoryTheory.CategoryStruct.comp k h✝

instance TauCeti.ExactStructure.AcyclicData.instEpiP {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {K : CochainComplex C ℤ} (h : E.AcyclicData K) (n : ℤ) :

CategoryTheory.Epi (h.p n)

instance TauCeti.ExactStructure.instIsClosedUnderIsomorphismsCochainComplexIntAcyclic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :

E.acyclic.IsClosedUnderIsomorphisms

An acyclic complex stays acyclic under isomorphism of complexes.

instance TauCeti.ExactStructure.instContainsZeroCochainComplexIntAcyclic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :

E.acyclic.ContainsZero

The zero complex is acyclic.

instance TauCeti.ExactStructure.instIsStableUnderShiftCochainComplexIntAcyclic {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :

E.acyclic.IsStableUnderShift ℤ

A shift of an acyclic complex is acyclic.

theorem TauCeti.ExactStructure.acyclic_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {K L : CochainComplex C ℤ} (hK : E.acyclic K) (hL : E.acyclic L) :

E.acyclic (K ⊞ L)

A direct sum of acyclic complexes is acyclic.

theorem TauCeti.ExactStructure.acyclic_mappingCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {K L : CochainComplex C ℤ} (φ : K ⟶ L) (hK : E.acyclic K) (hL : E.acyclic L) :

E.acyclic (CochainComplex.mappingCone φ)

Neeman's lemma: the mapping cone of a chain map between acyclic complexes is acyclic (Bühler, Lemma 10.3).

theorem TauCeti.ExactStructure.acyclic_mappingCone_of_isPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {K L : CochainComplex C ℤ} (φ : K ⟶ L) (B : ℤ → C) (j : (m : ℤ) → B m ⟶ L.X m) (q : (m : ℤ) → B m ⟶ K.X (m + 1)) (u : (m : ℤ) → L.X m ⟶ B (m + 1)) (v : (m : ℤ) → K.X m ⟶ B m) (hj : ∀ (m : ℤ), E.IsInflation (j m)) (sq : ∀ (m : ℤ), CategoryTheory.IsPushout (j m) (q m) (u m) (v (m + 1))) (hd : ∀ (m : ℤ), CategoryTheory.CategoryStruct.comp (u m) (j (m + 1)) = L.d m (m + 1)) (hφ : ∀ (m : ℤ), CategoryTheory.CategoryStruct.comp (v m) (j m) = φ.f m) (hq : ∀ (m : ℤ), CategoryTheory.CategoryStruct.comp (v m) (q m) = K.d m (m + 1)) (huq : ∀ (m : ℤ), CategoryTheory.CategoryStruct.comp (u m) (q (m + 1)) = 0) :

E.acyclic (CochainComplex.mappingCone φ)

The mapping cone of a map built from pushouts of inflations is acyclic. Let φ : K ⟶ L come with objects Bᵐ, inflations j : Bᵐ ↣ Lᵐ and pushout squares

Bᵐ ──j──▶ Lᵐ
│q        │u
▼         ▼
Kᵐ⁺¹ ─v─▶ Bᵐ⁺¹

such that the differential of L is u ≫ j, φ is v ≫ j, the differential of K is v ≫ q and u ≫ q = 0. Then the cone of φ is acyclic, with cycles Bᵐ: the pushout conflations Bᵐ ↣ Lᵐ ⊞ Kᵐ⁺¹ ↠ Bᵐ⁺¹ are its degreewise conflations. This is the dual of the last step of Bühler's proof of Theorem 12.7, where such data come from a recursive construction.

theorem TauCeti.ExactStructure.acyclic_mappingCone_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁} {φ₂ : K₂ ⟶ L₂} (a : K₁ ≅ K₂) (b : L₁ ≅ L₂) (comm : CategoryTheory.CategoryStruct.comp φ₁ b.hom = CategoryTheory.CategoryStruct.comp a.hom φ₂) (h : E.acyclic (CochainComplex.mappingCone φ₂)) :

E.acyclic (CochainComplex.mappingCone φ₁)

Acyclicity of mapping cones is invariant under isomorphisms of arrows, through Mathlib's HomologicalComplex.homotopyCofiber.mapArrowIso.