Bridgeland Stability Conditions

13.2. StabilityCondition: ConnectedComponent🔗

13.2.1. exists_basisNhd_subset_connectedComponent🔗

Every stability condition admits a small Bridgeland basis neighborhood contained in its topological connected component. Concretely, there exists \varepsilon \in (0, 1/8) such that B_\varepsilon(\sigma) is contained in the connected component of \sigma.

Proof: Takes the \varepsilon_0 < 1/10 witness from exists_epsilon0_tenth, sets \varepsilon = \varepsilon_0/2, and applies basisNhd_subset_connectedComponent_small.

🔗theorem
CategoryTheory.Triangulated.exists_basisNhd_subset_connectedComponent.{v,
    u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) :
  ∃ ε,
    0 < ε ∧
      ε < 1 / 8 ∧
        CategoryTheory.Triangulated.basisNhd C σ ε ⊆
          {τ | ConnectedComponents.mk τ = ConnectedComponents.mk σ}
CategoryTheory.Triangulated.exists_basisNhd_subset_connectedComponent.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v) :
  ∃ ε,
    0 < ε ∧
      ε < 1 / 8 ∧
        CategoryTheory.Triangulated.basisNhd
            C σ ε ⊆
          {τ |
            ConnectedComponents.mk τ =
              ConnectedComponents.mk σ}

Something wrong, better idea? Suggest a change

13.2.2. stabilityCondition_isOpen_connectedComponent🔗

Connected components of \operatorname{Stab}(\mathcal{D}) are open. Every connected component is an open subset in the Bridgeland topology.

Proof: For each point x in the connected component, exists_basisNhd_subset_connectedComponent provides a basis neighborhood inside the component, which is open by construction. So every point is an interior point.

🔗theorem
CategoryTheory.Triangulated.stabilityCondition_isOpen_connectedComponent.{v,
    u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) :
  IsOpen (connectedComponent σ)
CategoryTheory.Triangulated.stabilityCondition_isOpen_connectedComponent.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v) :
  IsOpen (connectedComponent σ)

Something wrong, better idea? Suggest a change

13.2.3. stabSeminorm_dominated_of_connected🔗

[Lemma 6.2] one direction; apply both ways for full equivalence

Lemma 6.2: On a connected component, seminorms are dominated. If \sigma and \tau lie in the same connected component \Sigma of \operatorname{Stab}(\mathcal{D}), then there exists a finite constant K such that \|U\|_\sigma \leq K \cdot \|U\|_\tau for all U \in \operatorname{Hom}(\Lambda, \mathbb{C}).

Proof: Uses the preconnected induction lemma IsPreconnected.induction₂' on the connected component, with the local step provided by stabSeminorm_dominated_of_basisNhd and transitivity from the multiplicativity of domination constants.

🔗theorem
CategoryTheory.Triangulated.stabSeminorm_dominated_of_connected.{v, u,
    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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (h : ConnectedComponents.mk σ = ConnectedComponents.mk τ) :
  ∃ K,
    K ≠ ⊤ ∧
      ∀ (f : Λ →+ ℂ),
        CategoryTheory.Triangulated.stabSeminorm C σ f ≤
          K * CategoryTheory.Triangulated.stabSeminorm C τ f
CategoryTheory.Triangulated.stabSeminorm_dominated_of_connected.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (h :
    ConnectedComponents.mk σ =
      ConnectedComponents.mk τ) :
  ∃ K,
    K ≠ ⊤ ∧
      ∀ (f : Λ →+ ℂ),
        CategoryTheory.Triangulated.stabSeminorm
            C σ f ≤
          K *
            CategoryTheory.Triangulated.stabSeminorm
              C τ f

Something wrong, better idea? Suggest a change

13.2.4. finiteSeminormSubgroup_eq_of_connected🔗

Lemma 6.2: On a connected component, the finite-seminorm subgroups agree: V(\sigma) = V(\tau) whenever \sigma and \tau are in the same component.

Proof: Both directions follow from stabSeminorm_dominated_of_connected: finite seminorm is preserved under multiplication by a finite constant.

🔗theorem
CategoryTheory.Triangulated.finiteSeminormSubgroup_eq_of_connected.{v,
    u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (h : ConnectedComponents.mk σ = ConnectedComponents.mk τ) :
  CategoryTheory.Triangulated.finiteSeminormSubgroup C σ =
    CategoryTheory.Triangulated.finiteSeminormSubgroup C τ
CategoryTheory.Triangulated.finiteSeminormSubgroup_eq_of_connected.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ τ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (h :
    ConnectedComponents.mk σ =
      ConnectedComponents.mk τ) :
  CategoryTheory.Triangulated.finiteSeminormSubgroup
      C σ =
    CategoryTheory.Triangulated.finiteSeminormSubgroup
      C τ

Something wrong, better idea? Suggest a change

13.2.5. basisNhdFamily🔗

The generating family of Bridgeland basis neighborhoods: \{\, B_\varepsilon(\sigma) : \sigma \in \operatorname{Stab}_v(\mathcal{D}),\, 0 < \varepsilon < 1/8 \,\}.

Construction: Defined as the set of sets of the form basisNhd C σ ε with the positivity and upper bound constraints on \varepsilon.

🔗def
CategoryTheory.Triangulated.basisNhdFamily.{v, u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ} :
  Set
    (Set
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v))
CategoryTheory.Triangulated.basisNhdFamily.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+
      Λ} :
  Set
    (Set
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v))

Something wrong, better idea? Suggest a change

13.2.6. exists_basisNhd_subset_of_mem_open🔗

Every open neighborhood of \sigma contains a centered Bridgeland basis neighborhood B_\varepsilon(\sigma).

Proof: Induction on the structure of TopologicalSpace.GenerateOpen: basic opens are basis neighborhoods (handled by exists_basisNhd_subset_basisNhd); intersections use the minimum of radii; unions are inherited from members.

🔗theorem
CategoryTheory.Triangulated.exists_basisNhd_subset_of_mem_open.{v, u,
    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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {s :
    Set
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)}
  (hs : IsOpen s) (hσ : σ ∈ s) :
  ∃ ε,
    0 < ε ∧ ε < 1 / 8 ∧ CategoryTheory.Triangulated.basisNhd C σ ε ⊆ s
CategoryTheory.Triangulated.exists_basisNhd_subset_of_mem_open.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {s :
    Set
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)}
  (hs : IsOpen s) (hσ : σ ∈ s) :
  ∃ ε,
    0 < ε ∧
      ε < 1 / 8 ∧
        CategoryTheory.Triangulated.basisNhd
            C σ ε ⊆
          s

Something wrong, better idea? Suggest a change

13.2.7. isTopologicalBasis_basisNhd🔗

The Bridgeland basis neighborhoods form a topological basis for \operatorname{Stab}_v(\mathcal{D}).

Proof: Verifies the two conditions of isTopologicalBasis_of_isOpen_of_nhds: each basis neighborhood is open in the generated topology, and every open set containing a point contains a basis neighborhood of that point (via exists_basisNhd_subset_of_mem_open).

🔗theorem
CategoryTheory.Triangulated.isTopologicalBasis_basisNhd.{v, u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  (v : CategoryTheory.Triangulated.K₀ C →+ Λ) :
  TopologicalSpace.IsTopologicalBasis
    (CategoryTheory.Triangulated.basisNhdFamily C)
CategoryTheory.Triangulated.isTopologicalBasis_basisNhd.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  (v :
    CategoryTheory.Triangulated.K₀ C →+
      Λ) :
  TopologicalSpace.IsTopologicalBasis
    (CategoryTheory.Triangulated.basisNhdFamily
      C)

Something wrong, better idea? Suggest a change

13.2.8. exists_basisNhd_subset_of_mem_nhds🔗

Neighborhood-form extraction: if s \in \mathcal{N}(\sigma), then there exists \varepsilon with B_\varepsilon(\sigma) \subseteq s.

Proof: Uses isTopologicalBasis_basisNhd to extract a basis element from the neighborhood filter, then applies exists_basisNhd_subset_basisNhd to recenter.

🔗theorem
CategoryTheory.Triangulated.exists_basisNhd_subset_of_mem_nhds.{v, u,
    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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {s :
    Set
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)}
  (hs : s ∈ nhds σ) :
  ∃ ε,
    0 < ε ∧ ε < 1 / 8 ∧ CategoryTheory.Triangulated.basisNhd C σ ε ⊆ s
CategoryTheory.Triangulated.exists_basisNhd_subset_of_mem_nhds.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {s :
    Set
      (CategoryTheory.Triangulated.StabilityCondition.WithClassMap
        C v)}
  (hs : s ∈ nhds σ) :
  ∃ ε,
    0 < ε ∧
      ε < 1 / 8 ∧
        CategoryTheory.Triangulated.basisNhd
            C σ ε ⊆
          s

Something wrong, better idea? Suggest a change

13.2.9. eq_zero_of_vanishes_on_cl🔗

An additive homomorphism U \colon \Lambda \to \mathbb{C} is zero if it vanishes on all class images \operatorname{cl}_v(E) and v is surjective.

Proof: The vanishing on class images means U \circ v = 0 on K_0(\mathcal{C}) (by the universal property). Surjectivity of v then forces U = 0.

🔗theorem
CategoryTheory.Triangulated.eq_zero_of_vanishes_on_cl.{v, u, 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] {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ} (U : Λ →+ ℂ)
  (hv : Function.Surjective ⇑v)
  (hU : ∀ (E : C), U (CategoryTheory.Triangulated.cl C v E) = 0) : U = 0
CategoryTheory.Triangulated.eq_zero_of_vanishes_on_cl.{v,
    u, 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]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (U : Λ →+ ℂ)
  (hv : Function.Surjective ⇑v)
  (hU :
    ∀ (E : C),
      U
          (CategoryTheory.Triangulated.cl
            C v E) =
        0) :
  U = 0

Something wrong, better idea? Suggest a change

13.2.10. eq_zero_of_stabSeminorm_toReal_eq_zero🔗

If the Bridgeland seminorm of U is finite and equal to zero, then U = 0 (assuming v is surjective).

Proof: Zero seminorm means \|U([E])\| \leq 0 for every semistable nonzero E, so U([E]) = 0 for every semistable object. By the HN filtration decomposition and K_0 additivity, U vanishes on all class images, and surjectivity of v gives U = 0.

🔗theorem
CategoryTheory.Triangulated.eq_zero_of_stabSeminorm_toReal_eq_zero.{v,
    u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (hv : Function.Surjective ⇑v) {U : Λ →+ ℂ}
  (hfin : CategoryTheory.Triangulated.stabSeminorm C σ U < ⊤)
  (hzero :
    (CategoryTheory.Triangulated.stabSeminorm C σ U).toReal = 0) :
  U = 0
CategoryTheory.Triangulated.eq_zero_of_stabSeminorm_toReal_eq_zero.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (hv : Function.Surjective ⇑v)
  {U : Λ →+ ℂ}
  (hfin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ U <
      ⊤)
  (hzero :
    (CategoryTheory.Triangulated.stabSeminorm
          C σ U).toReal =
      0) :
  U = 0

Something wrong, better idea? Suggest a change

13.2.11. Z_mem_finiteSeminormSubgroup🔗

Z(\sigma) has finite \sigma-seminorm: \|Z(\sigma)\|_\sigma \leq 1, so Z(\sigma) \in V(\sigma).

Proof: Each term in the supremum is \|Z([E])\| / \|Z([E])\| \leq 1 (or 0 when Z([E]) = 0).

🔗theorem
CategoryTheory.Triangulated.Z_mem_finiteSeminormSubgroup.{v, u, 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] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v) :
  σ.Z ∈ CategoryTheory.Triangulated.finiteSeminormSubgroup C σ
CategoryTheory.Triangulated.Z_mem_finiteSeminormSubgroup.{v,
    u, 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]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v) :
  σ.Z ∈
    CategoryTheory.Triangulated.finiteSeminormSubgroup
      C σ

Something wrong, better idea? Suggest a change