The owner deformed slicing predicate

This module defines the candidate phase slices associated to a controlled perturbation of the central charge. The predicate records the thin old phase window on which perturbed semistability is witnessed; construction of its HN filtrations is deliberately left to the subsequent assembly modules.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) (ε ψ : ℝ) : ObjectProperty C

The candidate deformed slice of phase ψ. A nonzero object belongs when it is perturbed-semistable in a thin old interval which envelops ψ by the deformation radius ε.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_of_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 Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) (ε ψ : ℝ) {E : C} (hE : Limits.IsZero E) : deformedPred C σ W hr0 hr1 hW ε ψ E

Every zero object belongs to every owner deformed slice.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_isClosedUnderIsomorphisms (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) (ε ψ : ℝ) : (deformedPred C σ W hr0 hr1 hW ε ψ).IsClosedUnderIsomorphisms

The owner deformed slice is invariant under isomorphism.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.exists_deformedPred_witness (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε ψ : ℝ} {E : C} (h : deformedPred C σ W hr0 hr1 hW ε ψ E) (hE : ¬Limits.IsZero E) : ∃ (a : ℝ) (b : ℝ) (hab : a < b), b - a + 2 * ε < 1 ∧ a + ε ≤ ψ ∧ ψ ≤ b - ε ∧ (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ψ

A nonzero member of an owner deformed slice exposes its thin interval witness and perturbed-semistability proof.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_charge_ne (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε ψ : ℝ} {E : C} (h : deformedPred C σ W hr0 hr1 hW ε ψ E) (hE : ¬Limits.IsZero E) : W (classOf C κ E) ≠ 0

The perturbed charge of a nonzero owner deformed-slice object does not vanish.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_charge_polar (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε ψ : ℝ} {E : C} (h : deformedPred C σ W hr0 hr1 hW ε ψ E) (hE : ¬Limits.IsZero E) : W (classOf C κ E) = ↑‖W (classOf C κ E)‖ * Complex.exp (↑(Real.pi * ψ) * Complex.I)

The perturbed charge of a nonzero deformed-slice object lies on the ray of its recorded phase.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_intrinsic_phase_window (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε ψ : ℝ} {E : C} (h : deformedPred C σ W hr0 hr1 hW ε ψ E) (hE : ¬Limits.IsZero E) : ∃ (a : ℝ) (b : ℝ), b - a + 2 * ε < 1 ∧ a + ε ≤ ψ ∧ ψ ≤ b - ε ∧ a < Slicing.phiMinus C σ.slicing E hE ∧ Slicing.phiPlus C σ.slicing E hE < b

A nonzero deformed-slice object belongs to an old thin interval whose endpoints both envelop the new phase.