Bridgeland Stability Conditions

4. ExtensionClosure🔗

4.1. ExtensionClosure🔗

The extension-closed subcategory generated by an object property P (Bridgeland p.6). An object E is in P^{\operatorname{ext}} if it is zero, satisfies P, or is the middle term of a distinguished triangle whose other two terms are in P^{\operatorname{ext}}. This is the smallest extension-closed subcategory containing P and zero objects.

Construction: An inductive type with three constructors: zero (any zero object is in the closure), mem (any object satisfying P is in the closure), and ext (if X \to E \to Y \to X[1] is distinguished and X, Y are in the closure, then E is in the closure).

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

Constructors

zero.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} {E : C} :
  CategoryTheory.Limits.IsZero E → P.ExtensionClosure E
mem.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} {E : C} :
  P E → P.ExtensionClosure E
ext.{v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} {X E Y : C}
  {f : X ⟶ E} {g : E ⟶ Y}
  {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X} :
  CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
      CategoryTheory.Pretriangulated.distinguishedTriangles →
    P.ExtensionClosure X →
      P.ExtensionClosure Y → P.ExtensionClosure E

Something wrong, better idea? Suggest a change

4.2. mono🔗

Extension closure is monotone: if P \le Q (i.e., P(E) \Rightarrow Q(E) for all E), then P^{\operatorname{ext}} \le Q^{\operatorname{ext}}.

Proof: Induction on the ExtensionClosure derivation: zero maps to zero, membership follows from P \le Q, and extensions are preserved since the inductive hypotheses give membership in Q^{\operatorname{ext}} for both outer terms.

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

Something wrong, better idea? Suggest a change

4.3. hom_eq_zero🔗

If generators are orthogonal (\operatorname{Hom}(P, Q) = 0), their extension closures are orthogonal: every morphism from an object in P^{\operatorname{ext}} to an object in Q^{\operatorname{ext}} is zero.

Proof: Nested induction on the ExtensionClosure structure. The base case is the generator orthogonality hypothesis. The extension step uses the exact Hom sequences from the distinguished triangles: coyoneda_exact2 and yoneda_exact2 factor any morphism through the outer terms, where the inductive hypothesis forces it to zero.

🔗theorem
CategoryTheory.ObjectProperty.ExtensionClosure.hom_eq_zero.{v, u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P Q : CategoryTheory.ObjectProperty C}
  (h : ∀ (E F : C), P E → Q F → ∀ (f : E ⟶ F), f = 0) {E F : C}
  (hE : P.ExtensionClosure E) (hF : Q.ExtensionClosure F) (f : E ⟶ F) :
  f = 0
CategoryTheory.ObjectProperty.ExtensionClosure.hom_eq_zero.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P Q : CategoryTheory.ObjectProperty C}
  (h :
    ∀ (E F : C),
      P E → Q F → ∀ (f : E ⟶ F), f = 0)
  {E F : C} (hE : P.ExtensionClosure E)
  (hF : Q.ExtensionClosure F)
  (f : E ⟶ F) : f = 0

Something wrong, better idea? Suggest a change

4.4. of_iso🔗

Extension closure is closed under isomorphisms: if X \cong Y and X \in P^{\operatorname{ext}}, then Y \in P^{\operatorname{ext}}.

Proof: Complete the isomorphism e : X \xrightarrow{\sim} Y to a distinguished triangle X \to Y \to Z \to X[1]. Since e is an iso, Z is zero. Then Y is an extension of X (in the closure) by Z (zero, hence in the closure).

🔗theorem
CategoryTheory.ObjectProperty.ExtensionClosure.of_iso.{v, u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} {X Y : C} (e : X ≅ Y)
  (h : P.ExtensionClosure X) : P.ExtensionClosure Y
CategoryTheory.ObjectProperty.ExtensionClosure.of_iso.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C}
  {X Y : C} (e : X ≅ Y)
  (h : P.ExtensionClosure X) :
  P.ExtensionClosure Y

Something wrong, better idea? Suggest a change

4.5. of_postnikovTower🔗

Walking a Postnikov tower: if every factor of a Postnikov tower of E satisfies Q, then E \in Q^{\operatorname{ext}}. This is the bridge from HN-filtration data to extension-closure membership.

Proof: Induction on the chain length k. The base case k = 0 uses the zero base. The inductive step uses the k-th distinguished triangle: A_k is in the closure by the inductive hypothesis, F_k is in the closure by the factor hypothesis, and A_{k+1} is an extension of the two. The top isomorphism A_n \cong E transfers membership.

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

Something wrong, better idea? Suggest a change

4.6. instIsClosedUnderIsomorphisms🔗

The extension closure of any property is closed under isomorphisms: if E \in P^{\mathrm{ext}} and E \cong F, then F \in P^{\mathrm{ext}}.

Construction: Provided by ExtensionClosure.of_iso.

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

Something wrong, better idea? Suggest a change

4.7. instIsTriangulatedClosed₂🔗

The extension closure is closed under extensions from distinguished triangles: if X, Y \in P^{\mathrm{ext}} and X \to E \to Y \to X[1] is a distinguished triangle, then E \in P^{\mathrm{ext}}.

Construction: The instance witnesses IsTriangulatedClosed₂ using the ExtensionClosure.ext constructor directly.

🔗theorem
CategoryTheory.ObjectProperty.ExtensionClosure.instIsTriangulatedClosed₂.{v,
    u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) :
  P.ExtensionClosure.IsTriangulatedClosed₂
CategoryTheory.ObjectProperty.ExtensionClosure.instIsTriangulatedClosed₂.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) :
  P.ExtensionClosure.IsTriangulatedClosed₂

Something wrong, better idea? Suggest a change

4.8. le_of_closed🔗

Extension closure is a left adjoint: P^{\operatorname{ext}} \le Q whenever Q contains zero objects, contains P, and is closed under extensions from distinguished triangles. This characterizes P^{\operatorname{ext}} as the smallest such property.

Proof: Induction on the ExtensionClosure derivation, dispatching each constructor to the corresponding hypothesis.

🔗theorem
CategoryTheory.ObjectProperty.ExtensionClosure.le_of_closed.{v, u}
  {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P Q : CategoryTheory.ObjectProperty C}
  (hzero : ∀ {E : C}, CategoryTheory.Limits.IsZero E → Q E)
  (hmem : P ≤ Q)
  (hext :
    ∀ {X E Y : C} {f : X ⟶ E} {g : E ⟶ Y}
      {h : Y ⟶ (CategoryTheory.shiftFunctor C 1).obj X},
      CategoryTheory.Pretriangulated.Triangle.mk f g h ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles →
        Q X → Q Y → Q E) :
  P.ExtensionClosure ≤ Q
CategoryTheory.ObjectProperty.ExtensionClosure.le_of_closed.{v,
    u}
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  {P Q : CategoryTheory.ObjectProperty C}
  (hzero :
    ∀ {E : C},
      CategoryTheory.Limits.IsZero E →
        Q E)
  (hmem : P ≤ Q)
  (hext :
    ∀ {X E Y : C} {f : X ⟶ E} {g : E ⟶ Y}
      {h :
        Y ⟶
          (CategoryTheory.shiftFunctor C
                1).obj
            X},
      CategoryTheory.Pretriangulated.Triangle.mk
            f g h ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles →
        Q X → Q Y → Q E) :
  P.ExtensionClosure ≤ Q

Something wrong, better idea? Suggest a change