Alignment and signed-ray loci of parameterized charge families

CentralCharge/Family.lean owns ChargeFamily, reindexing, pullback and postcomposition. This downstream file adds the determinant-alignment value and separates its zero locus from the positive-ray condition used to read equal phase.

For two classes v,w, their universal alignment equation is the determinant

Re Z(v) Im Z(w) - Im Z(v) Re Z(w) = 0.

The parameter type remains unconstrained. positiveRayLocus includes the nonvanishing and positive-sign data that the determinant equation alone omits. Actual destabilization still needs semistable objects and categorical existence data; none is asserted here.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v w : N) : ℝ

The universal numerical alignment expression for two classes.

Equations

• Z.alignmentValue p v w = Z.re p v * Z.im p w - Z.im p v * Z.re p w

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentLocus {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (v w : N) : Set P

The numerical alignment locus of two classes in the parameter space.

This is the determinant-zero locus where the two charges are real-linearly dependent. It is the whole parameter space when w is an integral multiple of v (alignmentLocus_self, alignmentLocus_add_zsmul_right) and wherever Z(v) = 0. It therefore does not by itself express equal phase or destabilization.

Equations

• Z.alignmentLocus v w = {p : P | Z.alignmentValue p v w = 0}

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.positiveRayLocus {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (v w : N) : Set P

The locus where two nonzero charges lie on the same positive real ray.

The explicit nonvanishing and positive scalar are the hypotheses omitted by the determinant alignment equation. This is the numerical equal-phase adapter; it still carries no semistable objects and is not an actual wall.

Equations

• Z.positiveRayLocus v w = {p : P | (Z.charge p) v ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ (Z.charge p) w = ↑r * (Z.charge p) v}

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.mem_alignmentLocus {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v w : N) : p ∈ Z.alignmentLocus v w ↔ Z.alignmentValue p v w = 0

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.mem_positiveRayLocus {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v w : N) : p ∈ Z.positiveRayLocus v w ↔ (Z.charge p) v ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ (Z.charge p) w = ↑r * (Z.charge p) v

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.positiveRayLocus_subset_alignmentLocus {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (v w : N) : Z.positiveRayLocus v w ⊆ Z.alignmentLocus v w

Positive-ray alignment implies determinant alignment. The converse needs the nonzero and sign conditions recorded by positiveRayLocus.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.zeroLocus_subset_alignmentLocus_left {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (v w : N) : Z.zeroLocus v ⊆ Z.alignmentLocus v w

Charge-zero parameters are automatically in every alignment locus with that class. This is exactly why alignment cannot by itself mean equal phase.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.zeroLocus_subset_alignmentLocus_right {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (v w : N) : Z.zeroLocus w ⊆ Z.alignmentLocus v w

The same containment for a zero charge in the second class.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_eq_neg_im_mul_conj {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v w : N) : Z.alignmentValue p v w = -((Z.charge p) v * (starRingEnd ℂ) ((Z.charge p) w)).im

The determinant alignment expression is the negative imaginary part of Z(v) * conj (Z(w)).

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_self {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v : N) : Z.alignmentValue p v v = 0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentLocus_self {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (v : N) : Z.alignmentLocus v v = Set.univ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_swap {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v w : N) : Z.alignmentValue p w v = -Z.alignmentValue p v w

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentLocus_swap {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (v w : N) : Z.alignmentLocus w v = Z.alignmentLocus v w

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_zero_left {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (w : N) : Z.alignmentValue p 0 w = 0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_zero_right {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v : N) : Z.alignmentValue p v 0 = 0

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_add_left {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v₁ v₂ w : N) : Z.alignmentValue p (v₁ + v₂) w = Z.alignmentValue p v₁ w + Z.alignmentValue p v₂ w

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_add_right {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v w₁ w₂ : N) : Z.alignmentValue p v (w₁ + w₂) = Z.alignmentValue p v w₁ + Z.alignmentValue p v w₂

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_neg_left {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v w : N) : Z.alignmentValue p (-v) w = -Z.alignmentValue p v w

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_neg_right {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (v w : N) : Z.alignmentValue p v (-w) = -Z.alignmentValue p v w

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_zsmul_right {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (n : ℤ) (v : N) : Z.alignmentValue p v (n • v) = 0

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_add_zsmul_right {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (n : ℤ) (v w : N) : Z.alignmentValue p v (w + n • v) = Z.alignmentValue p v w

An alignment locus depends on the competitor only modulo integral multiples of the reference class.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentLocus_add_zsmul_right {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (n : ℤ) (v w : N) : Z.alignmentLocus v (w + n • v) = Z.alignmentLocus v w

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_add_nsmul_right {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (p : P) (n : ℕ) (v w : N) : Z.alignmentValue p v (w + n • v) = Z.alignmentValue p v w

Compatibility version for a nonnegative integral multiple.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_linearAct {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (g : ℂ →ₗ[ℝ] ℂ) (p : P) (v w : N) : (Z.linearAct g).alignmentValue p v w = realDet g * Z.alignmentValue p v w

The determinant law. alignmentValue is the determinant of the 2 × 2 matrix of real and imaginary parts of the two charges, so post-composing with a real-linear map multiplies it by that map's determinant.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentLocus_linearAct {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) {g : ℂ →ₗ[ℝ] ℂ} (hg : realDet g ≠ 0) (v w : N) : (Z.linearAct g).alignmentLocus v w = Z.alignmentLocus v w

An invertible real-linear change of charge leaves every numerical alignment locus where it was.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentValue_smul {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (c : ℂ) (p : P) (v w : N) : (Z.smul c).alignmentValue p v w = Complex.normSq c * Z.alignmentValue p v w

Rescaling the charges by c scales every alignment expression by ‖c‖².

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.alignmentLocus_smul {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) {c : ℂ} (hc : c ≠ 0) (v w : N) : (Z.smul c).alignmentLocus v w = Z.alignmentLocus v w

Numerical walls are invariant under rescaling the central charge.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.reindex_alignmentLocus {P : Type u} {Q : Type v} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (f : Q → P) (v w : N) : (Z.reindex f).alignmentLocus v w = f ⁻¹' Z.alignmentLocus v w

Reindexing a charge family pulls its alignment locus back as a set.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.pullback_alignmentValue {P : Type u} {N : Type w} {M : Type x} [AddCommGroup N] [AddCommGroup M] (Z : ChargeFamily P N) (f : M →+ N) (p : P) (v w : M) : (Z.pullback f).alignmentValue p v w = Z.alignmentValue p (f v) (f w)

Pullback of numerical classes preserves the alignment expression.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.pullback_alignmentLocus {P : Type u} {N : Type w} {M : Type x} [AddCommGroup N] [AddCommGroup M] (Z : ChargeFamily P N) (f : M →+ N) (v w : M) : (Z.pullback f).alignmentLocus v w = Z.alignmentLocus (f v) (f w)

Pullback of numerical classes identifies the corresponding alignment loci.