def RiemannRochCurves.eulerChar (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (structureSheafEuler : ℤ := 1 - ↑(RiemannRochGeneral.arithmeticGenus k A)) : ℤ

Euler characteristic packaged as an integer, defaulting to 1 - g_a (the value at the structure sheaf).

noncomputable def RiemannRochCurves.curveGenus (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : ℕ

Genus of a curve presented by an affine Dedekind algebra: defined as dim_k Ω_{A/k}.

noncomputable def RiemannRochCurves.idealDeg (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] (I : Ideal A) : ℕ

Degree of an ideal I of A: dim_k (A / I).

noncomputable def RiemannRochCurves.moduleRk (A : Type u_1) [CommRing A] [IsDomain A] (M : Type u_2) [AddCommGroup M] [Module A M] : ℕ

Generic rank of an A-module M (for A a domain): the dimension over Frac A of the base-change Frac A ⊗_A M.

theorem RiemannRochCurves.additive_hom_determined_by_generators (f : ℤ × ℤ →+ ℤ) (p : ℤ × ℤ) : f p = p.1 * f (1, 0) + p.2 * f (0, 1)

An additive homomorphism ℤ × ℤ → ℤ is determined by its values on the generators (1, 0) and (0, 1).

theorem RiemannRochCurves.additive_homs_eq_of_generators_eq (f g : ℤ × ℤ →+ ℤ) (h_OX : f (1, 0) = g (1, 0)) (h_Ox : f (0, 1) = g (0, 1)) : f = g

Two additive homomorphisms ℤ × ℤ → ℤ agreeing on the two generators (1, 0) and (0, 1) are equal.

def RiemannRochCurves.rrHom (g : ℤ) : ℤ × ℤ →+ ℤ

The Riemann–Roch additive homomorphism for genus g: (r, d) ↦ d - r(g - 1).

theorem RiemannRochCurves.rrHom_apply (g r d : ℤ) : (rrHom g) (r, d) = d - r * (g - 1)

Evaluation formula for rrHom: rrHom g (r, d) = d - r(g - 1).

theorem RiemannRochCurves.rr_value_structure_sheaf (g : ℤ) : (rrHom g) (1, 0) = 1 - g

The Riemann–Roch hom on (1, 0) (structure sheaf): 1 - g.

theorem RiemannRochCurves.rr_value_skyscraper (g : ℤ) : (rrHom g) (0, 1) = 1

The Riemann–Roch hom on (0, 1) (skyscraper of length 1): 1.

theorem RiemannRochCurves.finrank_additive_ses (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] [Module.Finite k V] (W : Submodule k V) : ↑(Module.finrank k V) = ↑(Module.finrank k ↥W) + ↑(Module.finrank k (V ⧸ W))

For a short exact sequence 0 → W → V → V/W → 0 of finite-dimensional k-vector spaces, dimensions are additive: dim V = dim W + dim V/W.

theorem RiemannRochCurves.riemann_roch_curves_thm (g : ℤ) (χ : ℤ × ℤ →+ ℤ) (hχ_struct : χ (1, 0) = 1 - g) (hχ_sky : χ (0, 1) = 1) (r d : ℤ) : χ (r, d) = d - r * (g - 1)

Riemann–Roch for curves (Thm 24.2, Lec 24): the Euler characteristic homomorphism is χ(r, d) = d - r(g - 1), determined by its values on the structure sheaf and a skyscraper.

theorem RiemannRochCurves.rr_genus_zero (χ : ℤ × ℤ →+ ℤ) (hχ_struct : χ (1, 0) = 1) (hχ_sky : χ (0, 1) = 1) (r d : ℤ) : χ (r, d) = d + r

Genus-zero Riemann–Roch (i.e. on ℙ¹): χ(r, d) = d + r.

theorem RiemannRochCurves.idealDeg_top (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] : idealDeg k A ⊤ = 0

The unit ideal has degree zero: dim_k (A / A) = 0.

theorem RiemannRochCurves.idealDeg_bot (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] : idealDeg k A ⊥ = Module.finrank k A

The zero ideal has degree dim_k A: idealDeg k A ⊥ = dim_k A.