The see-saw inequality for the μ-slope on Coh X

For a short exact sequence 0 ⟶ B ⟶ C ⟶ Q ⟶ 0 of coherent sheaves, the slope of the middle term lies between the slopes of the ends. This file proves the half of that statement the Harder–Narasimhan recursion needs: if the sub has slope at most the quotient, then it has slope at most the whole.

No such inequality exists for the abstract weak slope in Abelian/Stability/**, and this one is not abstract: it is the mediant inequality for the ratio of two additive integer invariants, and its ⊤ cases are decided by the geometric input carried by MuPositivityData. It is stated here, for the recursion that consumes it.

The three cases

Multiplicity and degree coefficient are both additive on short exact sequences, so with m = multiplicity and d = hilbertDegreeCoefficient the middle term has m C = m B + m Q and d C = d B + d Q.

• m B = 0. The sub has slope ⊤, so the hypothesis forces the quotient to slope ⊤ as well, hence m Q = 0, hence m C = 0 and the whole has slope ⊤.
• m B > 0 and m Q = 0. The whole has m C = m B, and the inequality reduces to 0 ≤ d Q, which is exactly MuPositivityData.degree_nonneg_of_multiplicity_zero. This is the case that fails without that geometric input.
• Both positive. The mediant inequality: d B / m B ≤ d Q / m Q gives d B / m B ≤ (d B + d Q) / (m B + m Q).

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.multiplicity_shortExact {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) : P.multiplicity S.X₂ = P.multiplicity S.X₁ + P.multiplicity S.X₃

Multiplicity is additive on a short exact sequence.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.hilbertDegreeCoefficient_shortExact {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) : P.hilbertDegreeCoefficient S.X₂ = P.hilbertDegreeCoefficient S.X₁ + P.hilbertDegreeCoefficient S.X₃

The degree coefficient is additive on a short exact sequence.

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.topSlope_le_of_shortExact {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) (h3 : ¬CategoryTheory.Limits.IsZero S.X₃) (hle : (P.weakSlopeData h).topSlope S.X₁ ≤ (P.weakSlopeData h).topSlope S.X₃) : (P.weakSlopeData h).topSlope S.X₁ ≤ (P.weakSlopeData h).topSlope S.X₂

The see-saw inequality. In a short exact sequence, if the sub has slope at most the quotient then it has slope at most the whole. See the module docstring for the three cases; the multiplicity-zero quotient is the one where the geometric input is used, and it is the only case needing the quotient to be nonzero — the sub may be zero.