14.14. Deformation: PhaseArithmetic🔗

14.14.1. wPhaseOf_Z_eq🔗

Coarse phase perturbation bound. If E is \sigma-semistable of phase \phi \in (\alpha - 1, \alpha + 1], then \operatorname{wPhaseOf}(Z(E), \alpha) = \phi.

Proof: From compatibility, Z(E) = m \cdot e^{i\pi\phi} with m > 0. Apply wPhaseOf_of_exp.

theorem

CategoryTheory.Triangulated.wPhaseOf_Z_eq.{v, u, u'} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) {α : ℝ}
  (hφ : φ ∈ Set.Ioc (α - 1) (α + 1)) :
  CategoryTheory.Triangulated.wPhaseOf (σ.charge E) α = φ
CategoryTheory.Triangulated.wPhaseOf_Z_eq.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  {α : ℝ}
  (hφ : φ ∈ Set.Ioc (α - 1) (α + 1)) :
  CategoryTheory.Triangulated.wPhaseOf
      (σ.charge E) α =
    φ

Something wrong, better idea? Suggest a change

14.14.2. wPhaseOf_perturbation🔗

Phase perturbation for \sigma-semistable objects. If E is \sigma-semistable of phase \phi \in (\alpha - 1/2, \alpha + 1/2) and \|(W-Z)(E)\| / \|Z(E)\| < \sin(\pi\varepsilon) with 0 < \varepsilon \le 1/2, then |\operatorname{wPhaseOf}(W(E), \alpha) - \phi| < \varepsilon.

Proof: Write W(E) = Z(E) + \delta = m \cdot e^{i\pi\phi}(1 + u) where u = \delta / Z(E). The bound \|u\| < \sin(\pi\varepsilon) follows from the seminorm estimate. Apply wPhaseOf_perturbation_generic.

theorem

CategoryTheory.Triangulated.wPhaseOf_perturbation.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E) (W : Λ →+ ℂ) {α ε : ℝ}
  (hφα : φ ∈ Set.Ioo (α - 1 / 2) (α + 1 / 2)) (hε : 0 < ε)
  (hε2 : ε ≤ 1 / 2)
  (hbd :
    ‖(W - σ.Z) (CategoryTheory.Triangulated.cl C v E)‖ <
      Real.sin (Real.pi * ε) * ‖σ.charge E‖) :
  |CategoryTheory.Triangulated.wPhaseOf
          (W (CategoryTheory.Triangulated.cl C v E)) α -
        φ| <
    ε
CategoryTheory.Triangulated.wPhaseOf_perturbation.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C} {φ : ℝ} (hP : σ.slicing.P φ E)
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (W : Λ →+ ℂ) {α ε : ℝ}
  (hφα :
    φ ∈ Set.Ioo (α - 1 / 2) (α + 1 / 2))
  (hε : 0 < ε) (hε2 : ε ≤ 1 / 2)
  (hbd :
    ‖(W - σ.Z)
          (CategoryTheory.Triangulated.cl
            C v E)‖ <
      Real.sin (Real.pi * ε) *
        ‖σ.charge E‖) :
  |CategoryTheory.Triangulated.wPhaseOf
          (W
            (CategoryTheory.Triangulated.cl
              C v E))
          α -
        φ| <
    ε

Something wrong, better idea? Suggest a change

14.14.3. hperturb_of_stabSeminorm🔗

Phase perturbation from stabSeminorm. If \|W - Z\|_\sigma < \sin(\pi\varepsilon_0) and b - a < 1, then for every nonzero \sigma-semistable F with phase \phi \in (a, b), the W-phase satisfies |\operatorname{wPhaseOf}(W(F), (a+b)/2) - \phi| < \varepsilon_0.

Proof: The stabSeminorm bound gives \|(W-Z)(F)\| \le M \|Z(F)\| with M < \sin(\pi\varepsilon_0). Since \phi \in (a, b) and b - a < 1, we have \phi \in ((a+b)/2 - 1/2, (a+b)/2 + 1/2). Apply wPhaseOf_perturbation.

theorem

CategoryTheory.Triangulated.hperturb_of_stabSeminorm.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b : ℝ} (hthin : b - a < 1) {ε₀ : ℝ} (hε₀ : 0 < ε₀)
  (hε₀2 : ε₀ < 1 / 4)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm C σ (W - σ.Z) <
      ENNReal.ofReal (Real.sin (Real.pi * ε₀)))
  (F : C) (φ : ℝ) :
  σ.slicing.P φ F →
    ¬CategoryTheory.Limits.IsZero F →
      a < φ →
        φ < b →
          φ - ε₀ <
              CategoryTheory.Triangulated.wPhaseOf
                (W (CategoryTheory.Triangulated.cl C v F))
                ((a + b) / 2) ∧
            CategoryTheory.Triangulated.wPhaseOf
                (W (CategoryTheory.Triangulated.cl C v F))
                ((a + b) / 2) <
              φ + ε₀
CategoryTheory.Triangulated.hperturb_of_stabSeminorm.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  (W : Λ →+ ℂ)
  (hW :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal 1)
  {a b : ℝ} (hthin : b - a < 1) {ε₀ : ℝ}
  (hε₀ : 0 < ε₀) (hε₀2 : ε₀ < 1 / 4)
  (hsin :
    CategoryTheory.Triangulated.stabSeminorm
        C σ (W - σ.Z) <
      ENNReal.ofReal
        (Real.sin (Real.pi * ε₀)))
  (F : C) (φ : ℝ) :
  σ.slicing.P φ F →
    ¬CategoryTheory.Limits.IsZero F →
      a < φ →
        φ < b →
          φ - ε₀ <
              CategoryTheory.Triangulated.wPhaseOf
                (W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                ((a + b) / 2) ∧
            CategoryTheory.Triangulated.wPhaseOf
                (W
                  (CategoryTheory.Triangulated.cl
                    C v F))
                ((a + b) / 2) <
              φ + ε₀

Something wrong, better idea? Suggest a change

14.14.4. mem_upperHalfPlaneUnion_of_arg_pos🔗

A nonzero complex number z with \arg(z) > 0 lies in the upper half-plane union \{z : \mathrm{Im}(z) > 0\} \cup \{z : \mathrm{Im}(z) = 0,\, \mathrm{Re}(z) > 0\}. This is the entry point connecting the argument condition to upper half-plane membership used in the W-phase comparison lemmas.

Proof: The proof splits on whether \mathrm{Im}(z) > 0 (then z is in the open upper half-plane) or \mathrm{Im}(z) \le 0. In the latter case, non-negativity of \arg(z) forces \mathrm{Im}(z) = 0, and the assumption \arg(z) > 0 then rules out \mathrm{Re}(z) \le 0 via Complex.arg_eq_zero_iff.

theorem

CategoryTheory.Triangulated.mem_upperHalfPlaneUnion_of_arg_pos {z : ℂ}
  (h : 0 < z.arg) : z ∈ CategoryTheory.upperHalfPlaneUnion
CategoryTheory.Triangulated.mem_upperHalfPlaneUnion_of_arg_pos
  {z : ℂ} (h : 0 < z.arg) :
  z ∈ CategoryTheory.upperHalfPlaneUnion

Something wrong, better idea? Suggest a change

14.14.5. wPhaseOf_gt_of_mem_upperHalfPlaneUnion🔗

If w \cdot e^{-i\pi\psi} lies in the upper half-plane union, then \psi < \mathrm{wPhaseOf}(w, \psi). Together with mem_upperHalfPlaneUnion_of_wPhaseOf_gt, this gives an equivalence between upper half-plane membership of the rotated vector and \mathrm{wPhaseOf}(w, \psi) > \psi.

Proof: The proof extracts \arg(w \cdot e^{-i\pi\psi}) > 0 from the upper half-plane union membership via arg_pos_of_mem_upperHalfPlaneUnion, then converts to \mathrm{wPhaseOf} > \psi by dividing by \pi > 0 and unfolding the definition.

theorem

CategoryTheory.Triangulated.wPhaseOf_gt_of_mem_upperHalfPlaneUnion
  {w : ℂ} {ψ : ℝ}
  (h :
    w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I)) ∈
      CategoryTheory.upperHalfPlaneUnion) :
  ψ < CategoryTheory.Triangulated.wPhaseOf w ψ
CategoryTheory.Triangulated.wPhaseOf_gt_of_mem_upperHalfPlaneUnion
  {w : ℂ} {ψ : ℝ}
  (h :
    w *
        Complex.exp
          (-(↑(Real.pi * ψ) *
              Complex.I)) ∈
      CategoryTheory.upperHalfPlaneUnion) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf w
      ψ

Something wrong, better idea? Suggest a change

14.14.6. mem_upperHalfPlaneUnion_of_wPhaseOf_gt🔗

If \psi < \mathrm{wPhaseOf}(w, \psi), then w \cdot e^{-i\pi\psi} lies in the upper half-plane union. This is the converse of wPhaseOf_gt_of_mem_upperHalfPlaneUnion: the W-phase comparison is equivalent to upper half-plane membership of the rotated vector.

Proof: The proof unfolds the definition of \mathrm{wPhaseOf} to read off that \arg(w \cdot e^{-i\pi\psi})/\pi > 0, and then applies mem_upperHalfPlaneUnion_of_arg_pos.

theorem

CategoryTheory.Triangulated.mem_upperHalfPlaneUnion_of_wPhaseOf_gt
  {w : ℂ} {ψ : ℝ} (h : ψ < CategoryTheory.Triangulated.wPhaseOf w ψ) :
  w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I)) ∈
    CategoryTheory.upperHalfPlaneUnion
CategoryTheory.Triangulated.mem_upperHalfPlaneUnion_of_wPhaseOf_gt
  {w : ℂ} {ψ : ℝ}
  (h :
    ψ <
      CategoryTheory.Triangulated.wPhaseOf
        w ψ) :
  w *
      Complex.exp
        (-(↑(Real.pi * ψ) * Complex.I)) ∈
    CategoryTheory.upperHalfPlaneUnion

Something wrong, better idea? Suggest a change

14.14.7. wPhaseOf_sum_gt🔗

W-phase lower bound for sums. If complex numbers w_1, \ldots, w_n all have \operatorname{wPhaseOf}(w_j, \psi) > \psi, then their sum satisfies \operatorname{wPhaseOf}(\sum w_j, \psi) > \psi.

Proof: Rotate by e^{-i\pi\psi}: each w_j \cdot e^{-i\pi\psi} lies in the upper half-plane (since phase > \psi). The upper half-plane is closed under addition, so the sum lies there too, giving phase > \psi.

theorem

CategoryTheory.Triangulated.wPhaseOf_sum_gt.{u_1} {ι : Type u_1}
  {s : Finset ι} (hs : s.Nonempty) {f : ι → ℂ} {ψ : ℝ}
  (hf_phase :
    ∀ i ∈ s, ψ < CategoryTheory.Triangulated.wPhaseOf (f i) ψ) :
  ψ < CategoryTheory.Triangulated.wPhaseOf (∑ i ∈ s, f i) ψ
CategoryTheory.Triangulated.wPhaseOf_sum_gt.{u_1}
  {ι : Type u_1} {s : Finset ι}
  (hs : s.Nonempty) {f : ι → ℂ} {ψ : ℝ}
  (hf_phase :
    ∀ i ∈ s,
      ψ <
        CategoryTheory.Triangulated.wPhaseOf
          (f i) ψ) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      (∑ i ∈ s, f i) ψ

Something wrong, better idea? Suggest a change

14.14.8. im_pos_of_phase_above🔗

If w = m \cdot e^{i\pi\phi} with m > 0 and \phi \in (\psi, \psi + 1), then \operatorname{Im}(w \cdot e^{-i\pi\psi}) > 0.

Proof: After rotation, \operatorname{Im} = m \sin(\pi(\phi - \psi)), and \sin > 0 on (0, \pi).

theorem

CategoryTheory.Triangulated.im_pos_of_phase_above {w : ℂ} {m φ ψ : ℝ}
  (hm : 0 < m) (hw : w = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I))
  (hlo : ψ < φ) (hhi : φ < ψ + 1) :
  0 < (w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im
CategoryTheory.Triangulated.im_pos_of_phase_above
  {w : ℂ} {m φ ψ : ℝ} (hm : 0 < m)
  (hw :
    w =
      ↑m *
        Complex.exp
          (↑(Real.pi * φ) * Complex.I))
  (hlo : ψ < φ) (hhi : φ < ψ + 1) :
  0 <
    (w *
        Complex.exp
          (-(↑(Real.pi * ψ) *
              Complex.I))).im

Something wrong, better idea? Suggest a change

14.14.9. im_sum_pos_of_all_pos🔗

If each rotated vector f(i) \cdot e^{-i\pi\psi} has strictly positive imaginary part, then so does the sum \bigl(\sum_{i\in s} f(i)\bigr)\cdot e^{-i\pi\psi}. This is used to propagate phase-above bounds through K_0 decompositions.

Proof: The proof rewrites the imaginary part of the product-sum as a sum of imaginary parts (using additivity of \mathrm{Im}) and then applies Finset.sum_pos to conclude from the pointwise positivity hypothesis.

theorem

CategoryTheory.Triangulated.im_sum_pos_of_all_pos.{u_1} {ι : Type u_1}
  {s : Finset ι} (hs : s.Nonempty) {f : ι → ℂ} {ψ : ℝ}
  (hf :
    ∀ i ∈ s,
      0 < (f i * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im) :
  0 < (∑ i ∈ s, f i * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im
CategoryTheory.Triangulated.im_sum_pos_of_all_pos.{u_1}
  {ι : Type u_1} {s : Finset ι}
  (hs : s.Nonempty) {f : ι → ℂ} {ψ : ℝ}
  (hf :
    ∀ i ∈ s,
      0 <
        (f i *
            Complex.exp
              (-(↑(Real.pi * ψ) *
                  Complex.I))).im) :
  0 <
    (∑ i ∈ s,
        f i *
          Complex.exp
            (-(↑(Real.pi * ψ) *
                Complex.I))).im

Something wrong, better idea? Suggest a change

14.14.10. wPhaseOf_gt_of_im_pos🔗

If \mathrm{Im}(w \cdot e^{-i\pi\psi}) > 0 and \mathrm{wPhaseOf}(w, \alpha) \in (\psi - 1, \psi + 1), then \mathrm{wPhaseOf}(w, \alpha) > \psi. The range hypothesis rules out the aliased branch where \sin > 0 could arise from a phase difference in (-2, -1).

Proof: Assume for contradiction \mathrm{wPhaseOf}(w,\alpha) \le \psi. Combined with the range hypothesis, the phase difference \mathrm{wPhaseOf}(w,\alpha) - \psi \in (-1, 0]. The polar compatibility identity gives \mathrm{Im}(w \cdot e^{-i\pi\psi}) = \|w\| \cdot \sin(\pi(\mathrm{wPhaseOf} - \psi)), and \sin \le 0 on (-\pi, 0] yields a non-positive imaginary part, contradicting the hypothesis.

theorem

CategoryTheory.Triangulated.wPhaseOf_gt_of_im_pos {w : ℂ} {α ψ : ℝ}
  (him : 0 < (w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im)
  (hrange :
    CategoryTheory.Triangulated.wPhaseOf w α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  ψ < CategoryTheory.Triangulated.wPhaseOf w α
CategoryTheory.Triangulated.wPhaseOf_gt_of_im_pos
  {w : ℂ} {α ψ : ℝ}
  (him :
    0 <
      (w *
          Complex.exp
            (-(↑(Real.pi * ψ) *
                Complex.I))).im)
  (hrange :
    CategoryTheory.Triangulated.wPhaseOf w
        α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf w
      α

Something wrong, better idea? Suggest a change

14.14.11. im_neg_of_phase_below🔗

If w = m \cdot e^{i\pi\phi} with m > 0 and \phi \in (\psi - 1, \psi), then \operatorname{Im}(w \cdot e^{-i\pi\psi}) < 0. Dual of im_pos_of_phase_above.

Proof: After rotation, \operatorname{Im} = m \sin(\pi(\phi - \psi)), and \sin < 0 on (-\pi, 0).

theorem

CategoryTheory.Triangulated.im_neg_of_phase_below {w : ℂ} {m φ ψ : ℝ}
  (hm : 0 < m) (hw : w = ↑m * Complex.exp (↑(Real.pi * φ) * Complex.I))
  (hlo : ψ - 1 < φ) (hhi : φ < ψ) :
  (w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im < 0
CategoryTheory.Triangulated.im_neg_of_phase_below
  {w : ℂ} {m φ ψ : ℝ} (hm : 0 < m)
  (hw :
    w =
      ↑m *
        Complex.exp
          (↑(Real.pi * φ) * Complex.I))
  (hlo : ψ - 1 < φ) (hhi : φ < ψ) :
  (w *
        Complex.exp
          (-(↑(Real.pi * ψ) *
              Complex.I))).im <
    0

Something wrong, better idea? Suggest a change

14.14.12. im_sum_neg_of_all_neg🔗

If each rotated vector f(i) \cdot e^{-i\pi\psi} has strictly negative imaginary part, then so does the sum \bigl(\sum_{i\in s} f(i)\bigr)\cdot e^{-i\pi\psi}. This is the dual of im_sum_pos_of_all_pos and is used to propagate phase-below bounds through K_0 decompositions.

Proof: The proof rewrites the imaginary part of the product-sum as a sum of imaginary parts (using additivity of \mathrm{Im}) and then applies Finset.sum_neg to conclude from the pointwise negativity hypothesis.

theorem

CategoryTheory.Triangulated.im_sum_neg_of_all_neg.{u_1} {ι : Type u_1}
  {s : Finset ι} (hs : s.Nonempty) {f : ι → ℂ} {ψ : ℝ}
  (hf :
    ∀ i ∈ s,
      (f i * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im < 0) :
  (∑ i ∈ s, f i * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im < 0
CategoryTheory.Triangulated.im_sum_neg_of_all_neg.{u_1}
  {ι : Type u_1} {s : Finset ι}
  (hs : s.Nonempty) {f : ι → ℂ} {ψ : ℝ}
  (hf :
    ∀ i ∈ s,
      (f i *
            Complex.exp
              (-(↑(Real.pi * ψ) *
                  Complex.I))).im <
        0) :
  (∑ i ∈ s,
        f i *
          Complex.exp
            (-(↑(Real.pi * ψ) *
                Complex.I))).im <
    0

Something wrong, better idea? Suggest a change

14.14.13. wPhaseOf_lt_of_im_neg🔗

If \mathrm{Im}(w \cdot e^{-i\pi\psi}) < 0 and \mathrm{wPhaseOf}(w, \alpha) \in (\psi - 1, \psi + 1), then \mathrm{wPhaseOf}(w, \alpha) < \psi. This is the dual of wPhaseOf_gt_of_im_pos.

Proof: Assume for contradiction \psi \le \mathrm{wPhaseOf}(w,\alpha). Combined with the range hypothesis, the phase difference lies in [0, 1) so \sin(\pi(\mathrm{wPhaseOf} - \psi)) \ge 0. The polar compatibility identity then gives \mathrm{Im}(w \cdot e^{-i\pi\psi}) = \|w\| \cdot \sin(\ldots) \ge 0, contradicting the hypothesis.

theorem

CategoryTheory.Triangulated.wPhaseOf_lt_of_im_neg {w : ℂ} {α ψ : ℝ}
  (him : (w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im < 0)
  (hrange :
    CategoryTheory.Triangulated.wPhaseOf w α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w α < ψ
CategoryTheory.Triangulated.wPhaseOf_lt_of_im_neg
  {w : ℂ} {α ψ : ℝ}
  (him :
    (w *
          Complex.exp
            (-(↑(Real.pi * ψ) *
                Complex.I))).im <
      0)
  (hrange :
    CategoryTheory.Triangulated.wPhaseOf w
        α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w
      α <
    ψ

Something wrong, better idea? Suggest a change

14.14.14. im_eq_zero_of_wPhaseOf_eq🔗

If \operatorname{wPhaseOf}(w, \alpha) = \psi, then \operatorname{Im}(w \cdot e^{-i\pi\psi}) = 0.

Proof: From the polar decomposition, w \cdot e^{-i\pi\psi} = \|w\|, which is real.

theorem

CategoryTheory.Triangulated.im_eq_zero_of_wPhaseOf_eq {w : ℂ} {α ψ : ℝ}
  (h : CategoryTheory.Triangulated.wPhaseOf w α = ψ) :
  (w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im = 0
CategoryTheory.Triangulated.im_eq_zero_of_wPhaseOf_eq
  {w : ℂ} {α ψ : ℝ}
  (h :
    CategoryTheory.Triangulated.wPhaseOf w
        α =
      ψ) :
  (w *
        Complex.exp
          (-(↑(Real.pi * ψ) *
              Complex.I))).im =
    0

Something wrong, better idea? Suggest a change

14.14.15. im_pos_of_sum_zero_and_neg🔗

If w_1 + w_2 = w and \operatorname{Im}(w \cdot e^{-i\pi\psi}) = 0 and \operatorname{Im}(w_2 \cdot e^{-i\pi\psi}) < 0, then \operatorname{Im}(w_1 \cdot e^{-i\pi\psi}) > 0.

Proof: Additivity of the imaginary part: \operatorname{Im}(w_1 \cdot r) = \operatorname{Im}(w \cdot r) - \operatorname{Im}(w_2 \cdot r) = 0 - (\text{negative}) > 0.

theorem

CategoryTheory.Triangulated.im_pos_of_sum_zero_and_neg {w₁ w₂ w : ℂ}
  {ψ : ℝ} (hsum : w₁ + w₂ = w)
  (hw : (w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im = 0)
  (h₂ : (w₂ * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im < 0) :
  0 < (w₁ * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im
CategoryTheory.Triangulated.im_pos_of_sum_zero_and_neg
  {w₁ w₂ w : ℂ} {ψ : ℝ}
  (hsum : w₁ + w₂ = w)
  (hw :
    (w *
          Complex.exp
            (-(↑(Real.pi * ψ) *
                Complex.I))).im =
      0)
  (h₂ :
    (w₂ *
          Complex.exp
            (-(↑(Real.pi * ψ) *
                Complex.I))).im <
      0) :
  0 <
    (w₁ *
        Complex.exp
          (-(↑(Real.pi * ψ) *
              Complex.I))).im

Something wrong, better idea? Suggest a change

14.14.16. im_mul_exp_neg_eq_norm_mul_sin🔗

Rotated imaginary part identity. For any w \in \mathbb{C} and \alpha, \psi \in \mathbb{R}, \operatorname{Im}(w \cdot e^{-i\pi\psi}) = \|w\| \cdot \sin(\pi(\operatorname{wPhaseOf}(w, \alpha) - \psi)).

Proof: Substitute the polar decomposition w = \|w\| \cdot e^{i\pi \cdot \operatorname{wPhaseOf}(w, \alpha)} and simplify.

theorem

CategoryTheory.Triangulated.im_mul_exp_neg_eq_norm_mul_sin (w : ℂ)
  (α ψ : ℝ) :
  (w * Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im =
    ‖w‖ *
      Real.sin
        (Real.pi * (CategoryTheory.Triangulated.wPhaseOf w α - ψ))
CategoryTheory.Triangulated.im_mul_exp_neg_eq_norm_mul_sin
  (w : ℂ) (α ψ : ℝ) :
  (w *
        Complex.exp
          (-(↑(Real.pi * ψ) *
              Complex.I))).im =
    ‖w‖ *
      Real.sin
        (Real.pi *
          (CategoryTheory.Triangulated.wPhaseOf
              w α -
            ψ))

Something wrong, better idea? Suggest a change

14.14.17. wPhaseOf_seesaw🔗

Phase see-saw. If w = w_1 + w_2 with \operatorname{wPhaseOf}(w, \alpha) = \psi, \operatorname{wPhaseOf}(w_1, \alpha) \in (\psi - 1, \psi], and w_2 \ne 0 with \operatorname{wPhaseOf}(w_2, \alpha) \in (\psi - 1, \psi + 1), then \operatorname{wPhaseOf}(w_2, \alpha) \ge \psi.

Proof: By the imaginary-part sign argument: \operatorname{Im}(w \cdot r) = 0 (phase = \psi), \operatorname{Im}(w_1 \cdot r) \le 0 (phase \le \psi). If \operatorname{wPhaseOf}(w_2) < \psi, then \operatorname{Im}(w_2 \cdot r) < 0, giving \operatorname{Im}(w \cdot r) < 0, a contradiction.

theorem

CategoryTheory.Triangulated.wPhaseOf_seesaw {w w₁ w₂ : ℂ} {α ψ : ℝ}
  (hsum : w₁ + w₂ = w)
  (hψ : CategoryTheory.Triangulated.wPhaseOf w α = ψ)
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf w₁ α ∈ Set.Ioc (ψ - 1) ψ)
  (hw₂_ne : w₂ ≠ 0)
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf w₂ α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  ψ ≤ CategoryTheory.Triangulated.wPhaseOf w₂ α
CategoryTheory.Triangulated.wPhaseOf_seesaw
  {w w₁ w₂ : ℂ} {α ψ : ℝ}
  (hsum : w₁ + w₂ = w)
  (hψ :
    CategoryTheory.Triangulated.wPhaseOf w
        α =
      ψ)
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₁ α ∈
      Set.Ioc (ψ - 1) ψ)
  (hw₂_ne : w₂ ≠ 0)
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₂ α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  ψ ≤
    CategoryTheory.Triangulated.wPhaseOf
      w₂ α

Something wrong, better idea? Suggest a change

14.14.18. wPhaseOf_seesaw_strict🔗

Strict phase see-saw. If w = w_1 + w_2 with \operatorname{wPhaseOf}(w, \alpha) = \psi, \operatorname{wPhaseOf}(w_2, \alpha) < \psi, w_2 \ne 0, and both summands in the branch window (\psi - 1, \psi + 1), then \operatorname{wPhaseOf}(w_1, \alpha) > \psi.

Proof: Dual of wPhaseOf_seesaw: \operatorname{Im}(w_2 \cdot r) < 0 forces \operatorname{Im}(w_1 \cdot r) > 0, hence phase > \psi.

theorem

CategoryTheory.Triangulated.wPhaseOf_seesaw_strict {w w₁ w₂ : ℂ}
  {α ψ : ℝ} (hsum : w₁ + w₂ = w)
  (hψ : CategoryTheory.Triangulated.wPhaseOf w α = ψ)
  (hw₂_lt : CategoryTheory.Triangulated.wPhaseOf w₂ α < ψ)
  (hw₂_ne : w₂ ≠ 0)
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf w₂ α ∈ Set.Ioo (ψ - 1) (ψ + 1))
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf w₁ α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  ψ < CategoryTheory.Triangulated.wPhaseOf w₁ α
CategoryTheory.Triangulated.wPhaseOf_seesaw_strict
  {w w₁ w₂ : ℂ} {α ψ : ℝ}
  (hsum : w₁ + w₂ = w)
  (hψ :
    CategoryTheory.Triangulated.wPhaseOf w
        α =
      ψ)
  (hw₂_lt :
    CategoryTheory.Triangulated.wPhaseOf
        w₂ α <
      ψ)
  (hw₂_ne : w₂ ≠ 0)
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₂ α ∈
      Set.Ioo (ψ - 1) (ψ + 1))
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₁ α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  ψ <
    CategoryTheory.Triangulated.wPhaseOf
      w₁ α

Something wrong, better idea? Suggest a change

14.14.19. wPhaseOf_seesaw_dual🔗

Dual strict phase see-saw. If w = w_1 + w_2 with \operatorname{wPhaseOf}(w, \alpha) = \psi and \operatorname{wPhaseOf}(w_1, \alpha) > \psi, then \operatorname{wPhaseOf}(w_2, \alpha) < \psi.

Proof: \operatorname{Im}(w_1 \cdot r) > 0 and \operatorname{Im}(w_2 \cdot r) \ge 0 would give \operatorname{Im}(w \cdot r) > 0, contradicting phase = \psi.

theorem

CategoryTheory.Triangulated.wPhaseOf_seesaw_dual {w w₁ w₂ : ℂ} {α ψ : ℝ}
  (hsum : w₁ + w₂ = w)
  (hψ : CategoryTheory.Triangulated.wPhaseOf w α = ψ)
  (hw₁_gt : ψ < CategoryTheory.Triangulated.wPhaseOf w₁ α)
  (hw₁_ne : w₁ ≠ 0)
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf w₁ α ∈ Set.Ioo (ψ - 1) (ψ + 1))
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf w₂ α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w₂ α < ψ
CategoryTheory.Triangulated.wPhaseOf_seesaw_dual
  {w w₁ w₂ : ℂ} {α ψ : ℝ}
  (hsum : w₁ + w₂ = w)
  (hψ :
    CategoryTheory.Triangulated.wPhaseOf w
        α =
      ψ)
  (hw₁_gt :
    ψ <
      CategoryTheory.Triangulated.wPhaseOf
        w₁ α)
  (hw₁_ne : w₁ ≠ 0)
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₁ α ∈
      Set.Ioo (ψ - 1) (ψ + 1))
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₂ α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w₂
      α <
    ψ

Something wrong, better idea? Suggest a change

14.14.20. wPhaseOf_lt_of_add_le_lt🔗

If w = w_1 + w_2 where \mathrm{wPhaseOf}(w_1, \alpha) \in (\psi - 1, \psi] and \mathrm{wPhaseOf}(w_2, \alpha) < \psi with w_2 \ne 0, and the total W-phase \mathrm{wPhaseOf}(w, \alpha) lies in (\psi - 1, \psi + 1), then \mathrm{wPhaseOf}(w, \alpha) < \psi. Both summands being sub-phase (with w_1 weakly so and w_2 strictly) forces the total phase to be strictly below \psi.

Proof: Rotating by e^{-i\pi\psi}: \mathrm{Im}(w_1 \cdot \mathrm{rot}) \le 0 (from the phase \le \psi constraint and the range), \mathrm{Im}(w_2 \cdot \mathrm{rot}) < 0 (from w_2 \ne 0 and strict phase < \psi), so \mathrm{Im}(w \cdot \mathrm{rot}) < 0 by additivity. Then wPhaseOf_lt_of_im_neg and the range hypothesis conclude.

theorem

CategoryTheory.Triangulated.wPhaseOf_lt_of_add_le_lt {w w₁ w₂ : ℂ}
  {α ψ : ℝ} (hsum : w₁ + w₂ = w)
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf w₁ α ∈ Set.Ioc (ψ - 1) ψ)
  (hw₂_lt : CategoryTheory.Triangulated.wPhaseOf w₂ α < ψ)
  (hw₂_ne : w₂ ≠ 0)
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf w₂ α ∈ Set.Ioo (ψ - 1) (ψ + 1))
  (hw_range :
    CategoryTheory.Triangulated.wPhaseOf w α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w α < ψ
CategoryTheory.Triangulated.wPhaseOf_lt_of_add_le_lt
  {w w₁ w₂ : ℂ} {α ψ : ℝ}
  (hsum : w₁ + w₂ = w)
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₁ α ∈
      Set.Ioc (ψ - 1) ψ)
  (hw₂_lt :
    CategoryTheory.Triangulated.wPhaseOf
        w₂ α <
      ψ)
  (hw₂_ne : w₂ ≠ 0)
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₂ α ∈
      Set.Ioo (ψ - 1) (ψ + 1))
  (hw_range :
    CategoryTheory.Triangulated.wPhaseOf w
        α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w
      α <
    ψ

Something wrong, better idea? Suggest a change

14.14.21. wPhaseOf_lt_of_add_le_gt🔗

If w = w_1 + w_2, the total W-phase \mathrm{wPhaseOf}(w, \alpha) \le \psi, one summand satisfies \mathrm{wPhaseOf}(w_1, \alpha) > \psi (with w_1 \ne 0 and both summands in the branch window (\psi - 1, \psi + 1)), then the other summand satisfies \mathrm{wPhaseOf}(w_2, \alpha) < \psi. This is the one-sided source-envelope phase seesaw: a super-phase summand forces the complementary summand to be sub-phase.

Proof: Rotating by e^{-i\pi\psi}: \mathrm{Im}(w \cdot \mathrm{rot}) \le 0 (from the phase \le \psi condition and the range hypothesis), \mathrm{Im}(w_1 \cdot \mathrm{rot}) > 0 (from w_1 \ne 0 and phase > \psi), so by additivity of \mathrm{Im} we get \mathrm{Im}(w_2 \cdot \mathrm{rot}) < 0. Then wPhaseOf_lt_of_im_neg concludes.

theorem

CategoryTheory.Triangulated.wPhaseOf_lt_of_add_le_gt {w w₁ w₂ : ℂ}
  {α ψ : ℝ} (hsum : w₁ + w₂ = w)
  (hw_le : CategoryTheory.Triangulated.wPhaseOf w α ≤ ψ)
  (hw_range :
    CategoryTheory.Triangulated.wPhaseOf w α ∈ Set.Ioo (ψ - 1) (ψ + 1))
  (hw₁_gt : ψ < CategoryTheory.Triangulated.wPhaseOf w₁ α)
  (hw₁_ne : w₁ ≠ 0)
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf w₁ α ∈ Set.Ioo (ψ - 1) (ψ + 1))
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf w₂ α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w₂ α < ψ
CategoryTheory.Triangulated.wPhaseOf_lt_of_add_le_gt
  {w w₁ w₂ : ℂ} {α ψ : ℝ}
  (hsum : w₁ + w₂ = w)
  (hw_le :
    CategoryTheory.Triangulated.wPhaseOf w
        α ≤
      ψ)
  (hw_range :
    CategoryTheory.Triangulated.wPhaseOf w
        α ∈
      Set.Ioo (ψ - 1) (ψ + 1))
  (hw₁_gt :
    ψ <
      CategoryTheory.Triangulated.wPhaseOf
        w₁ α)
  (hw₁_ne : w₁ ≠ 0)
  (hw₁_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₁ α ∈
      Set.Ioo (ψ - 1) (ψ + 1))
  (hw₂_range :
    CategoryTheory.Triangulated.wPhaseOf
        w₂ α ∈
      Set.Ioo (ψ - 1) (ψ + 1)) :
  CategoryTheory.Triangulated.wPhaseOf w₂
      α <
    ψ

Something wrong, better idea? Suggest a change

14.14.22. im_W_pos_of_intervalProp🔗

Im positivity from HN factors. If E \in \mathcal{P}((a, b)) is nonzero and every nonzero \sigma-semistable factor has \operatorname{Im}(W(F_j) \cdot e^{-i\pi\psi}) > 0, then \operatorname{Im}(W(E) \cdot e^{-i\pi\psi}) > 0.

Proof: Decompose W([E]) = \sum W([F_j]) via K_0 additivity. The imaginary part is additive, each term is positive, and the first nonzero factor gives strict positivity.

theorem

CategoryTheory.Triangulated.im_W_pos_of_intervalProp.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E) (W : Λ →+ ℂ)
  {ψ a b : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (him_pos :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              0 <
                (W (CategoryTheory.Triangulated.cl C v F) *
                    Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im) :
  0 <
    (W (CategoryTheory.Triangulated.cl C v E) *
        Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im
CategoryTheory.Triangulated.im_W_pos_of_intervalProp.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (W : Λ →+ ℂ) {ψ a b : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (him_pos :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              0 <
                (W
                      (CategoryTheory.Triangulated.cl
                        C v F) *
                    Complex.exp
                      (-(↑(Real.pi * ψ) *
                          Complex.I))).im) :
  0 <
    (W
          (CategoryTheory.Triangulated.cl
            C v E) *
        Complex.exp
          (-(↑(Real.pi * ψ) *
              Complex.I))).im

Something wrong, better idea? Suggest a change

14.14.23. im_W_neg_of_intervalProp🔗

Im negativity from HN factors. Dual of im_W_pos_of_intervalProp: if every factor has \operatorname{Im}(W(F_j) \cdot e^{-i\pi\psi}) < 0, then \operatorname{Im}(W(E) \cdot e^{-i\pi\psi}) < 0.

Proof: Negate and apply the same K_0 decomposition argument.

theorem

CategoryTheory.Triangulated.im_W_neg_of_intervalProp.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E) (W : Λ →+ ℂ)
  {ψ a b : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (him_neg :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              (W (CategoryTheory.Triangulated.cl C v F) *
                    Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im <
                0) :
  (W (CategoryTheory.Triangulated.cl C v E) *
        Complex.exp (-(↑(Real.pi * ψ) * Complex.I))).im <
    0
CategoryTheory.Triangulated.im_W_neg_of_intervalProp.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (W : Λ →+ ℂ) {ψ a b : ℝ}
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (him_neg :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              (W
                      (CategoryTheory.Triangulated.cl
                        C v F) *
                    Complex.exp
                      (-(↑(Real.pi * ψ) *
                          Complex.I))).im <
                0) :
  (W
          (CategoryTheory.Triangulated.cl
            C v E) *
        Complex.exp
          (-(↑(Real.pi * ψ) *
              Complex.I))).im <
    0

Something wrong, better idea? Suggest a change

14.14.24. wPhaseOf_gt_of_intervalProp🔗

W-phase lower bound for interval objects (Lemma 7.3(b)). If E \in \mathcal{P}((a, b)) is nonzero and every nonzero \sigma-semistable factor of phase \phi \in (a, b) has W-phase in (a - \varepsilon, a - \varepsilon + 1), then \operatorname{wPhaseOf}(W(E), \alpha) > a - \varepsilon.

Proof: Each factor has \operatorname{Im}(W(F) \cdot e^{-i\pi(a-\varepsilon)}) > 0 (from the phase window). By K_0 decomposition, \operatorname{Im}(W(E) \cdot e^{-i\pi(a-\varepsilon)}) > 0. A contrapositive sin-sign argument converts this to a phase lower bound.

theorem

CategoryTheory.Triangulated.wPhaseOf_gt_of_intervalProp.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E) (W : Λ →+ ℂ)
  {α a b ε : ℝ} (hα_ge : a - ε ≤ α)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (hW_ne :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ → φ < b → W (CategoryTheory.Triangulated.cl C v F) ≠ 0)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              a - ε <
                  CategoryTheory.Triangulated.wPhaseOf
                    (W (CategoryTheory.Triangulated.cl C v F)) α ∧
                CategoryTheory.Triangulated.wPhaseOf
                    (W (CategoryTheory.Triangulated.cl C v F)) α <
                  a - ε + 1) :
  a - ε <
    CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v E)) α
CategoryTheory.Triangulated.wPhaseOf_gt_of_intervalProp.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (W : Λ →+ ℂ) {α a b ε : ℝ}
  (hα_ge : a - ε ≤ α)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (hW_ne :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              W
                  (CategoryTheory.Triangulated.cl
                    C v F) ≠
                0)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              a - ε <
                  CategoryTheory.Triangulated.wPhaseOf
                    (W
                      (CategoryTheory.Triangulated.cl
                        C v F))
                    α ∧
                CategoryTheory.Triangulated.wPhaseOf
                    (W
                      (CategoryTheory.Triangulated.cl
                        C v F))
                    α <
                  a - ε + 1) :
  a - ε <
    CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v E))
      α

Something wrong, better idea? Suggest a change

14.14.25. wPhaseOf_lt_of_intervalProp🔗

W-phase upper bound for interval objects. Dual of wPhaseOf_gt_of_intervalProp: if every factor has W-phase in (b + \varepsilon - 1, b + \varepsilon), then \operatorname{wPhaseOf}(W(E), \alpha) < b + \varepsilon.

Proof: Each factor has \operatorname{Im}(W(F) \cdot e^{-i\pi(b+\varepsilon)}) < 0. By K_0 decomposition, \operatorname{Im}(W(E) \cdot e^{-i\pi(b+\varepsilon)}) < 0, giving the upper phase bound.

theorem

CategoryTheory.Triangulated.wPhaseOf_lt_of_intervalProp.{v, u, u'}
  (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v : CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ : CategoryTheory.Triangulated.StabilityCondition.WithClassMap C v)
  {E : C} (hE : ¬CategoryTheory.Limits.IsZero E) (W : Λ →+ ℂ)
  {α a b ε : ℝ} (hα_le : α ≤ b + ε)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp C σ.slicing a b E)
  (hW_ne :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ → φ < b → W (CategoryTheory.Triangulated.cl C v F) ≠ 0)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              b + ε - 1 <
                  CategoryTheory.Triangulated.wPhaseOf
                    (W (CategoryTheory.Triangulated.cl C v F)) α ∧
                CategoryTheory.Triangulated.wPhaseOf
                    (W (CategoryTheory.Triangulated.cl C v F)) α <
                  b + ε) :
  CategoryTheory.Triangulated.wPhaseOf
      (W (CategoryTheory.Triangulated.cl C v E)) α <
    b + ε
CategoryTheory.Triangulated.wPhaseOf_lt_of_intervalProp.{v,
    u, u'}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C]
  [CategoryTheory.IsTriangulated C]
  {Λ : Type u'} [AddCommGroup Λ]
  {v :
    CategoryTheory.Triangulated.K₀ C →+ Λ}
  (σ :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap
      C v)
  {E : C}
  (hE : ¬CategoryTheory.Limits.IsZero E)
  (W : Λ →+ ℂ) {α a b ε : ℝ}
  (hα_le : α ≤ b + ε)
  (hI :
    CategoryTheory.Triangulated.Slicing.intervalProp
      C σ.slicing a b E)
  (hW_ne :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              W
                  (CategoryTheory.Triangulated.cl
                    C v F) ≠
                0)
  (hperturb :
    ∀ (F : C) (φ : ℝ),
      σ.slicing.P φ F →
        ¬CategoryTheory.Limits.IsZero F →
          a < φ →
            φ < b →
              b + ε - 1 <
                  CategoryTheory.Triangulated.wPhaseOf
                    (W
                      (CategoryTheory.Triangulated.cl
                        C v F))
                    α ∧
                CategoryTheory.Triangulated.wPhaseOf
                    (W
                      (CategoryTheory.Triangulated.cl
                        C v F))
                    α <
                  b + ε) :
  CategoryTheory.Triangulated.wPhaseOf
      (W
        (CategoryTheory.Triangulated.cl C
          v E))
      α <
    b + ε

Something wrong, better idea? Suggest a change