Owner-authored pre-stability conditions

A pre-stability condition consists of a slicing and a central charge whose value on every nonzero semistable object lies on the positive ray determined by its phase. Local finiteness is deliberately deferred to the next ownership slice.

structure CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) extends CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition v : Type (max u u')

A pre-stability condition whose central charge factors through a chosen class map v : K₀ C → Λ.

Ordinary prestability is a strict refinement of weak prestability. The named parent projection makes that relationship part of the Lean type rather than a downstream compatibility adapter.

• slicing : Slicing C
• Z : Λ →+ ℂ
• compat' (φ : ℝ) (E : C) : self.slicing.P φ E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 ≤ m ∧ ((∀ (n : ℤ), φ ≠ ↑n) → 0 < m) ∧ self.Z (v (K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)
• compatible (φ : ℝ) (E : C) : self.slicing.P φ E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 < m ∧ self.Z (v (K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)

  A nonzero semistable object's charge lies on its positive phase ray.

def CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ofStrict {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (slicing : Slicing C) (Z : Λ →+ ℂ) (compatible : ∀ (φ : ℝ) (E : C), slicing.P φ E → ¬Limits.IsZero E → ∃ (m : ℝ), 0 < m ∧ Z (v (K₀.of C E)) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)) : WithClassMap C v

Build ordinary prestability from its strict compatibility proof. The weak compatibility field is derived canonically from strict positivity.

Equations

• CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ofStrict slicing Z compatible = { slicing := slicing, Z := Z, compat' := ⋯, compatible := compatible }

@[reducible, inline]

abbrev CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) (E : C) : ℂ

The central charge evaluated on the class of an object.

Equations

• σ.charge E = σ.Z (CategoryTheory.Triangulated.classOf C v E)

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_def {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) (E : C) : σ.charge E = σ.Z (classOf C v E)

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.compat {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) (φ : ℝ) (E : C) (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) : ∃ (m : ℝ), 0 < m ∧ σ.charge E = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)

Compatibility expressed through charge.

@[simp]

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_isZero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) {E : C} (hE : Limits.IsZero E) : σ.charge E = 0

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_congr {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} (h : σ.Z = τ.Z) (E : C) : σ.charge E = τ.charge E

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge_postnikovTower_eq_sum {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} (σ : WithClassMap C v) {E : C} (P : PostnikovTower C E) : σ.charge E = ∑ i : Fin P.n, σ.charge (P.factor i)

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ext {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} (hslicing : σ.slicing = τ.slicing) (hZ : σ.Z = τ.Z) : σ = τ

theorem CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.ext_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ C →+ Λ} {σ τ : WithClassMap C v} : σ = τ ↔ σ.slicing = τ.slicing ∧ σ.Z = τ.Z

@[reducible, inline]

abbrev CategoryTheory.Triangulated.PreStabilityCondition (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Type u

A pre-stability condition with the identity class map.

Equations

• CategoryTheory.Triangulated.PreStabilityCondition C = CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C (AddMonoidHom.id (CategoryTheory.Triangulated.K₀ C))

theorem CategoryTheory.Triangulated.preStabilityCondition_compat_apply (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (σ : PreStabilityCondition C) (φ : ℝ) (E : C) (hP : σ.slicing.P φ E) (hE : ¬Limits.IsZero E) : ∃ (m : ℝ), 0 < m ∧ σ.Z (K₀.of C E) = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)