Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.CentralCharge.Numerical.SurfaceFamily

The (s, t) numerical charge as a generic charge family #

CentralCharge/Family.lean defines arbitrary parameterized families of additive complex charges. This file packages the three-coordinate surface model as one child of that abstraction without importing wall equations.

The specialization is deliberately thin: its parameter space is ℝ × ℝ, its class carrier is NumClass = ℝ × ℝ × ℝ, and its universal determinant is compared with the existing wallExpr downstream under Walls/Numerical/.

source
noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.stCharge (s t : ℝ) :
NumClass →+ ℂ

The complex charge whose real and imaginary parts are the (s,t) polynomials reZ and imZ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.stCharge_re (s t : ℝ) (v : NumClass) :
    ((stCharge s t) v).re = reZ s t v
    source
    @[simp]
    theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.stCharge_im (s t : ℝ) (v : NumClass) :
    ((stCharge s t) v).im = imZ s t v
    source
    noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.stChargeFamily :
    ChargeFamily (ℝ × ℝ) NumClass

    The old half-plane model, represented as a child of ChargeFamily.

    No positivity condition is built into the parameter type: the hypotheses t > 0 or t ≠ 0 remain attached to precisely the geometric consequences that need them.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.stChargeFamily_charge (p : ℝ × ℝ) (v : NumClass) :
      (stChargeFamily.charge p) v = ↑(reZ p.1 p.2 v) + Complex.I * ↑(imZ p.1 p.2 v)