theorem RiemannRochEulerCurves.chi_rr_curve (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) : C.χ (r, d) = d + r * (1 - C.g)

Riemann–Roch in additive form for a curve: χ(r, d) = d + r(1 - g).

theorem RiemannRochEulerCurves.chi_rr_curve_alt (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) : C.χ (r, d) = d - r * (C.g - 1)

Riemann–Roch in subtractive form: χ(r, d) = d - r(g - 1).

theorem RiemannRochEulerCurves.euler_char_additive (C : CanonicalSheafCurves.SmoothCompleteCurve) (a b : ℤ × ℤ) : C.χ (a + b) = C.χ a + C.χ b

Additivity of the Euler-characteristic hom on the Grothendieck-class group: χ(a + b) = χ(a) + χ(b).

theorem RiemannRochEulerCurves.euler_char_neg (C : CanonicalSheafCurves.SmoothCompleteCurve) (a : ℤ × ℤ) : C.χ (-a) = -C.χ a

Negation under the Euler characteristic: χ(-a) = -χ(a).

theorem RiemannRochEulerCurves.euler_char_zsmul (C : CanonicalSheafCurves.SmoothCompleteCurve) (n : ℤ) (a : ℤ × ℤ) : C.χ (n • a) = n • C.χ a

Integer scaling under the Euler characteristic: χ(n • a) = n • χ(a).

theorem RiemannRochEulerCurves.euler_char_zero (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.χ 0 = 0

χ(0) = 0.

theorem RiemannRochEulerCurves.euler_char_determines_chi (C : CanonicalSheafCurves.SmoothCompleteCurve) (f : ℤ × ℤ →+ ℤ) (hf_struct : f (1, 0) = 1 - C.g) (hf_sky : f (0, 1) = 1) (p : ℤ × ℤ) : f p = C.χ p

Any additive map agreeing with χ on the structure sheaf and a skyscraper equals χ on all classes.

theorem RiemannRochEulerCurves.chi_structure_sheaf_curve (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.χ (1, 0) = 1 - C.g

The Euler characteristic of the structure sheaf is 1 - g.

theorem RiemannRochEulerCurves.euler_char_skyscraper (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.χ (0, 1) = 1

The Euler characteristic of a length-1 skyscraper is 1.

theorem RiemannRochEulerCurves.euler_char_line_bundle (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) : C.χ (1, d) = d + 1 - C.g

Riemann–Roch for line bundles: χ(L_d) = d + 1 - g.

theorem RiemannRochEulerCurves.euler_char_torsion (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) : C.χ (0, d) = d

Euler characteristic of a torsion sheaf of length d: χ(0, d) = d.

theorem RiemannRochEulerCurves.euler_char_free (C : CanonicalSheafCurves.SmoothCompleteCurve) (r : ℤ) : C.χ (r, 0) = r * (1 - C.g)

Euler characteristic of a free sheaf of rank r: χ(r, 0) = r(1 - g).

theorem RiemannRochEulerCurves.euler_char_twist (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d n : ℤ) : C.χ (r, d + n * r) = C.χ (r, d) + n * r

Twisting by a point shifts the Euler characteristic by the rank.

theorem RiemannRochEulerCurves.euler_char_dual_line_bundle (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) : C.χ (1, d) + C.χ (1, C.degK - d) = 0

Serre duality for line bundles: χ(L) + χ(K ⊗ L^*) = 0.

theorem RiemannRochEulerCurves.euler_char_serre_O_K (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.χ (1, 0) + C.χ (1, C.degK) = 0

Special case of Serre duality: χ(𝒪) + χ(ω) = 0.

theorem RiemannRochEulerCurves.h0_lower_bound (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0 h1 : ℤ) (hchi : C.χ (1, d) = h0 - h1) (hh1 : h1 ≥ 0) : h0 ≥ d + 1 - C.g

Riemann inequality: from χ(L) = h^0 - h^1 ≥ h^0 - (h^0 - (d + 1 - g)) - ... combined with h^1 ≥ 0 we get h^0 ≥ d + 1 - g.

theorem RiemannRochEulerCurves.h0_of_vanishing_h1 (C : CanonicalSheafCurves.SmoothCompleteCurve) (d h0 : ℤ) (hchi : C.χ (1, d) = h0) : h0 = d + 1 - C.g

When h^1 = 0, Riemann–Roch is exact: h^0 = d + 1 - g.

theorem RiemannRochEulerCurves.euler_char_positive_slope (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) (_hr : r > 0) (hd : d > r * (C.g - 1)) : C.χ (r, d) > 0

For positive rank and large enough degree, the Euler characteristic is strictly positive.

theorem RiemannRochEulerCurves.euler_char_canonical (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.χ (1, C.degK) = C.g - 1

Euler characteristic of the canonical sheaf: χ(ω_C) = g - 1.

theorem RiemannRochEulerCurves.euler_char_canonical_from_rr (C : CanonicalSheafCurves.SmoothCompleteCurve) : C.degK + 1 - C.g = C.g - 1

Numerical Euler characteristic of ω: deg K + 1 - g = g - 1, equivalent to deg K = 2g - 2.

theorem RiemannRochEulerCurves.euler_char_P1 (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) (d : ℤ) : C.χ (1, d) = d + 1

Riemann–Roch on ℙ¹ (g = 0): χ(𝒪(d)) = d + 1.

theorem RiemannRochEulerCurves.euler_char_elliptic (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 1) (d : ℤ) : C.χ (1, d) = d

Riemann–Roch on an elliptic curve (g = 1): χ(𝒪(d)) = d.

theorem RiemannRochEulerCurves.euler_char_genus2_O (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 2) : C.χ (1, 0) = -1

For a genus-2 curve, χ(𝒪) = -1.

theorem RiemannRochEulerCurves.mkCurve_euler_char (g : ℕ) (r d : ℤ) : (CanonicalSheafCurves.mkCurve g).χ (r, d) = d + r * (1 - ↑g)

Riemann–Roch for the standard curve mkCurve g: χ(r, d) = d + r(1 - g).

theorem RiemannRochEulerCurves.euler_char_degree_shift (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) : C.χ (r, d + 1) = C.χ (r, d) + 1

Increasing the degree by 1 shifts χ by 1: χ(r, d + 1) = χ(r, d) + 1.

theorem RiemannRochEulerCurves.euler_char_rank_shift (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) : C.χ (r + 1, d) = C.χ (r, d) + (1 - C.g)

Increasing the rank by 1 shifts χ by 1 - g.

theorem RiemannRochEulerCurves.euler_char_minus_trivial (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) : C.χ (r, d) - C.χ (r, 0) = d

The Euler characteristic difference along the degree axis equals the degree: χ(r, d) - χ(r, 0) = d.