The exponential twist on compressed degrees

twist m β acts on HDeg m by convolution with (-β)^j / j!. Its group law and the identity charge m w (twist m β d) = charge m (w + β) d come from the same finite exponential convolution, over the reals and complexes respectively. The truncation degree is arbitrary and no geometric hypothesis is needed. Comparisons with tuple and geometric presentations live downstream.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.twist (m : ℕ) (β : ℝ) (d : HDeg m) : HDeg m

The truncated e^{-βH} action on the weighted H-degrees.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.twist_apply (m : ℕ) (β : ℝ) (d : HDeg m) (i : Fin (m + 1)) : twist m β d i = ∑ j : Fin (↑i + 1), (-β) ^ (↑i - ↑j) / ↑(↑i - ↑j).factorial * d ⟨↑j, ⋯⟩

The component formula, with the bound carried by the summation index.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.twist_twist (m : ℕ) (β γ : ℝ) (d : HDeg m) : twist m β (twist m γ d) = twist m (β + γ) d

The coefficientwise identity e^{-βH} e^{-γH} = e^{-(β+γ)H}. The finite Vandermonde convolution involves only lower degrees, so truncation does not discard any term needed by the group law.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.twist_zero (m : ℕ) (d : HDeg m) : twist m 0 d = d

The zero parameter acts as the identity.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Exp.charge_twist (m : ℕ) (w : ℂ) (β : ℝ) (d : HDeg m) : (charge m w) (twist m β d) = (charge m (w + ↑β)) d

The Cauchy product of the charge exponential and the real twist exponential. The parameter shifts by +β: both exponentials carry the same negative sign. This identity holds on the entire complex parameter plane.