Extension-closed cuts of the owner deformed predicate

The provisional Q(>t), Q(≤t), and Q(<t) subcategories are the extension closures generated by owner deformed slices on the corresponding side of a phase cutoff. Their order laws are independent of hom-vanishing and HN existence, so they can be owned before the final slicing is assembled.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtGen (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) (ε t : ℝ) : ObjectProperty C

Generators of the provisional owner cut Q(>t).

Equations

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

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLeGen (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) (ε t : ℝ) : ObjectProperty C

Generators of the provisional owner cut Q(≤t).

Equations

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

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtGen (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) (ε t : ℝ) : ObjectProperty C

Generators of the provisional owner cut Q(<t).

Equations

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

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred (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) (ε t : ℝ) : ObjectProperty C

The provisional owner cut Q(>t).

Equations

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

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred (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) (ε t : ℝ) : ObjectProperty C

The provisional owner cut Q(≤t).

Equations

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

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred (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) (ε t : ℝ) : ObjectProperty C

The provisional owner cut Q(<t).

Equations

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

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_mono (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) {ε t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) : deformedLePred C σ W hr0 hr1 hW ε t₁ ≤ deformedLePred C σ W hr0 hr1 hW ε t₂

Provisional Q(≤t) is monotone in the cutoff.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred_mono (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) {ε t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) : deformedLtPred C σ W hr0 hr1 hW ε t₁ ≤ deformedLtPred C σ W hr0 hr1 hW ε t₂

Provisional Q(<t) is monotone in the cutoff.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_of_deformedLtPred (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) {ε t : ℝ} : deformedLtPred C σ W hr0 hr1 hW ε t ≤ deformedLePred C σ W hr0 hr1 hW ε t

Every provisional Q(<t) object belongs to Q(≤t).

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_anti (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) {ε t₁ t₂ : ℝ} (ht : t₁ ≤ t₂) : deformedGtPred C σ W hr0 hr1 hW ε t₂ ≤ deformedGtPred C σ W hr0 hr1 hW ε t₁

Provisional Q(>t) is antitone in the cutoff.