The Mukai tilt stability function on the bounded derived category of a K3 #
This file is the geometric adapter from coherent-sheaf data to the abstract
Mukai tilt assembly. It constructs the correctly normalized numerical slope,
transfers its HN property from the Hilbert-coefficient slope, transports it to
the standard heart of Dᵇ(Coh X), and extends the coherent Mukai class
canonically to K₀(Dᵇ(Coh X)) through the cohomological Euler equivalence.
Two genuinely geometric seams remain explicit: the dimension-zero sheaf classification and the boundary Jordan--Hölder/Mukai-square decomposition. The latter is exactly the existing abstract boundary hypothesis: issue #332 supplies finite-dimensional Hom spaces but not yet the stable-simple, Jordan--Hölder, and Serre-duality argument needed to prove that decomposition. No topology and no full stability condition are introduced here.
Grothendieck's boundedness lemma in the exact form needed for μ-HN
filtrations. This is the only part of MuHNInput that remains supplied on a
Noetherian scheme.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Noetherianity of coherent sheaves discharges the first MuHNInput field;
only Grothendieck slope boundedness is retained.
The precise affine normalization relating the leading two Hilbert
coefficients to numerical rank and ω · ch₁ on a surface.
For the usual Hilbert polynomial of a polarized K3, scale is H² and
shift is H² / 2. They remain explicit because the current geometric
reconstruction and Gieseker packages do not yet prove that comparison.
- scale : ℤ
Positive integral scaling between numerical rank and multiplicity.
The scaling is strictly positive.
- shift : ℝ
The affine shift of finite slopes.
Hilbert multiplicity is the scaled numerical rank.
- degree_eq (F : Coh X) : ↑(P.hilbertDegreeCoefficient F) = R.divisorSpace.pair ω (R.chernCharacter.chOne (CategoryTheory.K₀Ab.of F)) + self.shift * ↑(V.rank (CategoryTheory.K₀Ab.of F))
The next Hilbert coefficient is divisor degree plus the rank shift.
Instances For
Numerical rank and ω · ch₁ as weak slope data on coherent sheaves.
Equations
- N.mukaiSlopeData hμ = { rankHom := V.rank, degreeHom := (R.divisorSpace.intersection ω).toAddMonoidHom.comp R.chernCharacter.chOne, rank_nonneg := ⋯, degree_nonneg_of_rank_zero := ⋯ }
Instances For
At positive numerical rank, the Hilbert slope is the Mukai slope followed by the positive affine normalization.
The Hilbert-coefficient slope and the numerical Mukai slope induce the same order on coherent sheaves.
The numerical Mukai slope inherits HN filtrations from Gieseker's Hilbert-coefficient slope.
The standard heart of the bounded derived category #
The standard t-structure restricted to Dᵇ(Coh X).
Equations
Instances For
The standard heart of Dᵇ(Coh X).
Equations
Instances For
The numerical Mukai slope transported from coherent sheaves to the
standard heart of Dᵇ(Coh X).
Equations
Instances For
The bounded-heart numerical slope has the HN property.
The real Mukai class and its ambient realization #
The real Mukai class of coherent sheaves supplied by the numerical surface realization.
Equations
Instances For
The coherent Mukai class transported to the standard bounded heart.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An ambient Mukai class on K₀(Dᵇ(Coh X)) realizes the geometric class
when its restriction to the standard heart is the transported coherent-sheaf
class. This predicate remains useful for arbitrary ambient class maps; the
canonical cohomological extension below satisfies it automatically.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coherent Mukai class extended canonically to the bounded derived category by its cohomological Euler class.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical derived Mukai class restricts to the supplied coherent Mukai class on the standard bounded heart.
On a numerical K3, the ambient geometric Mukai class computes the rank and divisor degree of the bounded-heart normalized slope.
The canonical derived Mukai class computes the bounded-heart normalized slope data; no separate ambient realization hypothesis is needed.
The remaining sheaf-level geometric classification #
The dimension-zero Mukai-class statement at the coherent-sheaf level.
This is the honest geometric gap: the repository does not yet have a theory of support dimension and length from which to prove it. Naming it here avoids replacing that missing theorem by a manufactured heart-level witness.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A coherent-sheaf dimension-zero classification supplies exactly the abstract torsion-boundary input required by the Mukai tilt argument.
A coherent-sheaf dimension-zero classification supplies the torsion boundary statement for the canonical derived Mukai class.
The K3 Mukai tilt stability function #
The exponential Mukai charge as a stability function on the tilted
standard heart of Dᵇ(Coh X).
All formal inputs are discharged here. The ambient realization equality, dimension-zero classification, and K3 boundary decomposition remain visible geometric hypotheses. The last is the named gap whose missing categorical ingredients are tracked from issue #332. The conclusion is only a stability function; it does not assert the HN property on the tilted heart or package a full stability condition.
Equations
- N.tiltStabilityFunction hμ hbounded hK3 m hm hHodge hω hzero hboundary = CategoryTheory.Triangulated.MukaiWeakSlopeCompat.tiltStabilityFunction ⋯ ⋯ hω ⋯ ⋯ ⋯ hboundary
Instances For
The assembled stability function uses the original ambient exponential Mukai charge, with no numerical replacement of the third coordinate.
The K3 tilt stability function using the canonical cohomological extension of the coherent Mukai class. The genuine geometric boundedness, dimension-zero, Hodge, and boundary-decomposition obligations remain explicit.
Equations
- One or more equations did not get rendered due to their size.