Plane geometry of the phase tilt

This file owns the coordinate facts underlying the tilt of a weak stability condition: clockwise rotation through pi * beta as an additive endomorphism, the rotated charge, the closed weak upper half plane and its closure and rigidity properties, the scalar cross product, and the resulting strict slope comparisons from strict separation of old slicing phases.

WeakUpperClosed, cross, and the four lemmas exported alongside them are the shared vocabulary of the rest of Semistable; the helpers used only here stay private.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltRotation (beta : ℝ) : ℂ →+ ℂ

Clockwise rotation through pi * beta, as an additive endomorphism of the complex plane.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltRotation_apply (beta : ℝ) (z : ℂ) : (phaseTiltRotation beta) z = z * Complex.exp (-(↑Real.pi * ↑beta) * Complex.I)

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltCharge {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (beta : ℝ) : K₀ C →+ ℂ

The central charge rotated clockwise through the phase cutoff.

Equations

• sigma.phaseTiltCharge beta = (CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltRotation beta).comp (sigma.Z.comp v)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltCharge_apply {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) (beta : ℝ) (E : C) : (sigma.phaseTiltCharge beta) (K₀.of C E) = sigma.Z (v (K₀.of C E)) * Complex.exp (-(↑Real.pi * ↑beta) * Complex.I)

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.WeakUpperClosed (z : ℂ) : Prop

The closed weak upper half plane: nonnegative imaginary part, and on the real axis only the nonpositive reals. This is the region in which the charge of an object of a tilted heart is constrained to lie.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.WeakUpperClosed z = (0 ≤ z.im ∧ (z.im = 0 → z.re ≤ 0))

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakUpperClosed_zero : WeakUpperClosed 0

Zero lies in the closed weak upper half plane.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakUpperClosed_sum {I : Type u_3} [Fintype I] (f : I → ℂ) (hf : ∀ (i : I), WeakUpperClosed (f i)) : WeakUpperClosed (∑ i : I, f i)

The closed weak upper half plane is closed under finite sums.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.weakUpperClosed_eq_zero_of_sum_eq_zero {I : Type u_3} [Fintype I] (f : I → ℂ) (hf : ∀ (i : I), WeakUpperClosed (f i)) (hsum : ∑ i : I, f i = 0) (i : I) : f i = 0

If a finite family in the closed weak upper half plane sums to zero, every member is zero. This is the rigidity used to detect zero-charge factors.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.rotatedRay_weakUpperClosed {beta phi m : ℝ} (hm : 0 ≤ m) (hphi : phi ∈ Set.Ioc beta (beta + 1)) : WeakUpperClosed (↑m * Complex.exp (↑(Real.pi * phi) * Complex.I) * Complex.exp (-(↑Real.pi * ↑beta) * Complex.I))

A ray of nonnegative length at a phase in the tilted window lies in the closed weak upper half plane after the clockwise rotation through pi * beta.

def CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.cross (z w : ℂ) : ℝ

The scalar cross product of two complex numbers, read as plane vectors. Its sign compares the arguments of z and w.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.cross z w = z.re * w.im - z.im * w.re

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTiltCharge_im_pos_of_phaseTors {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {beta : ℝ} (hbeta0 : 0 < beta) {E : C} (hE : phaseTors sigma.slicing beta E) (hcharge : (phaseTiltRotation beta) (sigma.weakStabilityFunctionOnHeart.charge E) ≠ 0) : 0 < ((phaseTiltRotation beta) (sigma.weakStabilityFunctionOnHeart.charge E)).im

A nonzero charged torsion-class object lies in the open upper half-plane after a nontrivial phase rotation.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTilt_slope_lt_of_phase_separated {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {beta : ℝ} {tTilt : TStructure C} (W : WeakStabilityFunction tTilt) {A B : C} (hAheart : (Slicing.toTStructure C sigma.slicing).heart A) (hBheart : (Slicing.toTStructure C sigma.slicing).heart B) (hAtilt : tTilt.heart A) (hBtilt : tTilt.heart B) (hWA : W.charge A = (phaseTiltRotation beta) (sigma.weakStabilityFunctionOnHeart.charge A)) (hWB : W.charge B = (phaseTiltRotation beta) (sigma.weakStabilityFunctionOnHeart.charge B)) (hA0 : ¬Limits.IsZero A) (hB0 : ¬Limits.IsZero B) (hsep : Slicing.phiPlus C sigma.slicing A hA0 < Slicing.phiMinus C sigma.slicing B hB0) (hAplus : Slicing.phiPlus C sigma.slicing A hA0 < 1) (hBcharge : sigma.weakStabilityFunctionOnHeart.charge B ≠ 0) : W.slope A < W.slope B

Strict phase separation below phase 1 gives strict slope separation after rotation.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTilt_slope_shift_lt_shift_of_phase_separated {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {beta : ℝ} {tTilt : TStructure C} (W : WeakStabilityFunction tTilt) {A B : C} (hAheart : (Slicing.toTStructure C sigma.slicing).heart A) (hBheart : (Slicing.toTStructure C sigma.slicing).heart B) (hAtilt : tTilt.heart ((shiftFunctor C 1).obj A)) (hBtilt : tTilt.heart ((shiftFunctor C 1).obj B)) (hWA : W.charge ((shiftFunctor C 1).obj A) = (phaseTiltRotation beta) (-sigma.weakStabilityFunctionOnHeart.charge A)) (hWB : W.charge ((shiftFunctor C 1).obj B) = (phaseTiltRotation beta) (-sigma.weakStabilityFunctionOnHeart.charge B)) (hA0 : ¬Limits.IsZero A) (hB0 : ¬Limits.IsZero B) (hsep : Slicing.phiPlus C sigma.slicing A hA0 < Slicing.phiMinus C sigma.slicing B hB0) (hAplus : Slicing.phiPlus C sigma.slicing A hA0 < 1) (hBcharge : sigma.weakStabilityFunctionOnHeart.charge B ≠ 0) : W.slope ((shiftFunctor C 1).obj A) < W.slope ((shiftFunctor C 1).obj B)

The shifted version of strict phase/slope separation. This public form is used by the H⁻¹ quotient induction for the weak upper tilt.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.WeakPreStabilityCondition.phaseTilt_slope_unshifted_lt_shifted_of_phase_separated {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u_2} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : WeakPreStabilityCondition v) {beta : ℝ} {tTilt : TStructure C} (W : WeakStabilityFunction tTilt) {U V : C} (hUheart : (Slicing.toTStructure C sigma.slicing).heart U) (hVheart : (Slicing.toTStructure C sigma.slicing).heart V) (hUshiftTilt : tTilt.heart ((shiftFunctor C 1).obj U)) (hVtilt : tTilt.heart V) (hWU : W.charge ((shiftFunctor C 1).obj U) = (phaseTiltRotation beta) (-sigma.weakStabilityFunctionOnHeart.charge U)) (hWV : W.charge V = (phaseTiltRotation beta) (sigma.weakStabilityFunctionOnHeart.charge V)) (hU0 : ¬Limits.IsZero U) (hV0 : ¬Limits.IsZero V) (hsep : Slicing.phiPlus C sigma.slicing U hU0 < Slicing.phiMinus C sigma.slicing V hV0) (hUplus : Slicing.phiPlus C sigma.slicing U hU0 < 1) (hVcharge : sigma.weakStabilityFunctionOnHeart.charge V ≠ 0) : W.slope V < W.slope ((shiftFunctor C 1).obj U)

A higher-phase unshifted factor has smaller tilted slope than the shift of a lower-phase factor.