Complete resolutions

A complete resolution in an exact category is a bi-infinite sequence of conflations Zⁿ ↪ Xⁿ ↠ Zⁿ⁺¹, indexed by n : ℤ, whose middle terms are projective-injective. Splicing the conflations gives a cochain complex with differential Xⁿ ↠ Zⁿ⁺¹ ↪ Xⁿ⁺¹; it is acyclic in the sense of the exact structure, and its object of cycles in degree zero is Z⁰.

In a Frobenius exact category every object has a complete resolution. Its conflations are injective presentations in nonnegative degrees and projective presentations in negative degrees. The interface retains the conflations, so an exact functor can transport the sequence before its maps are spliced. Uniqueness up to homotopy is the comparison theorem in TauCeti.CategoryTheory.Exact.Resolution.Complete.Comparison.

Main definitions

• TauCeti.ExactStructure.CompleteResolution: a complete resolution, as the data of its conflations.
• TauCeti.ExactStructure.CompleteResolution.complex: the spliced cochain complex, acyclic by TauCeti.ExactStructure.CompleteResolution.acyclicData.
• TauCeti.ExactStructure.CompleteResolution.cyclesMap: the morphism of the objects of cycles in degree zero induced by a map of the spliced complexes.
• TauCeti.ExactStructure.IsFrobenius.completeResolution: a complete resolution of an object of a Frobenius exact category, with TauCeti.ExactStructure.IsFrobenius.completeResolutionIso.

References

• Ragnar-Olaf Buchweitz, Maximal Cohen–Macaulay Modules and Tate Cohomology, Section 4.
• Theo Bühler, Exact categories, Sections 11–13.

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

A complete resolution in an exact category: a bi-infinite sequence of conflations Zⁿ ↪ Xⁿ ↠ Zⁿ⁺¹ whose middle terms are both relatively projective and relatively injective. The spliced complex is TauCeti.ExactStructure.CompleteResolution.complex; it is a complete resolution of the object of cycles Z 0.

• Z : ℤ → C

  The object of cycles Zⁿ in degree n.

• X : ℤ → C

  The term Xⁿ of the complex in degree n.

• ι (n : ℤ) : self.Z n ⟶ self.X n

  The inflation Zⁿ ↪ Xⁿ.

• π (n : ℤ) : self.X n ⟶ self.Z (n + 1)

  The deflation Xⁿ ↠ Zⁿ⁺¹.

• ι_π (n : ℤ) : CategoryTheory.CategoryStruct.comp (self.ι n) (self.π n) = 0
• conflation (n : ℤ) : E.Conflation { X₁ := self.Z n, X₂ := self.X n, X₃ := self.Z (n + 1), f := self.ι n, g := self.π n, zero := ⋯ }

  The sequences Zⁿ ↪ Xⁿ ↠ Zⁿ⁺¹ are conflations.

• projectiveInjective (n : ℤ) : E.projectiveInjective (self.X n)

  The terms are projective-injective.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.ι_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (self : E.CompleteResolution) (n : ℤ) {Z : C} (h : self.Z (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.ι n) (CategoryTheory.CategoryStruct.comp (self.π n) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem TauCeti.ExactStructure.CompleteResolution.isProjective_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : E.isProjective (r.X n)

theorem TauCeti.ExactStructure.CompleteResolution.isInjective_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : E.isInjective (r.X n)

theorem TauCeti.ExactStructure.CompleteResolution.isInflation_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : E.IsInflation (r.ι n)

theorem TauCeti.ExactStructure.CompleteResolution.isDeflation_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : E.IsDeflation (r.π n)

instance TauCeti.ExactStructure.CompleteResolution.instMonoι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : CategoryTheory.Mono (r.ι n)

instance TauCeti.ExactStructure.CompleteResolution.instEpiπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : CategoryTheory.Epi (r.π n)

noncomputable def TauCeti.ExactStructure.CompleteResolution.d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : r.X n ⟶ r.X (n + 1)

The differential Xⁿ ↠ Zⁿ⁺¹ ↪ Xⁿ⁺¹ of the spliced complex.

theorem TauCeti.ExactStructure.CompleteResolution.d_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : r.d n = CategoryTheory.CategoryStruct.comp (r.π n) (r.ι (n + 1))

theorem TauCeti.ExactStructure.CompleteResolution.d_negSucc_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) : r.d (Int.negSucc 0) = CategoryTheory.CategoryStruct.comp (r.π (Int.negSucc 0)) (r.ι 0)

The differential out of degree -1, whose target index Int.negSucc 0 + 1 reduces to 0.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.ι_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : CategoryTheory.CategoryStruct.comp (r.ι n) (r.d n) = 0

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.ι_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) {Z : C} (h : r.X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (r.ι n) (CategoryTheory.CategoryStruct.comp (r.d n) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.d_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : CategoryTheory.CategoryStruct.comp (r.d n) (r.π (n + 1)) = 0

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.d_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) {Z : C} (h : r.Z (n + 1 + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (r.d n) (CategoryTheory.CategoryStruct.comp (r.π (n + 1)) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.d_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : CategoryTheory.CategoryStruct.comp (r.d n) (r.d (n + 1)) = 0

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.d_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) {Z : C} (h : r.X (n + 1 + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (r.d n) (CategoryTheory.CategoryStruct.comp (r.d (n + 1)) h) = CategoryTheory.CategoryStruct.comp 0 h

@[reducible, inline]

abbrev TauCeti.ExactStructure.CompleteResolution.shortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : CategoryTheory.ShortComplex C

The n-th conflation Zⁿ ↪ Xⁿ ↠ Zⁿ⁺¹ of a complete resolution, as a short complex.

@[reducible, inline]

noncomputable abbrev TauCeti.ExactStructure.CompleteResolution.complex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) : CochainComplex C ℤ

The cochain complex spliced from the conflations of a complete resolution, through CochainComplex.splice: consecutive conflations share their end terms Zⁿ⁺¹, so the connecting isomorphisms are identities.

theorem TauCeti.ExactStructure.CompleteResolution.complex_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : r.complex.d n (n + 1) = r.d n

The differential of the complex in consecutive degrees, in the form rw can use. It is not a simp lemma: simp already reduces its left-hand side through CochainComplex.of_d.

theorem TauCeti.ExactStructure.CompleteResolution.complex_d_negSucc_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) : r.complex.d (Int.negSucc 0) 0 = r.d (Int.negSucc 0)

The differential of the complex out of degree -1, whose target index is not syntactically of the form n + 1.

def TauCeti.ExactStructure.CompleteResolution.acyclicData {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) : E.AcyclicData r.complex

The spliced complex of a complete resolution is acyclic, with objects of cycles Zⁿ.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.acyclicData_Z {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (a✝ : ℤ) : r.acyclicData.Z a✝ = r.Z a✝

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.acyclicData_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : r.acyclicData.p n = r.π n

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.acyclicData_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : r.acyclicData.i n = r.ι n

theorem TauCeti.ExactStructure.CompleteResolution.f_comp_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) {r' : E.CompleteResolution} (φ : r.complex ⟶ r'.complex) (n : ℤ) : CategoryTheory.CategoryStruct.comp (φ.f n) (r'.d n) = CategoryTheory.CategoryStruct.comp (r.d n) (φ.f (n + 1))

A map of the spliced complexes commutes with the differentials of the resolutions.

theorem TauCeti.ExactStructure.CompleteResolution.f_comp_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) {r' : E.CompleteResolution} (φ : r.complex ⟶ r'.complex) (n : ℤ) {Z : C} (h : r'.X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (φ.f n) (CategoryTheory.CategoryStruct.comp (r'.d n) h) = CategoryTheory.CategoryStruct.comp (r.d n) (CategoryTheory.CategoryStruct.comp (φ.f (n + 1)) h)

A map of the spliced complexes commutes with the differentials of the resolutions.

@[reducible, inline]

abbrev TauCeti.ExactStructure.CompleteResolution.injectivePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : E.InjectivePresentation (r.Z n)

The n-th conflation as an injective presentation of the cycles Zⁿ.

@[reducible, inline]

abbrev TauCeti.ExactStructure.CompleteResolution.projectivePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) (n : ℤ) : E.ProjectivePresentation (r.Z (n + 1))

The n-th conflation as a projective presentation of the cycles Zⁿ⁺¹.

noncomputable def TauCeti.ExactStructure.CompleteResolution.liftZ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) {A : C} (n : ℤ) (k : A ⟶ r.X n) (hk : CategoryTheory.CategoryStruct.comp k (r.π n) = 0) : A ⟶ r.Z n

The morphism into the cycles Zⁿ induced by a morphism into Xⁿ killed by Xⁿ ↠ Zⁿ⁺¹.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.liftZ_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) {A : C} (n : ℤ) (k : A ⟶ r.X n) (hk : CategoryTheory.CategoryStruct.comp k (r.π n) = 0) : CategoryTheory.CategoryStruct.comp (r.liftZ n k hk) (r.ι n) = k

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.liftZ_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) {A : C} (n : ℤ) (k : A ⟶ r.X n) (hk : CategoryTheory.CategoryStruct.comp k (r.π n) = 0) {Z : C} (h : r.X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (r.liftZ n k hk) (CategoryTheory.CategoryStruct.comp (r.ι n) h) = CategoryTheory.CategoryStruct.comp k h

noncomputable def TauCeti.ExactStructure.CompleteResolution.descZ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) {A : C} (n : ℤ) (k : r.X n ⟶ A) (hk : CategoryTheory.CategoryStruct.comp (r.ι n) k = 0) : r.Z (n + 1) ⟶ A

The morphism out of the cycles Zⁿ⁺¹ induced by a morphism out of Xⁿ killing Zⁿ ↪ Xⁿ.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.π_descZ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) {A : C} (n : ℤ) (k : r.X n ⟶ A) (hk : CategoryTheory.CategoryStruct.comp (r.ι n) k = 0) : CategoryTheory.CategoryStruct.comp (r.π n) (r.descZ n k hk) = k

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.π_descZ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (r : E.CompleteResolution) {A : C} (n : ℤ) (k : r.X n ⟶ A) (hk : CategoryTheory.CategoryStruct.comp (r.ι n) k = 0) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (r.π n) (CategoryTheory.CategoryStruct.comp (r.descZ n k hk) h) = CategoryTheory.CategoryStruct.comp k h

noncomputable def TauCeti.ExactStructure.CompleteResolution.cyclesMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r r' : E.CompleteResolution} (φ : r.complex ⟶ r'.complex) : r.Z 0 ⟶ r'.Z 0

The morphism of the objects of cycles in degree zero induced by a map of the spliced complexes: the restriction of the degree-zero component to Z⁰ ↪ X⁰, which lands in Z'⁰.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.cyclesMap_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r r' : E.CompleteResolution} (φ : r.complex ⟶ r'.complex) : CategoryTheory.CategoryStruct.comp (cyclesMap φ) (r'.ι 0) = CategoryTheory.CategoryStruct.comp (r.ι 0) (φ.f 0)

The map of complexes extends the induced morphism of the objects of cycles.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.cyclesMap_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r r' : E.CompleteResolution} (φ : r.complex ⟶ r'.complex) {Z : C} (h : r'.X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (cyclesMap φ) (CategoryTheory.CategoryStruct.comp (r'.ι 0) h) = CategoryTheory.CategoryStruct.comp (r.ι 0) (CategoryTheory.CategoryStruct.comp (φ.f 0) h)

The map of complexes extends the induced morphism of the objects of cycles.

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.cyclesMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r : E.CompleteResolution} : cyclesMap (CategoryTheory.CategoryStruct.id r.complex) = CategoryTheory.CategoryStruct.id (r.Z 0)

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.cyclesMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r r' r'' : E.CompleteResolution} (φ : r.complex ⟶ r'.complex) (ψ : r'.complex ⟶ r''.complex) : cyclesMap (CategoryTheory.CategoryStruct.comp φ ψ) = CategoryTheory.CategoryStruct.comp (cyclesMap φ) (cyclesMap ψ)

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.cyclesMap_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r r' : E.CompleteResolution} : cyclesMap 0 = 0

@[simp]

theorem TauCeti.ExactStructure.CompleteResolution.cyclesMap_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {r r' : E.CompleteResolution} (φ ψ : r.complex ⟶ r'.complex) : cyclesMap (φ + ψ) = cyclesMap φ + cyclesMap ψ

noncomputable def TauCeti.ExactStructure.IsFrobenius.completeResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) (X : C) : E.CompleteResolution

A complete resolution of an object of a Frobenius exact category, spliced from injective presentations in nonnegative degrees and projective presentations in negative degrees. Its object of cycles in degree zero is the given object, by TauCeti.ExactStructure.IsFrobenius.completeResolutionIso.

noncomputable def TauCeti.ExactStructure.IsFrobenius.completeResolutionIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} (hE : E.IsFrobenius) (X : C) : (hE.completeResolution X).Z 0 ≅ X

The object of cycles in degree zero of TauCeti.ExactStructure.IsFrobenius.completeResolution is the given object.