Generation time: the ℕ∞-valued extension-step count

For object properties P Q in a pretriangulated category, P.generationTime Q : ℕ∞ is the least n such that every object of Q is reachable from P by shifts, binary products, retracts and at most n extensions -- that is, the least n with Q ≤ P.triangEnvelopeIter n -- and ⊤ when there is no such n. It is the numerical layer on top of Mathlib's ObjectProperty.triangEnvelopeIter, and it introduces no new closure operation.

The order API

• generationTime_le_coe_iff: P.generationTime Q ≤ n ↔ Q ≤ P.triangEnvelopeIter n. The reverse direction is sInf_le; the forward direction uses that ℕ∞ is well-ordered, so a nonempty defining set attains its infimum, and then monotone'_triangEnvelopeIter.
• Antitone in P (generationTime_antitone_left), monotone in Q (generationTime_mono_right).
• The degenerate values: = 0 exactly when Q is already reachable with no extension (generationTime_eq_zero_iff, unfolded in generationTime_eq_zero_iff'), P.generationTime P = 0 unconditionally (generationTime_self), and = ⊤ exactly when no finite number of extensions suffices (generationTime_eq_top_iff).
• The bridges to Mathlib's predicates: P is a strong triangulated generator iff P.generationTime ⊤ ≠ ⊤ (isStrongTriangulatedGenerator_iff_generationTime_ne_top), and then it is a classical one (isClassicalTriangulatedGenerator_of_generationTime_ne_top).

No side conditions

Nothing here carries a P.ContainsZero or P.Nonempty hypothesis. Mathlib's monotone'_triangEnvelopeIter has none at the pin -- it discharges the degenerate case internally -- and carrying one would weaken every lemma downstream, including the Rouquier dimension characterisations, which instantiate at ObjectProperty.singleton G, a property that is not ContainsZero.

Generation time is not subadditive

The bound P.generationTime R ≤ P.generationTime Q + Q.generationTime R is false, and the shape of triangEnvelopeIter_add is not evidence for it. Reaching R from P through Q does not compose additively in the extension count: triangEnvelopeIter_add says P.triangEnvelopeIter (n + m) is the retract closure of extensions of a P.triangEnvelopeIter n' by a P.triangEnvelopeIter m, with n = n' + 1, so the count is off by one at every composition and the honest law is multiplicative in the ⟨-⟩-index of Bondal--Van den Bergh, where ⟨P⟩_{n + 1} is P.triangEnvelopeIter n: composing ⟨-⟩_a with ⟨-⟩_b lands in ⟨-⟩_{a b} (Stacks 0FXA), which in extension counts reads ((a + 1) * (b + 1)) - 1, not a + b. That composition law is the deliverable of the follow-up issue on composition of iterated envelopes and is not proved here; do not re-derive an additive bound from triangEnvelopeIter_add.

noncomputable def CategoryTheory.ObjectProperty.generationTime {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P Q : ObjectProperty C) : ℕ∞

Generation time. The least n : ℕ with Q ≤ P.triangEnvelopeIter n, as an element of ℕ∞; ⊤ when there is none. sInf over ℕ∞ is total, and sInf ∅ = ⊤ is the junk-value convention.

Equations

• P.generationTime Q = sInf ((fun (m : ℕ) => ↑m) '' {m : ℕ | Q ≤ P.triangEnvelopeIter m})

theorem CategoryTheory.ObjectProperty.generationTime_le_coe_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P Q : ObjectProperty C) (n : ℕ) : P.generationTime Q ≤ ↑n ↔ Q ≤ P.triangEnvelopeIter n

The characterisation of generation time. P.generationTime Q ≤ n exactly when Q is reachable from P with at most n extensions.

theorem CategoryTheory.ObjectProperty.generationTime_antitone_left {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {P P' : ObjectProperty C} (h : P ≤ P') (Q : ObjectProperty C) : P'.generationTime Q ≤ P.generationTime Q

Generation time is antitone in the generating property: more generators, fewer steps.

theorem CategoryTheory.ObjectProperty.generationTime_mono_right {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {Q Q' : ObjectProperty C} (h : Q ≤ Q') : P.generationTime Q ≤ P.generationTime Q'

Generation time is monotone in the generated property: more to reach, more steps.

theorem CategoryTheory.ObjectProperty.generationTime_eq_zero_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P Q : ObjectProperty C) : P.generationTime Q = 0 ↔ Q ≤ P.triangEnvelopeIter 0

Generation time is zero exactly when no extension is needed.

theorem CategoryTheory.ObjectProperty.generationTime_eq_zero_iff' {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P Q : ObjectProperty C) : P.generationTime Q = 0 ↔ Q ≤ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure

Generation time is zero exactly when Q lies in the retract closure of binary products of shifts of P: generationTime_eq_zero_iff with the zeroth envelope unfolded.

theorem CategoryTheory.ObjectProperty.generationTime_self {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.generationTime P = 0

A property generates itself in no steps, unconditionally.

theorem CategoryTheory.ObjectProperty.generationTime_eq_top_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P Q : ObjectProperty C) : P.generationTime Q = ⊤ ↔ ∀ (n : ℕ), ¬Q ≤ P.triangEnvelopeIter n

Generation time is infinite exactly when no finite number of extensions suffices.

theorem CategoryTheory.ObjectProperty.isStrongTriangulatedGenerator_iff_generationTime_ne_top {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) : P.IsStrongTriangulatedGenerator ↔ P.generationTime ⊤ ≠ ⊤

Strong generation is finite generation time. P is a strong triangulated generator exactly when P.generationTime ⊤ ≠ ⊤.

theorem CategoryTheory.ObjectProperty.isClassicalTriangulatedGenerator_of_generationTime_ne_top {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (h : P.generationTime ⊤ ≠ ⊤) : P.IsClassicalTriangulatedGenerator

Finite generation time makes P a classical triangulated generator, through strong generation.