Wall equations on orthogonal divisorial charge slices

The orthogonal slice, its charge family, and its real and imaginary formulas live upstream under CentralCharge/Divisorial/. This file adds exactly the determinant-alignment locus and its formula.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.alignmentLocus {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (ch : ChernCharacter N D) (v w : N) : Set (Point U)

The numerical determinant-alignment alignmentLocus of two classes in an orthogonal divisor slice.

Equations

• T.alignmentLocus ch v w = (T.chargeFamily ch).alignmentLocus v w

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.alignmentValue_eq {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (ch : ChernCharacter N D) (p : Point U) (v w : N) : (T.chargeFamily ch).alignmentValue p v w = T.reFormula ch p v * T.imFormula ch p w - T.imFormula ch p v * T.reFormula ch p w

The universal determinant equation evaluated using the two divisorial slice formulas.