Extension closure and triangulated envelopes

This file compares CategoryTheory.Triangulated.ExtensionClosure with Mathlib's CategoryTheory.ObjectProperty.extensionProductIter and CategoryTheory.ObjectProperty.triangEnvelope without adding closure operations or strengthening the owner extension closure. Every finite iterate of CategoryTheory.ObjectProperty.extensionProduct lies in the owner extension closure. Conversely, the whole owner extension closure lies in the triangulated envelope when the generators are nonempty and the category is triangulated.

Main definitions

This file introduces no definitions. It reuses the owner extension closure and Mathlib's extension-product and triangulated-envelope constructions.

Main results

Declaration	Role
CategoryTheory.Triangulated.ExtensionClosure.extensionProductIter_le	Finite iterates lie in the owner closure.
CategoryTheory.Triangulated.ExtensionClosure.le_of_closed_under_isomorphisms	Restates closure induction using Mathlib's typeclass hypotheses.
CategoryTheory.Triangulated.ExtensionClosure.le_triangEnvelope	Compares the owner closure and Mathlib's envelope under nonemptiness.
CategoryTheory.Triangulated.ExtensionClosure.eq_iSup_extensionProductIter	Identifies the owner closure with the supremum after adjoining zero objects.
CategoryTheory.Triangulated.ExtensionClosure.extensionProductIter_le_triangEnvelopeIter	Preserves the finite stage index.
CategoryTheory.Triangulated.ExtensionClosure.generationTime_singleton_le_of_mem_extensionProductIter	Converts a finite stage into a generation-time bound.

Implementation notes

The nonemptiness assumption in the envelope comparison is essential: when P = ⊥, CategoryTheory.Triangulated.ExtensionClosure contains every zero object by its zero constructor, while CategoryTheory.ObjectProperty.triangEnvelope sends ⊥ to ⊥. The supremum equality adjoins CategoryTheory.Limits.IsZero: the owner closure contains zero objects even when its generator property is empty. The numerical bound uses a direct inclusion into each CategoryTheory.ObjectProperty.triangEnvelopeIter stage; passing through the whole triangulated envelope would lose the count.

The typeclass restatement of CategoryTheory.Triangulated.ExtensionClosure.le_of_closed uses CategoryTheory.ObjectProperty.ContainsZero together with closure under isomorphisms: its witness gives one zero object, and CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms transfers membership to every zero object.

References

• Mathlib.CategoryTheory.Triangulated.Subcategory
• Mathlib.CategoryTheory.Triangulated.Generators
• Mathlib.CategoryTheory.ObjectProperty.ContainsZero

Tags

extension closure, triangulated envelope, generation time

theorem CategoryTheory.Triangulated.ExtensionClosure.extensionProductIter_le {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (n : ℕ) : P.extensionProductIter n ≤ ExtensionClosure P

Every finite iterate of Mathlib's extension product is contained in the repository's owner extension closure. The triangle in CategoryTheory.ObjectProperty.extensionProduct has the orientation used by CategoryTheory.Triangulated.ExtensionClosure.ext, so no rotation is needed.

theorem CategoryTheory.Triangulated.ExtensionClosure.le_of_closed_under_isomorphisms {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} [Q.ContainsZero] [Q.IsClosedUnderIsomorphisms] [Q.IsTriangulatedClosed₂] (hPQ : P ≤ Q) : ExtensionClosure P ≤ Q

Induction into an isomorphism-closed property containing a zero object and closed under distinguished extensions. The CategoryTheory.ObjectProperty.ContainsZero witness is enough because CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms transfers it to every zero object.

theorem CategoryTheory.Triangulated.ExtensionClosure.le_triangEnvelope {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.Nonempty] [IsTriangulated C] : ExtensionClosure P ≤ P.triangEnvelope

If the generators are nonempty and the category is triangulated, the owner extension closure is contained in Mathlib's triangulated envelope. The CategoryTheory.IsTriangulated hypothesis supplies closure under distinguished extensions, and nonemptiness supplies zero objects to that envelope. Nonemptiness is essential: for P = ⊥, the owner closure contains zero objects, but CategoryTheory.ObjectProperty.triangEnvelope sends ⊥ to ⊥.

theorem CategoryTheory.Triangulated.ExtensionClosure.eq_iSup_extensionProductIter {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) [IsTriangulated C] : ExtensionClosure P = ⨆ (n : ℕ), (P ⊔ Limits.IsZero).extensionProductIter n

The owner extension closure is exactly the supremum of Mathlib extension iterates generated by P together with the zero-object property. The zero property is needed because CategoryTheory.Triangulated.ExtensionClosure contains zero objects even when the original generator property is empty.

theorem CategoryTheory.Triangulated.ExtensionClosure.extensionProductIter_le_triangEnvelopeIter {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) (n : ℕ) : P.extensionProductIter n ≤ P.triangEnvelopeIter n

Mathlib's extension iterate at stage n lies in the corresponding triangulated-envelope stage. This direct comparison preserves the finite step bound used by CategoryTheory.ObjectProperty.generationTime.

theorem CategoryTheory.Triangulated.ExtensionClosure.generationTime_singleton_le_of_mem_extensionProductIter {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) {X : C} (n : ℕ) (hX : P.extensionProductIter n X) : P.generationTime (ObjectProperty.singleton X) ≤ ↑n

An object in the nth extension-product iterate has generation time at most n, by its direct inclusion into the nth triangulated-envelope stage.