Interval independence for owner deformed slices

The owner candidate slicing is defined using an existential thin old interval. This module supplies the comparison lemmas that let later constructions replace one interval witness by a compatible smaller witness without changing the perturbed phase or semistability condition.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_eq_of_target_envelope (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) {a b c d ε ψ : ℝ} (hab : a < b) (hcd : c < d) (hε : 0 < ε) (hthinTarget : d - c + 2 * ε < 1) (hcψ : c + ε ≤ ψ) (hψd : ψ ≤ d - ε) {E : C} (hSS : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ψ) : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hcd).phase E = ψ

A perturbed-semistable object's recorded phase is unchanged when read on any other thin owner branch whose interval envelops that phase. This is the phase-choice part of interval independence; transport of all admissible subobject tests is handled separately.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_rewitness_subinterval (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) {a b c d ε ψ : ℝ} (hab : a < b) (hcd : c < d) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthinSource : b - a + 2 * ε < 1) (hthinTarget : d - c + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (hleft : (c + d) / 2 - 1 < a - ε) (hright : b + ε ≤ (c + d) / 2 + 1) (hcψ : c + ε ≤ ψ) (hψd : ψ ≤ d - ε) (hmono : Slicing.intervalProp C σ.slicing c d ≤ Slicing.intervalProp C σ.slicing a b) {E : C} (hI : Slicing.intervalProp C σ.slicing c d E) (hSS : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ψ) : deformedPred C σ W hr0 hr1 hW ε ψ E

A deformed-slice witness may be replaced by a compatible thin subinterval that still envelops the recorded perturbed phase.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_nested_interval (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) {a b c d ε ψ : ℝ} (hab : a < b) (hcd : c < d) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthin : b - a + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (hleft : (c + d) / 2 - 1 < a - ε) (hright : b + ε ≤ (c + d) / 2 + 1) (hac : a ≤ c) (hdb : d ≤ b) {E : C} (hI : Slicing.intervalProp C σ.slicing c d E) (hSS : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ψ) : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hcd).IsSemistable E ψ

Endpoint inequalities provide the interval inclusion required by owner semistability transport.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_controlled_subinterval (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) {a b c d ε ψ : ℝ} (hab : a < b) (hcd : c < d) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthinTarget : d - c + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (hleft : (a + b) / 2 - 1 < c - ε) (hright : d + ε ≤ (a + b) / 2 + 1) (hac : a ≤ c) (hdb : d ≤ b) {E : C} (hI : Slicing.intervalProp C σ.slicing c d E) (hSS : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ψ) : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hcd).IsSemistable E ψ

Semistability restricts to a nested thin interval when the smaller interval's controlled phase window lies in the original branch.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_on_witness_intersection (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) {a b c d ε ψ : ℝ} (hab : a < b) (_hcd : c < d) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthin : b - a + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (haψ : a + ε ≤ ψ) (hψb : ψ ≤ b - ε) (hcψ : c + ε ≤ ψ) (hψd : ψ ≤ d - ε) {E : C} (hI : Slicing.intervalProp C σ.slicing c d E) (hSS : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ψ) : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW ⋯).IsSemistable E ψ

Two phase-enveloping witness intervals admit their intersection as a common thin presentation of the first skewed-semistability proof.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_common_refinement (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) {a b c d ε ψ : ℝ} (hab : a < b) (hcd : c < d) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthinAB : b - a + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (haψ : a + ε ≤ ψ) (hψb : ψ ≤ b - ε) (hcψ : c + ε ≤ ψ) (hψd : ψ ≤ d - ε) {E : C} (hAB : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ψ) (hCD : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hcd).IsSemistable E ψ) : ∃ (hinter : max a c < min b d), have F := WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hinter; F.IsSemistable E ψ ∧ F.phase E = (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).phase E ∧ F.phase E = (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hcd).phase E

Two complete witness presentations restrict to semistability proofs on one common thin intersection interval.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_rewitness_nested_interval (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) {a b c d ε ψ : ℝ} (hab : a < b) (hcd : c < d) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthinSource : b - a + 2 * ε < 1) (hthinTarget : d - c + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (hleft : (c + d) / 2 - 1 < a - ε) (hright : b + ε ≤ (c + d) / 2 + 1) (hcψ : c + ε ≤ ψ) (hψd : ψ ≤ d - ε) (hac : a ≤ c) (hdb : d ≤ b) {E : C} (hI : Slicing.intervalProp C σ.slicing c d E) (hSS : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable E ψ) : deformedPred C σ W hr0 hr1 hW ε ψ E

A deformed-slice witness may be replaced by a nested compatible thin interval using only endpoint inequalities.