Hom-vanishing preparations for owner deformed slices

This module separates the formal interval-orthogonality part of sharp deformed Hom-vanishing from the phase-confinement and midpoint-heart image arguments which supply its hypotheses.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_intrinsic_deformed_gap (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 κ) {E F : C} {ψ₁ ψ₂ ε : ℝ} (hE : ¬Limits.IsZero E) (hF : ¬Limits.IsZero F) (hElo : ψ₁ - ε ≤ Slicing.phiMinus C σ.slicing E hE) (hEhi : Slicing.phiPlus C σ.slicing E hE ≤ ψ₁ + ε) (hFlo : ψ₂ - ε ≤ Slicing.phiMinus C σ.slicing F hF) (hFhi : Slicing.phiPlus C σ.slicing F hF ≤ ψ₂ + ε) (hgap : ψ₂ + 2 * ε < ψ₁) (f : E ⟶ F) : f = 0

Objects intrinsically confined to radius ε around phases separated by more than 2ε have no morphisms from the larger phase to the smaller one.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedPred_large_gap (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 F : C} (hE : deformedPred C σ W hr0 hr1 hW ε ψ₁ E) (hF : deformedPred C σ W hr0 hr1 hW ε ψ₂ F) (hconf : ∀ {X : C} {ψ : ℝ}, deformedPred C σ W hr0 hr1 hW ε ψ X → ∀ (hX : ¬Limits.IsZero X), ψ - ε ≤ Slicing.phiMinus C σ.slicing X hX ∧ Slicing.phiPlus C σ.slicing X hX ≤ ψ + ε) (hgap : ψ₂ + 2 * ε < ψ₁) (f : E ⟶ F) : f = 0

Large-gap Hom-vanishing for owner deformed predicates from weak intrinsic phase confinement.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedPred_gap (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 →+ Λ} [IsTriangulated C] (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε ψ₁ ψ₂ : ℝ} (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) {E F : C} (hE : deformedPred C σ W hr0 hr1 hW ε ψ₁ E) (hF : deformedPred C σ W hr0 hr1 hW ε ψ₂ F) (hgap : ψ₂ + 2 * ε < ψ₁) (f : E ⟶ F) : f = 0

Owner deformed slices separated by more than twice the deformation radius are Hom-orthogonal.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedCuts_gap (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 →+ Λ} [IsTriangulated C] (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε t₁ t₂ : ℝ} (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (hsep : t₂ + 2 * ε ≤ t₁) {E F : C} (hE : deformedGtPred C σ W hr0 hr1 hW ε t₁ E) (hF : deformedLePred C σ W hr0 hr1 hW ε t₂ F) (f : E ⟶ F) : f = 0

Extension-closed owner deformed cuts are Hom-orthogonal once their cutoffs are separated by twice the deformation radius.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_skewed_small_gap (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 →+ Λ} [IsTriangulated C] (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {a l u δ ε ψ₁ ψ₂ : ℝ} (hau : a < u) (hua : u ≤ a + 1) (hla : l < a + 1) (hδ : 0 < δ) (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hthinLeft : u - a + 2 * ε < 1) (_hthinRight : a + 1 + δ - l + 2 * ε < 1) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (haψ : a + ε ≤ ψ₁) (hψu : ψ₁ ≤ u - ε) (hbranchLeft : (l + (a + 1 + δ)) / 2 - 1 < a - ε) (hbranchRight : u + ε ≤ (l + (a + 1 + δ)) / 2 + 1) {E F : C} (hE : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hau).IsSemistable E ψ₁) (hF : (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW ⋯).IsSemistable F ψ₂) (hE_lower : ∀ (hEne : ¬Limits.IsZero E), l < Slicing.phiMinus C σ.slicing E hEne) (hF_upper : ∀ (hFne : ¬Limits.IsZero F), Slicing.phiPlus C σ.slicing F hFne < u) (hEheart : (Slicing.toTStructure C (Slicing.phaseShift C σ.slicing a)).heart E) (hFheart : (Slicing.toTStructure C (Slicing.phaseShift C σ.slicing a)).heart F) (hgap : ψ₂ < ψ₁) (f : E ⟶ F) : f = 0

Sharp Hom-vanishing in the small-gap branch once the source and target have been transported to the two overlapping thin interval presentations. The common midpoint heart supplies an abelian image; semistability bounds its phase from opposite sides, while interval independence identifies the two selected image phases.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedPred_of_target_transport (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 →+ Λ} [IsTriangulated C] (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε : ℝ} (hε : 0 < ε) (hε2 : ε ≤ 1 / 2) (hε8 : ε < 1 / 8) (hsin : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε))) (htransport : ∀ {a b c d ψ : ℝ} {X : C} (hab : a < b) (hcd : c < d), b - a + 2 * ε < 1 → d - c + 2 * ε < 1 → a + ε ≤ ψ → ψ ≤ b - ε → c + ε ≤ ψ → ψ ≤ d - ε → Slicing.intervalProp C σ.slicing c d X → (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hab).IsSemistable X ψ → (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW hcd).IsSemistable X ψ) {E F : C} {ψ₁ ψ₂ : ℝ} (hE : deformedPred C σ W hr0 hr1 hW ε ψ₁ E) (hF : deformedPred C σ W hr0 hr1 hW ε ψ₂ F) (hgap : ψ₂ < ψ₁) (f : E ⟶ F) : f = 0

Sharp Hom-vanishing reduced to the one remaining interval-widening contract. All witness extraction, boundary reduction, midpoint-heart placement, and small-gap phase arithmetic are owner-native in this theorem. The transport hypothesis says that semistability may be read on any second thin interval which contains the object and envelops the same phase.