Finite resolutions in an exact category

Let E be an exact structure on an additive category C and let P be a property of objects of C. A finite P-resolution of an object X is a finite chain of E-conflations

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

whose resolving terms Q₀, …, Qₙ₋₁ and whose last syzygy Kₙ all satisfy P. Equivalently, it is a bounded exact augmented complex 0 → Kₙ → Qₙ₋₁ → ⋯ → Q₀ → X → 0 built from conflations. TauCeti.ExactStructure.FiniteResolution records exactly that chain, as data, by recursion on its length.

This file is the reusable resolution vocabulary in which the resolution theorem is stated. It develops the operations a later Euler-class argument needs -- length, syzygies and truncation, transport along an isomorphism, zero padding, and direct sums -- for an arbitrary object property, before any projectivity hypothesis is available.

Main definitions

• TauCeti.ExactStructure.FiniteResolution E P X: a finite P-resolution of X, as data.
• TauCeti.ExactStructure.FiniteResolution.length: the number of conflations in the chain.
• TauCeti.ExactStructure.FiniteResolution.foldAlternating: the alternating fold of a function on the objects satisfying P along a resolution, the common shape of the Euler-type invariants of a resolution.
• TauCeti.ExactStructure.FiniteResolution.syzygy and TauCeti.ExactStructure.FiniteResolution.truncate: the n-th syzygy of a resolution, and the resolution of it obtained by discarding the first n conflations.
• TauCeti.ExactStructure.FiniteResolution.ofIso: transport along an isomorphism of the resolved object.
• TauCeti.ExactStructure.FiniteResolution.zeroPad and TauCeti.ExactStructure.FiniteResolution.pad: lengthen a resolution by adjoining trivial conflations 0 ↪ Kₙ ↠ Kₙ at its far end.
• TauCeti.ExactStructure.FiniteResolution.biprod: the componentwise direct sum of two resolutions.
• TauCeti.ExactStructure.FiniteResolution.map: the image of a resolution under a conflation-exact functor carrying P into P', a finite P'-resolution of the image.
• TauCeti.ExactStructure.admitsFiniteResolution: the object property of admitting some finite P-resolution, the object-property presentation of the above data.

Main results

• TauCeti.ExactStructure.FiniteResolution.syzygy_truncate and TauCeti.ExactStructure.FiniteResolution.syzygy_eq_syzygy_length_of_length_le: truncating shifts the syzygies, and they stabilise at the last one past the length.
• TauCeti.ExactStructure.FiniteResolution.prop_syzygy_length: the last syzygy of a resolution satisfies P; more generally TauCeti.ExactStructure.FiniteResolution.prop_syzygy covers every index beyond the length.
• TauCeti.ExactStructure.FiniteResolution.length_biprod: a direct sum of resolutions has the larger of the two lengths, the shorter chain being padded against the longer one.
• TauCeti.ExactStructure.exists_conflation_of_exists_finiteResolution_length_le_succ: a resolution of length at most n + 1 yields a first conflation K ↪ Q ↠ X together with a resolution of K of length at most n; this is how an induction on the length peels off one step.
• TauCeti.ExactStructure.exists_conflation_prop_X₂_admitsFiniteResolution_X₁: an object admitting a finite resolution has a conflation whose middle term satisfies P and whose kernel still admits a finite resolution.
• TauCeti.ExactStructure.exists_finiteResolution_X₁_length_le_of_prop_X₃: kernel closure for P preserves the resolution-length bound along a deflation onto an object satisfying P.
• TauCeti.ExactStructure.admitsFiniteResolution_induction: the object property of admitting a finite P-resolution is the smallest one containing P and closed under passing from the subobject of a conflation with resolving middle term to its quotient.
• TauCeti.ExactStructure.admitsFiniteResolution_le_inverseImage: a conflation-exact functor carrying P into P' carries objects of finite P-dimension to objects of finite P'-dimension.

Implementation notes

The recursion is on the deep end of the chain: TauCeti.ExactStructure.FiniteResolution.base is a resolution of length zero of an object already satisfying P, and TauCeti.ExactStructure.FiniteResolution.step prepends one conflation K ↪ Q ↠ X to a resolution of K. This is the presentation in which zero padding is the operation that rewrites the base leaf, and it is the one the roadmap's AdmitsFiniteResolutionAlong uses. The conflations are stored by their two maps rather than as a CategoryTheory.ShortComplex, so that the resolved object is a genuine index of the family and FiniteResolution E P X never needs an equality of objects to be matched on.

Every operation is sealed behind its @[simp] equations, with two exceptions. TauCeti.ExactStructure.FiniteResolution.syzygy is the type index of TauCeti.ExactStructure.FiniteResolution.truncate, so the statements of the truncate equations only typecheck when its body is exposed. TauCeti.ExactStructure.FiniteResolution.map is exposed so that the terms of an image resolution reduce on constructors: the identification TauCeti.ExactStructure.FiniteResolution.termMapIso of those terms with the images of the original terms is defined by recursion along the resolution, and each of its cases only typechecks when the image of a constructor unfolds to a constructor.

The closure hypotheses on P are Mathlib's object-property type classes, and are assumed only where they are used: repleteness for ofIso, CategoryTheory.ObjectProperty.ContainsZero for padding, and closure under binary products for direct sums, the last of these reaching biproducts through CategoryTheory.ObjectProperty.prop_biprod_of_isClosedUnderBinaryProducts. The resolving-subcategory package, which bundles these with extension closure and closure under kernels of deflations, is downstream.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 7, where finite resolutions by a resolving subcategory and the resolution theorem are developed.
• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, Sections 11--12, for resolutions in a Quillen exact category.

inductive TauCeti.ExactStructure.FiniteResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) : C → Type (max u v)

A finite P-resolution of an object X of an exact category: a finite chain of conflations

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

whose resolving terms Qᵢ satisfy P, ending at a syzygy Kₙ which satisfies P as well. The recursion is on the deep end: base is the empty chain, available when X already satisfies P, and step prepends one conflation to a resolution of its subobject.

• base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (hX : P X) : E.FiniteResolution P X

  An object satisfying P is its own resolution, of length zero.

• step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : E.FiniteResolution P X

  Prepend a conflation K ↪ Q ↠ X with resolving term Q to a resolution of K.

def TauCeti.ExactStructure.FiniteResolution.length {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} : E.FiniteResolution P X → ℕ

The length of a resolution: the number of conflations in its chain.

Equations

• (TauCeti.ExactStructure.FiniteResolution.base hX).length = 0
• (TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r).length = r.length + 1

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.length_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (hX : P X) : (base hX).length = 0

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.length_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : (step hQ i p zero hp r).length = r.length + 1

def TauCeti.ExactStructure.FiniteResolution.foldAlternating {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {A : Type u_1} [AddGroup A] (f : (Z : C) → P Z → A) {X : C} : E.FiniteResolution P X → A

The alternating fold of f along a resolution: f Q₀ - f Q₁ + ⋯ + (-1)ⁿ f Kₙ, where f assigns an element of an additive group to every object satisfying P.

This is the common shape of the Euler-type invariants of a finite resolution; TauCeti.ExactStructure.FiniteResolution.homEuler is the alternating Hom dimension obtained from it.

Equations

• TauCeti.ExactStructure.FiniteResolution.foldAlternating f (TauCeti.ExactStructure.FiniteResolution.base hX) = f x✝ hX
• TauCeti.ExactStructure.FiniteResolution.foldAlternating f (TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r) = f Q hQ - TauCeti.ExactStructure.FiniteResolution.foldAlternating f r

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.foldAlternating_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {A : Type u_1} [AddGroup A] (f : (Z : C) → P Z → A) {X : C} (hX : P X) : foldAlternating f (base hX) = f X hX

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.foldAlternating_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {A : Type u_1} [AddGroup A] (f : (Z : C) → P Z → A) {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : foldAlternating f (step hQ i p zero hp r) = f Q hQ - foldAlternating f r

def TauCeti.ExactStructure.FiniteResolution.syzygy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} : E.FiniteResolution P X → ℕ → C

The n-th syzygy of a resolution of X: the object resolved by what is left after discarding the first n conflations. It is X itself for n = 0, and it stabilises at the last syzygy once n reaches the length.

Equations

• (TauCeti.ExactStructure.FiniteResolution.base hX).syzygy x✝ = x✝¹
• (TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r).syzygy 0 = x✝
• (TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r).syzygy n.succ = r.syzygy n

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (hX : P X) (n : ℕ) : (base hX).syzygy n = X

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) : r.syzygy 0 = X

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_step_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) (n : ℕ) : (step hQ i p zero hp r).syzygy (n + 1) = r.syzygy n

def TauCeti.ExactStructure.FiniteResolution.truncate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) (n : ℕ) : E.FiniteResolution P (r.syzygy n)

The truncation of a resolution below degree n: the chain that remains after discarding the first n conflations, a resolution of the n-th syzygy.

Equations

• (TauCeti.ExactStructure.FiniteResolution.base hX).truncate x✝ = TauCeti.ExactStructure.FiniteResolution.base hX
• (TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r).truncate 0 = TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r
• (TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r).truncate n.succ = r.truncate n

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.truncate_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (hX : P X) (n : ℕ) : (base hX).truncate n = base hX

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.truncate_step_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : (step hQ i p zero hp r).truncate 0 = step hQ i p zero hp r

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.truncate_step_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) (n : ℕ) : (step hQ i p zero hp r).truncate (n + 1) = r.truncate n

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_truncate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) (n m : ℕ) : (r.truncate n).syzygy m = r.syzygy (n + m)

The syzygies of a truncation are the syzygies of the original chain, shifted.

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.length_truncate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) (n : ℕ) : (r.truncate n).length = r.length - n

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_eq_syzygy_length_of_length_le {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) {n : ℕ} (hn : r.length ≤ n) : r.syzygy n = r.syzygy r.length

Once the index reaches the length, the syzygies stabilise at the last one.

theorem TauCeti.ExactStructure.FiniteResolution.prop_syzygy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) {n : ℕ} (hn : r.length ≤ n) : P (r.syzygy n)

Every syzygy of index at least the length satisfies P: the chain has run out.

theorem TauCeti.ExactStructure.FiniteResolution.prop_syzygy_length {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) : P (r.syzygy r.length)

The last syzygy of a resolution satisfies P.

def TauCeti.ExactStructure.FiniteResolution.ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] {X Y : C} : (X ≅ Y) → E.FiniteResolution P X → E.FiniteResolution P Y

Transport a resolution along an isomorphism of the resolved object.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.ExactStructure.FiniteResolution.ofIso x✝ (TauCeti.ExactStructure.FiniteResolution.base hX) = TauCeti.ExactStructure.FiniteResolution.base ⋯

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.ofIso_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) (hX : P X) : ofIso e (base hX) = base ⋯

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.ofIso_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] {K Q X Y : C} (e : X ≅ Y) (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : ofIso e (step hQ i p zero hp r) = step hQ i (CategoryTheory.CategoryStruct.comp p e.hom) ⋯ ⋯ r

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.length_ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) (r : E.FiniteResolution P X) : (ofIso e r).length = r.length

noncomputable def TauCeti.ExactStructure.FiniteResolution.zeroPad {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} : E.FiniteResolution P X → E.FiniteResolution P X

Lengthen a resolution by one, adjoining the trivial conflation 0 ↪ Kₙ ↠ Kₙ at its last syzygy.

Equations

• One or more equations did not get rendered due to their size.
• (TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r).zeroPad = TauCeti.ExactStructure.FiniteResolution.step hQ i p zero hp r.zeroPad

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.zeroPad_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (hX : P X) : (base hX).zeroPad = step hX 0 (CategoryTheory.CategoryStruct.id X) ⋯ ⋯ (base ⋯)

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.zeroPad_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : (step hQ i p zero hp r).zeroPad = step hQ i p zero hp r.zeroPad

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.length_zeroPad {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) : r.zeroPad.length = r.length + 1

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_zeroPad_of_le_length {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) {n : ℕ} (hn : n ≤ r.length) : r.zeroPad.syzygy n = r.syzygy n

Zero padding does not change the syzygies in the original resolution.

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_zeroPad_of_length_lt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) {n : ℕ} (hn : r.length < n) : r.zeroPad.syzygy n = 0

After the original resolution ends, every syzygy of its zero padding is the zero object.

noncomputable def TauCeti.ExactStructure.FiniteResolution.pad {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) : ℕ → E.FiniteResolution P X

Lengthen a resolution by n, adjoining n trivial conflations at its last syzygy.

Equations

• r.pad 0 = r
• r.pad n.succ = (r.pad n).zeroPad

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.pad_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) : r.pad 0 = r

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.pad_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) (n : ℕ) : r.pad (n + 1) = (r.pad n).zeroPad

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.length_pad {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) (n : ℕ) : (r.pad n).length = r.length + n

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_pad_of_le_length {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) (m : ℕ) {n : ℕ} (hn : n ≤ r.length) : (r.pad m).syzygy n = r.syzygy n

Iterated padding does not change the syzygies in the original resolution.

theorem TauCeti.ExactStructure.FiniteResolution.syzygy_pad_succ_of_length_lt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} (r : E.FiniteResolution P X) (m : ℕ) {n : ℕ} (hn : r.length < n) : (r.pad (m + 1)).syzygy n = 0

After the original resolution ends, every syzygy of a positive padding is the zero object.

noncomputable def TauCeti.ExactStructure.FiniteResolution.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] {X Y : C} : E.FiniteResolution P X → E.FiniteResolution P Y → E.FiniteResolution P (X ⊞ Y)

The componentwise direct sum of two finite P-resolutions. Where one chain has run out, it is padded against the other by the trivial conflation on its last syzygy.

Equations

• One or more equations did not get rendered due to their size.
• (TauCeti.ExactStructure.FiniteResolution.base hX).biprod (TauCeti.ExactStructure.FiniteResolution.base hY) = TauCeti.ExactStructure.FiniteResolution.base ⋯

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.biprod_base_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] {X Y : C} (hX : P X) (hY : P Y) : (base hX).biprod (base hY) = base ⋯

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.biprod_base_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] {X K Q Y : C} (hX : P X) (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ Y) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := Y, f := i, g := p, zero := zero }) (s : E.FiniteResolution P K) : (base hX).biprod (step hQ i p zero hp s) = step ⋯ (CategoryTheory.Limits.biprod.map 0 i) (CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.id X) p) ⋯ ⋯ (ofIso (CategoryTheory.Limits.isoZeroBiprod ⋯) s)

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.biprod_step_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] {K Q X Y : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) (hY : P Y) : (step hQ i p zero hp r).biprod (base hY) = step ⋯ (CategoryTheory.Limits.biprod.map i 0) (CategoryTheory.Limits.biprod.map p (CategoryTheory.CategoryStruct.id Y)) ⋯ ⋯ (ofIso (CategoryTheory.Limits.isoBiprodZero ⋯) r)

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.biprod_step_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] {K Q X K' Q' Y : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) (hQ' : P Q') (i' : K' ⟶ Q') (p' : Q' ⟶ Y) (zero' : CategoryTheory.CategoryStruct.comp i' p' = 0) (hp' : E.Conflation { X₁ := K', X₂ := Q', X₃ := Y, f := i', g := p', zero := zero' }) (s : E.FiniteResolution P K') : (step hQ i p zero hp r).biprod (step hQ' i' p' zero' hp' s) = step ⋯ (CategoryTheory.Limits.biprod.map i i') (CategoryTheory.Limits.biprod.map p p') ⋯ ⋯ (r.biprod s)

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.length_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] {X Y : C} (r : E.FiniteResolution P X) (s : E.FiniteResolution P Y) : (r.biprod s).length = max r.length s.length

def TauCeti.ExactStructure.FiniteResolution.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} : E.FiniteResolution P X → E'.FiniteResolution P' (F.obj X)

The image of a finite P-resolution under a conflation-exact functor F carrying P into P': applying F to every conflation of the chain gives a finite P'-resolution of F X.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.ExactStructure.FiniteResolution.map hF hPP' (TauCeti.ExactStructure.FiniteResolution.base hX) = TauCeti.ExactStructure.FiniteResolution.base ⋯

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.map_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (hX : P X) : map hF hPP' (base hX) = base ⋯

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.map_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) : map hF hPP' (step hQ i p zero hp r) = step ⋯ (F.map i) (F.map p) ⋯ ⋯ (map hF hPP' r)

@[simp]

theorem TauCeti.ExactStructure.FiniteResolution.length_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (r : E.FiniteResolution P X) : (map hF hPP' r).length = r.length

theorem TauCeti.ExactStructure.exists_conflation_of_exists_finiteResolution_length_le_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] {X : C} {n : ℕ} (h : ∃ (r : E.FiniteResolution P X), r.length ≤ n + 1) : ∃ (K : C) (Q : C) (m : K ⟶ Q) (a : Q ⟶ X) (hm : CategoryTheory.CategoryStruct.comp m a = 0), P Q ∧ E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := m, g := a, zero := hm } ∧ ∃ (s : E.FiniteResolution P K), s.length ≤ n

The first step of a finite P-resolution of length at most n + 1: a conflation K ↪ Q ↠ X with P Q, whose subobject K still admits a finite P-resolution of length at most n. A resolution of length zero contributes the trivial conflation 0 ↪ X ↠ X.

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

The object property of admitting some finite P-resolution: the object-property presentation of TauCeti.ExactStructure.FiniteResolution.

Equations

• E.admitsFiniteResolution P X = Nonempty (E.FiniteResolution P X)

@[simp]

theorem TauCeti.ExactStructure.admitsFiniteResolution_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) {X : C} : E.admitsFiniteResolution P X ↔ Nonempty (E.FiniteResolution P X)

theorem TauCeti.ExactStructure.exists_conflation_prop_X₂_admitsFiniteResolution_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] [P.ContainsZero] (X : C) (hX : E.admitsFiniteResolution P X) : ∃ (K : C) (Q : C) (i : K ⟶ Q) (p : Q ⟶ X) (hip : CategoryTheory.CategoryStruct.comp i p = 0), P Q ∧ E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := hip } ∧ E.admitsFiniteResolution P K

An object admitting a finite P-resolution is the quotient of a conflation K ↪ Q ↠ X whose middle term satisfies P and whose kernel again admits a finite P-resolution.

theorem TauCeti.ExactStructure.exists_finiteResolution_X₁_length_le_of_prop_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.IsClosedUnderIsomorphisms] {n : ℕ} (hkernel : ∀ {T : CategoryTheory.ShortComplex C}, E.Conflation T → P T.X₂ → P T.X₃ → P T.X₁) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (h₃ : P S.X₃) (h₂ : ∃ (r : E.FiniteResolution P S.X₂), r.length ≤ n) : ∃ (r : E.FiniteResolution P S.X₁), r.length ≤ n

For a replete property closed under kernels of deflations between its objects, the kernel of a deflation from an object of P-dimension at most n onto an object of P has P-dimension at most n.

theorem TauCeti.ExactStructure.le_admitsFiniteResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) : P ≤ E.admitsFiniteResolution P

An object satisfying P admits a finite P-resolution, namely the empty chain.

theorem TauCeti.ExactStructure.admitsFiniteResolution_of_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) {K Q X : C} (hQ : P Q) {i : K ⟶ Q} {p : Q ⟶ X} {zero : CategoryTheory.CategoryStruct.comp i p = 0} (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (hK : E.admitsFiniteResolution P K) : E.admitsFiniteResolution P X

Admitting a finite P-resolution passes from the subobject of a conflation with resolving middle term to its quotient.

theorem TauCeti.ExactStructure.admitsFiniteResolution_induction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) {motive : CategoryTheory.ObjectProperty C} (hP : P ≤ motive) (hstep : ∀ {K Q X : C}, P Q → ∀ {i : K ⟶ Q} {p : Q ⟶ X} {zero : CategoryTheory.CategoryStruct.comp i p = 0}, E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero } → motive K → motive X) {X : C} (hX : E.admitsFiniteResolution P X) : motive X

The object-property presentation. Admitting a finite P-resolution is the smallest object property containing P and closed under passing from the subobject of a conflation with resolving middle term to its quotient.

instance TauCeti.ExactStructure.instIsClosedUnderIsomorphismsAdmitsFiniteResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] : (E.admitsFiniteResolution P).IsClosedUnderIsomorphisms

instance TauCeti.ExactStructure.instContainsZeroAdmitsFiniteResolutionOfIsClosedUnderIsomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] [P.ContainsZero] : (E.admitsFiniteResolution P).ContainsZero

theorem TauCeti.ExactStructure.admitsFiniteResolution_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] {X Y : C} (hX : E.admitsFiniteResolution P X) (hY : E.admitsFiniteResolution P Y) : E.admitsFiniteResolution P (X ⊞ Y)

Admitting a finite P-resolution is closed under binary direct sums.

instance TauCeti.ExactStructure.instIsClosedUnderBinaryProductsAdmitsFiniteResolutionOfIsClosedUnderIsomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] [P.IsClosedUnderBinaryProducts] : (E.admitsFiniteResolution P).IsClosedUnderBinaryProducts

theorem TauCeti.ExactStructure.admitsFiniteResolution_le_inverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (P : CategoryTheory.ObjectProperty C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) : E.admitsFiniteResolution P ≤ (E'.admitsFiniteResolution P').inverseImage F

A conflation-exact functor carrying P into P' carries objects of finite P-dimension to objects of finite P'-dimension, by TauCeti.ExactStructure.FiniteResolution.map.