The surface charge family and its wall equation

The compressed charge and family are owned upstream by CentralCharge/. This module identifies their determinant-alignment locus with the established surface wall polynomial.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.stChargeFamily_alignmentValue (p : ℝ × ℝ) (v w : NumClass) : stChargeFamily.alignmentValue p v w = wallExpr p.1 p.2 v w

The generic determinant specializes exactly to the surface wall expression.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.mem_stChargeFamily_alignmentLocus (p : ℝ × ℝ) (v w : NumClass) : p ∈ stChargeFamily.alignmentLocus v w ↔ wallExpr p.1 p.2 v w = 0

The generic alignment wall is the zero locus of the surface wall expression.