The owner slicing distance

The generalized Bridgeland distance on repository-owned slicings is the supremum of the two intrinsic phase discrepancies. It defines the intrinsic pseudo-extended-metric topology on owner slicings.

noncomputable def CategoryTheory.Triangulated.slicingDist (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) : ENNReal

The generalized distance between two owner slicings.

Equations

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

theorem CategoryTheory.Triangulated.slicingDistTerm_le (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) (E : C) (hE : ¬Limits.IsZero E) : ENNReal.ofReal (max |Slicing.phiPlus C s E hE - Slicing.phiPlus C t E hE| |Slicing.phiMinus C s E hE - Slicing.phiMinus C t E hE|) ≤ slicingDist C s t

The discrepancy on one nonzero object is bounded by the slicing distance.

theorem CategoryTheory.Triangulated.phiPlusDist_le (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) (E : C) (hE : ¬Limits.IsZero E) : ENNReal.ofReal |Slicing.phiPlus C s E hE - Slicing.phiPlus C t E hE| ≤ slicingDist C s t

The highest-phase discrepancy is bounded by the slicing distance.

theorem CategoryTheory.Triangulated.phiMinusDist_le (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) (E : C) (hE : ¬Limits.IsZero E) : ENNReal.ofReal |Slicing.phiMinus C s E hE - Slicing.phiMinus C t E hE| ≤ slicingDist C s t

The lowest-phase discrepancy is bounded by the slicing distance.

@[simp]

theorem CategoryTheory.Triangulated.slicingDist_self (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) : slicingDist C s s = 0

The owner slicing distance vanishes on the diagonal.

theorem CategoryTheory.Triangulated.slicingDist_symm (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) : slicingDist C s t = slicingDist C t s

The owner slicing distance is symmetric.

theorem CategoryTheory.Triangulated.slicingDist_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t u : Slicing C) : slicingDist C s u ≤ slicingDist C s t + slicingDist C t u

The owner slicing distance satisfies the triangle inequality.

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.instPseudoEMetricSpaceSlicing (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : PseudoEMetricSpace (Slicing C)

Owner slicings carry the pseudo-extended metric induced by intrinsic phase distance.

Equations

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

theorem CategoryTheory.Triangulated.abs_phiPlus_sub_lt_of_slicingDist (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) {E : C} (hE : ¬Limits.IsZero E) {ε : ℝ} (hε : 0 < ε) (hd : slicingDist C s t < ENNReal.ofReal ε) : |Slicing.phiPlus C s E hE - Slicing.phiPlus C t E hE| < ε

A strict slicing-distance bound controls the highest intrinsic phase.

theorem CategoryTheory.Triangulated.abs_phiMinus_sub_lt_of_slicingDist (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) {E : C} (hE : ¬Limits.IsZero E) {ε : ℝ} (hε : 0 < ε) (hd : slicingDist C s t < ENNReal.ofReal ε) : |Slicing.phiMinus C s E hE - Slicing.phiMinus C t E hE| < ε

A strict slicing-distance bound controls the lowest intrinsic phase.

theorem CategoryTheory.Triangulated.intervalProp_of_semistable_slicingDist (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) {E : C} {φ : ℝ} (hE : ¬Limits.IsZero E) (hP : t.P φ E) {ε : ℝ} (hε : 0 < ε) (hd : slicingDist C s t < ENNReal.ofReal ε) : Slicing.intervalProp C s (φ - ε) (φ + ε) E

A nonzero semistable object for a nearby slicing lies in the corresponding phase window for the original slicing.

theorem CategoryTheory.Triangulated.slicingDist_le_of_phase_bounds (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s t : Slicing C) {ε : ℝ} (hplus : ∀ (E : C) (hE : ¬Limits.IsZero E), |Slicing.phiPlus C s E hE - Slicing.phiPlus C t E hE| ≤ ε) (hminus : ∀ (E : C) (hE : ¬Limits.IsZero E), |Slicing.phiMinus C s E hE - Slicing.phiMinus C t E hE| ≤ ε) : slicingDist C s t ≤ ENNReal.ofReal ε

Uniform phase bounds give an upper bound for the owner slicing distance.