Families of additive complex charges

This file owns the dimension- and geometry-independent charge-family root. A ChargeFamily P N is only a family of additive maps N →+ ℂ, indexed by an arbitrary parameter type P. It contains no heart, slicing, support property, wall locus, Chern character, or scheme.

reindex changes parameters and pullback changes the additive class presentation. zeroLocus names charge vanishing without calling it a wall. Real-linear postcomposition and complex rescaling also belong here because they act on charges before any wall or phase is considered.

The declarations keep their established ...Wall namespace so the source cutover preserves public names. The path records the mathematical owner; wall equations are downstream in StabilityCondition/Walls/Alignment.lean.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily (P : Type u) (N : Type v) [AddCommGroup N] : Type (max u v)

A parameterized family of additive complex central charges.

This is numerical data only: it deliberately does not contain a heart, a slicing, support-property data, or a topology on the parameter space.

• charge : P → N →+ ℂ

  The central charge at a parameter value.

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

The parameters where the charge of one class vanishes. This is generally two real equations, not a codimension-one numerical alignment wall.

Equations

• Z.zeroLocus v = {p : P | (Z.charge p) v = 0}

@[simp]

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.ext {P : Type u} {N : Type w} [AddCommGroup N] {Z W : ChargeFamily P N} (h : ∀ (p : P), Z.charge p = W.charge p) : Z = W

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.ext_iff {P : Type u} {N : Type w} [AddCommGroup N] {Z W : ChargeFamily P N} : Z = W ↔ ∀ (p : P), Z.charge p = W.charge p

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.reindex {P : Type u} {Q : Type v} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (f : Q → P) : ChargeFamily Q N

Change the parameter space of a charge family.

Equations

• Z.reindex f = { charge := fun (q : Q) => Z.charge (f q) }

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

Pull a charge family back along an additive map of numerical class carriers.

Equations

• Z.pullback f = { charge := fun (p : P) => (Z.charge p).comp f }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.reindex_charge {P : Type u} {Q : Type v} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (f : Q → P) (q : Q) : (Z.reindex f).charge q = Z.charge (f q)

@[simp]

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.reindex_pullback_charge {P : Type u} {Q : Type v} {N : Type w} {M : Type x} [AddCommGroup N] [AddCommGroup M] (Z : ChargeFamily P N) (f : Q → P) (g : M →+ N) (q : Q) (v : M) : (((Z.reindex f).pullback g).charge q) v = (Z.charge (f q)) (g v)

Simultaneously changing parameters and pulling back classes evaluates by composition in the two independent inputs.

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

Reindexing pulls a charge-zero locus back along the parameter map.

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

Pullback of classes compares the corresponding charge-zero loci.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.reindex_id {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) : Z.reindex id = Z

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.reindex_reindex {P : Type u} {Q : Type v} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) {R : Type u_1} (f : Q → P) (g : R → Q) : (Z.reindex f).reindex g = Z.reindex (f ∘ g)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.pullback_id {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) : Z.pullback (AddMonoidHom.id N) = Z

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.pullback_pullback {P : Type u} {N : Type w} {M : Type x} [AddCommGroup N] [AddCommGroup M] (Z : ChargeFamily P N) {L : Type u_1} [AddCommGroup L] (f : M →+ N) (g : L →+ M) : (Z.pullback f).pullback g = Z.pullback (f.comp g)

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

Reindexing and pullback act on independent inputs, so they commute.

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

The real part of the central charge of a class.

Equations

• Z.re p v = ((Z.charge p) v).re

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

The imaginary part of the central charge of a class.

Equations

• Z.im p v = ((Z.charge p) v).im

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.realDet (g : ℂ →ₗ[ℝ] ℂ) : ℝ

The determinant of a real-linear endomorphism of ℂ, computed in the basis 1, I.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.realDet g = (g 1).re * (g Complex.I).im - (g 1).im * (g Complex.I).re

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.map_eq_smul_add_smul (g : ℂ →ₗ[ℝ] ℂ) (z : ℂ) : g z = z.re • g 1 + z.im • g Complex.I

A real-linear map of ℂ is determined by its values on 1 and I.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.linearAct {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (g : ℂ →ₗ[ℝ] ℂ) : ChargeFamily P N

Post-compose every charge of a family with a real-linear map of ℂ.

Equations

• Z.linearAct g = { charge := fun (p : P) => g.toAddMonoidHom.comp (Z.charge p) }

@[simp]

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.smul {P : Type u} {N : Type w} [AddCommGroup N] (Z : ChargeFamily P N) (c : ℂ) : ChargeFamily P N

Rescale every charge by a complex scalar.

Equations

• Z.smul c = Z.linearAct (LinearMap.mulLeft ℝ c)

@[simp]

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily.realDet_mulLeft (c : ℂ) : realDet (LinearMap.mulLeft ℝ c) = Complex.normSq c

Multiplication by c has determinant ‖c‖² as a real-linear map.