The tilt charge family, as the surface family pulled back along a truncation

The (n, m) = (3, 2) tilt charge needs no new polynomial and no kernel. It is stChargeFamily -- the existing three-coordinate surface family owned by CentralCharge/Numerical/SurfaceFamily.lean -- reindexed by Prod.swap and pulled back along the four-to-three coordinate drop.

What is actually new here

threefoldTruncate is the only new construction: the additive map that forgets the fourth compressed degree. Without it the surface nested-semicircle theorems cannot be applied to tilt walls at all, because they speak about stChargeFamily and tilt walls do not.

The chart transposition

The surface family is indexed (s, t) and the threefold half plane is indexed (alpha, beta), with s = beta and t = alpha. That transposition lives in exactly one reindex Prod.swap and nowhere else.

Main results

• tiltFamily -- the tilt charge family, definitionally the surface family.
• rotatedTiltFamily -- tiltFamily.phaseRotate (1/2), the charge Bayer--Lahoz--Macri--Stellari actually induce from.
• nu_eq_tilt_slope, chargeSlope_tilt -- the tilt slope is alpha times the charge slope, tying the family to the existing Threefold.nu.
• rotatedTiltFamily_alignmentLocus_eq_preimage -- every rotated tilt wall is a Prod.swap preimage of an stChargeFamily alignment locus. This is what lets walls_nested_of_discr_nonneg, wall_circle_eq and wall_eq_of_meet apply to tilt walls. The abstraction-audit remediation names this statement rotatedTiltFamily_wall_eq_preimage; MO1.03 (#1314) renamed the wall locus to alignmentLocus, and the name here follows the current spelling.

Two negative results, recorded rather than dropped

• exists_tilt_alignmentValue_ne_threefold -- the tilt family is not a chart change of Threefold.chargeFamily. Their alignment loci genuinely differ, and the witness below is computed, not asserted: the truncation forgets the fourth degree, which the threefold charge reads.
• exists_chargeSlope_rotatedTiltFamily_ne -- the rotation is not cosmetic. It fixes every alignment value (phaseRotate_alignmentValue) and still moves chargeSlope, so a construction that keeps the tilt walls and drops the rotation is right about the wall locus and wrong about which objects are semistable.

The tilt-stability categorical content -- a heart, a slicing, or the BMT inequality -- is asserted nowhere in this file. This is numerical data only.

The four-to-three coordinate drop

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.threefoldTruncate : Threefold.NumClass →+ NumClass

The truncation: forget the fourth compressed degree, and nothing more.

This is the one new construction of the tilt slice. It is additive because the four compressed degrees are additive coordinates on a product of copies of the reals, and it is not an isomorphism: exists_tilt_alignmentValue_ne_threefold records exactly what it forgets.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.threefoldTruncate_apply (v : Threefold.NumClass) : threefoldTruncate v = (v.deg0, v.deg1, v.deg2)

Not a simp lemma. The three coordinate projections below are the normal form worth having, and marking the tuple form simp too would rewrite their left-hand sides out from under them -- which the environment linter reports as rk_threefoldTruncate simplifying to NumClass.rk (v.deg0, v.deg1, v.deg2) rather than to v.deg0.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.rk_threefoldTruncate (v : Threefold.NumClass) : (threefoldTruncate v).rk = v.deg0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.deg_threefoldTruncate (v : Threefold.NumClass) : (threefoldTruncate v).deg = v.deg1

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.ch2_threefoldTruncate (v : Threefold.NumClass) : (threefoldTruncate v).ch2 = v.deg2

The tilt family

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily : ChargeFamily (ℝ × ℝ) Threefold.NumClass

The tilt charge family, at (n, m) = (3, 2).

The existing surface family, transposed once and pulled back along the truncation. No new polynomial and no new kernel: the canonical root is stChargeFamily.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.rotatedTiltFamily : ChargeFamily (ℝ × ℝ) Threefold.NumClass

The rotated tilt family, the charge Bayer--Lahoz--Macri--Stellari induce from. At beta = 1/2 the rotation scalar is -i, which is the division by i those authors write.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily_charge (p : ℝ × ℝ) (v : Threefold.NumClass) : (tiltFamily.charge p) v = (stCharge p.2 p.1) (threefoldTruncate v)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily_re (α β : ℝ) (v : Threefold.NumClass) : tiltFamily.re (α, β) v = -((Threefold.betaTwist β v).deg2 - α ^ 2 / 2 * v.deg0)

The real part of the tilt charge is the Bayer--Macri--Toda numerator, with its sign.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.tiltFamily_im (α β : ℝ) (v : Threefold.NumClass) : tiltFamily.im (α, β) v = α * (Threefold.betaTwist β v).deg1

The imaginary part of the tilt charge is alpha times the twisted first degree.

The tilt slope is the charge slope

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.nu_eq_tilt_slope (α β : ℝ) (v : Threefold.NumClass) (h : 0 < tiltFamily.im (α, β) v) : Threefold.nu α β v = α * (-tiltFamily.re (α, β) v / tiltFamily.im (α, β) v)

The tilt slope is alpha times the charge slope. Threefold.nu of Walls/Threefold/Basic.lean is the charge slope of the tilt family, rescaled.

The hypothesis is the one the slope convention needs: chargeSlope is the top element off the open upper half plane, and Threefold.nu is junk where its denominator vanishes, so the two agree exactly where both are defined.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.chargeSlope_tilt (α β : ℝ) (v : Threefold.NumClass) (h : 0 < tiltFamily.im (α, β) v) : chargeSlope ((tiltFamily.charge (α, β)) v) = ↑(Threefold.nu α β v / α)

The tilt family's chargeSlope, in Bayer--Macri--Toda coordinates.

Every rotated tilt wall is a surface wall

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.rotatedTiltFamily_alignmentLocus_eq_preimage (v w : Threefold.NumClass) : rotatedTiltFamily.alignmentLocus v w = _root_.Prod.swap ⁻¹' stChargeFamily.alignmentLocus (threefoldTruncate v) (threefoldTruncate w)

The rotated tilt walls are Prod.swap preimages of stChargeFamily walls.

This is the statement that lets the surface nested-semicircle theorems apply to tilt walls: walls_nested_of_discr_nonneg, wall_circle_eq and wall_eq_of_meet are about stChargeFamily, and this identifies the tilt wall with one of theirs.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.rotatedTiltFamily_alignmentValue (p : ℝ × ℝ) (v w : Threefold.NumClass) : rotatedTiltFamily.alignmentValue p v w = stChargeFamily.alignmentValue p.swap (threefoldTruncate v) (threefoldTruncate w)

The same statement on the alignment expression itself, which the rotation also fixes.

The two negative results

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.exists_tilt_alignmentValue_ne_threefold : ∃ (p : ℝ × ℝ) (v : Threefold.NumClass) (w : Threefold.NumClass), tiltFamily.alignmentValue p v w = 0 ∧ Threefold.chargeFamily.alignmentValue p v w ≠ 0

The tilt family is not a chart change of the threefold family.

Their alignment loci genuinely differ, and here is the computed witness: at (alpha, beta) = (1, 0) the classes (0, 1, 1, 0) and (0, 1, 1, 1) have the same truncation, so the tilt alignment value vanishes, while the threefold charge reads the fourth degree and its alignment value is 1.

This is the content the truncation forgets, stated as a theorem instead of left as a remark.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Tilt.exists_chargeSlope_rotatedTiltFamily_ne : ∃ (p : ℝ × ℝ) (v : Threefold.NumClass), chargeSlope ((rotatedTiltFamily.charge p) v) ≠ chargeSlope ((tiltFamily.charge p) v)

The rotation is not cosmetic.

phaseRotate_alignmentValue fixes every alignment value, so no tilt wall moves. chargeSlope is a different matter: at (alpha, beta) = (1, 0) the class (0, 1, 1, 0) has tilt charge -1 + i, of slope 1, and rotated charge 1 + i, of slope -1.

Semistability is read off the phase, so a construction that keeps the walls and drops the rotation is right about the wall locus and wrong about which objects are semistable.