Orthogonal slices of divisorial surface-charge families

CentralCharge/Family.lean defines parameterized additive charges. This file supplies a divisorial descendant without importing wall equations.

Given a real divisor space, a distinguished class H, and a linear family of transverse classes G(u) orthogonal to H, an OrthogonalSlice parameterizes

B = s H + G(u), omega = t H.

The transverse parameter space U is an arbitrary real vector space. Thus a rank-one surface uses the zero-dimensional U, a Picard-rank-two surface may use U = ℝ, and higher-rank surfaces may use a finite-dimensional coordinate space or the entire intrinsic orthogonal subspace. Bases remain optional children of the construction.

Wall loci and their determinant formulas are added downstream in Walls/Divisorial/Slice.lean. Ampleness and the Hodge-index signature are separate proposition-valued certificates; neither is required to define the charge family.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.chargeFamily {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] {P : Type w} (ch : ChernCharacter N D) (S : DivisorSpace D) (parameters : P → StabilityParameters D) : ChargeFamily P N

Any parameterization of divisorial data induces a generic central-charge family.

Equations

• ch.chargeFamily S parameters = { charge := fun (p : P) => ch.centralCharge S (parameters p) }

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.fullChargeFamily {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) : ChargeFamily (StabilityParameters D) N

The full divisorial wall family, indexed by arbitrary independent real B and omega classes. Every surface slice below is a reindexing of this parent family.

Equations

• ch.fullChargeFamily S = ch.chargeFamily S id

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.chargeFamily_charge {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] {P : Type w} (ch : ChernCharacter N D) (S : DivisorSpace D) (parameters : P → StabilityParameters D) (p : P) (E : N) : ((ch.chargeFamily S parameters).charge p) E = (ch.centralCharge S (parameters p)) E

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.fullChargeFamily_charge {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (p : StabilityParameters D) (E : N) : ((ch.fullChargeFamily S).charge p) E = (ch.centralCharge S p) E

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice {D : Type u} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (U : Type w) [AddCommGroup U] [Module ℝ U] : Type (max u w)

A basis-free orthogonal slice through the real divisor parameter space.

Only orthogonality is structural. Positivity, ampleness, and negative definiteness belong to OrthogonalSlice.IsHodge and .IsGeometric.

• H : D

  The distinguished polarization direction.

• transverse : U →ₗ[ℝ] D

  A linear parameterization of directions transverse to H.

• orthogonal (u : U) : S.pair self.H (self.transverse u) = 0

  Every transverse direction is intersection-orthogonal to H.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point (U : Type w) : Type w

A point (s,u,t) of an orthogonal slice.

• s : ℝ

  Coefficient of H in the B-field.

• u : U

  Transverse B-field parameter.

• t : ℝ

  Coefficient of H in omega.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.parameters {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) : StabilityParameters D

The intrinsic divisor parameters represented by a slice point.

Equations

• T.parameters p = { B := p.s • T.H + T.transverse p.u, omega := p.t • T.H }

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.chargeFamily {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) : ChargeFamily (Point U) N

The central-charge family obtained from an orthogonal divisor slice.

Equations

• T.chargeFamily ch = (ch.fullChargeFamily S).reindex T.parameters

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.orthogonalSubspace {D : Type u} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (H : D) : Submodule ℝ D

The intrinsic intersection-orthogonal complement of a divisor class.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.orthogonalSubspace S H = (S.intersection H).ker

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.fullOrthogonal {D : Type u} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (H : D) : OrthogonalSlice S ↥(orthogonalSubspace S H)

The basis-free slice using the full intrinsic orthogonal complement of H.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.exists_fullOrthogonal_coordinates {D : Type u} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (H B : D) (hH : S.pair H H ≠ 0) : ∃ (s : ℝ) (G : ↥(orthogonalSubspace S H)), B = s • H + ↑G

Every real divisor class decomposes into its H component and an orthogonal component when H² is nonzero. Thus the intrinsic fullOrthogonal slice loses no B-field directions; only omega is restricted to the ray through H.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.rankOne {D : Type u} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (H : D) : OrthogonalSlice S (Fin 0 → ℝ)

The rank-one slice has no transverse directions.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.rankOne S H = { H := H, transverse := 0, orthogonal := ⋯ }

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point.rankOne (s t : ℝ) : Point (Fin 0 → ℝ)

A point of the rank-one slice.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point.rankOne s t = { s := s, u := 0, t := t }

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.IsHodge {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) : Prop

Numerical Hodge-index data for an orthogonal slice. It is not needed for the wall equation itself.

• H_square_pos : 0 < S.pair T.H T.H

  The distinguished direction has positive square.

• transverse_square_neg (u : U) : u ≠ 0 → S.pair (T.transverse u) (T.transverse u) < 0

  Every nonzero transverse parameter has negative square.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.IsGeometric {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (ample : Set D) extends T.IsHodge : Prop

Geometry-specific ampleness attached to the numerical Hodge data.

• H_square_pos : 0 < S.pair T.H T.H
• transverse_square_neg (u : U) : u ≠ 0 → S.pair (T.transverse u) (T.transverse u) < 0
• H_ample : T.H ∈ ample

  The distinguished direction lies in the supplied ample cone.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.parameters_B {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) : (T.parameters p).B = p.s • T.H + T.transverse p.u

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.parameters_omega {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) : (T.parameters p).omega = p.t • T.H

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.B_square {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) : S.pair (T.parameters p).B (T.parameters p).B = p.s ^ 2 * S.pair T.H T.H + S.pair (T.transverse p.u) (T.transverse p.u)

The B-field square splits into its longitudinal and transverse parts.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.omega_square {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) : S.pair (T.parameters p).omega (T.parameters p).omega = p.t ^ 2 * S.pair T.H T.H

The polarization square on the slice.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.omega_B {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) : S.pair (T.parameters p).omega (T.parameters p).B = p.t * p.s * S.pair T.H T.H

The mixed product omega.B has no transverse contribution.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.B_pair {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) (x : D) : S.pair (T.parameters p).B x = p.s * S.pair T.H x + S.pair (T.transverse p.u) x

Pairing the B-field with an arbitrary divisor class.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.omega_pair {D : Type u} [AddCommGroup D] [Module ℝ D] {U : Type w} [AddCommGroup U] [Module ℝ U] {S : DivisorSpace D} (T : OrthogonalSlice S U) (p : Point U) (x : D) : S.pair (T.parameters p).omega x = p.t * S.pair T.H x

Pairing omega with an arbitrary divisor class.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.reFormula {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) (E : N) : ℝ

The real-part polynomial of the divisorial charge on the slice.

Equations

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

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.imFormula {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) (E : N) : ℝ

The imaginary-part polynomial of the divisorial charge on the slice.

Equations

• T.imFormula ch p E = p.t * (S.pair T.H (ch.chOne E) - p.s * S.pair T.H T.H * ch.rank E)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.centralCharge_eq_formula {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) (E : N) : (ch.centralCharge S (T.parameters p)) E = ↑(T.reFormula ch p E) + Complex.I * ↑(T.imFormula ch p E)

The intrinsic divisorial central charge restricted to an arbitrary orthogonal slice.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.charge_re {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) (E : N) : (((T.chargeFamily ch).charge p) E).re = T.reFormula ch p E

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.charge_im {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) (E : N) : (((T.chargeFamily ch).charge p) E).im = T.imFormula ch p E