Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.ExtensionClosure

Extension closure #

The extension closure generated by an object property, defined intrinsically from distinguished triangles.

Placement #

Generic triangulated vocabulary: this file imports only PostnikovTower and Mathlib, mentions no stability condition, and lives in namespace CategoryTheory.Triangulated. It sat under StabilityCondition/Foundation/ until #488 because its consumers are the deformed phase cuts (Foundation/Deformation/), which is a statement about who calls it, not about what it is. Same move as #454 made for PostnikovTower and K₀.

What this file does not assert #

The closure is an ObjectProperty, not a subcategory with structure. The only instance proved about it is IsClosedUnderIsomorphisms; it is not shown to be closed under shifts, to be thick, or to be a triangulated subcategory, and although Mathlib.CategoryTheory.Triangulated.Subcategory is imported, no declaration here compares the two.

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

The owner extension closure generated by an object property.

Instances For
    source
    theorem CategoryTheory.Triangulated.ExtensionClosure.mono {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} (h : P ≤ Q) :
    ExtensionClosure P ≤ ExtensionClosure Q

    Owner extension closure is monotone in its generators.

    source
    theorem CategoryTheory.Triangulated.ExtensionClosure.hom_eq_zero {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} (h : ∀ (E F : C), P E → Q F → ∀ (f : E ⟶ F), f = 0) {E F : C} (hE : ExtensionClosure P E) (hF : ExtensionClosure Q F) (f : E ⟶ F) :
    f = 0

    Orthogonal generators have orthogonal owner extension closures.

    source
    theorem CategoryTheory.Triangulated.ExtensionClosure.ofIso {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 Y : C} (e : X ≅ Y) (h : ExtensionClosure P X) :
    ExtensionClosure P Y

    Owner extension closure is invariant under isomorphism.

    source
    theorem CategoryTheory.Triangulated.ExtensionClosure.ofPostnikovTower {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Q : ObjectProperty C} {E : C} (P : PostnikovTower C E) (hfactors : ∀ (i : Fin P.n), Q (P.factor i)) :
    ExtensionClosure Q E

    Walking an owner Postnikov tower assembles extension-closure membership from membership of all factors.

    source
    instance CategoryTheory.Triangulated.ExtensionClosure.instIsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (P : ObjectProperty C) :
    (ExtensionClosure P).IsClosedUnderIsomorphisms
    source
    theorem CategoryTheory.Triangulated.ExtensionClosure.le_of_closed {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} (hzero : ∀ {E : C}, Limits.IsZero E → Q E) (hmem : P ≤ Q) (hext : ∀ {X E Y : C} {f : X ⟶ E} {g : E ⟶ Y} {h : Y ⟶ (shiftFunctor C 1).obj X}, Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles → Q X → Q Y → Q E) :
    ExtensionClosure P ≤ Q

    Induction principle into any object property containing zero and the generators and closed under distinguished extensions.