Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Foundation.Deformation.RelativePhase

Relative phases of complex numbers #

The deformation construction must choose a real lift of the argument of a complex charge. relativePhase w α is the unique lift in (α - 1, α + 1]. Keeping this branch-control layer independent of categories makes the later stability-condition deformation API depend on an owner-controlled analytic primitive rather than the retained package.

source
noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase (w : ℂ) (α : ℝ) :
ℝ

The lift of the phase of w whose branch is centred at α.

Equations
Instances For
    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_mem_Ioc (w : ℂ) (α : ℝ) :
    relativePhase w α ∈ Set.Ioc (α - 1) (α + 1)

    The relative phase lies on its selected branch.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_polar (w : ℂ) (α : ℝ) :
    w = ↑‖w‖ * Complex.exp (↑(Real.pi * relativePhase w α) * Complex.I)

    Polar reconstruction using the selected relative phase.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_of_ray {m φ α : ℝ} (hm : 0 < m) (hφ : φ ∈ Set.Ioc (α - 1) (α + 1)) :
    relativePhase (↑m * Complex.exp (↑(Real.pi * φ) * Complex.I)) α = φ

    A positive point on a ray is recognized on every compatible branch.

    source
    @[simp]
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_zero (α : ℝ) :
    relativePhase 0 α = α
    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_neg {w : ℂ} (hw : w ≠ 0) (α : ℝ) :
    relativePhase (-w) (α + 1) = relativePhase w α + 1

    Negating a nonzero charge and moving the branch centre by one shifts its relative phase by one.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_add_two {w : ℂ} (hw : w ≠ 0) (α : ℝ) :
    relativePhase w (α + 2) = relativePhase w α + 2

    Moving the branch centre by a full period moves the phase by that period.

    source
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.relativePhase_eq_of_mem {w : ℂ} (hw : w ≠ 0) (α β : ℝ) (h : relativePhase w α ∈ Set.Ioc (β - 1) (β + 1)) :
    relativePhase w α = relativePhase w β

    Relative phase is independent of the branch centre once one chosen lift also lies on the other branch.