noncomputable def RiemannRochGeneral.moduleRank (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.

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

Degree of a maximal ideal I of an algebra A over k: dim_k (A / I).

noncomputable def RiemannRochGeneral.lineBundleDegree (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] (J : Ideal A) : ℕ

Degree of a line bundle ideal J of A over k: dim_k (A / J).

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

Arithmetic genus of a Dedekind algebra A over k: dim_k Ω_{A/k}.

theorem RiemannRochGeneral.kaehler_polynomial_rank (k : Type u_1) [Field k] : Module.finrank (Polynomial k) Ω[Polynomial k⁄k] = 1

The Kähler differentials of the polynomial ring k[x] are a free k[x]-module of rank 1.

theorem RiemannRochGeneral.idealDegree_bot_field (k : Type u_1) [Field k] : idealDegree k k ⊥ = 1

For a field k, the ideal ⊥ of k has degree 1 (since k / ⊥ ≅ k).

theorem RiemannRochGeneral.lineBundleDegree_top (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] : lineBundleDegree k A ⊤ = 0

The unit ideal has line bundle degree zero.

theorem RiemannRochGeneral.lineBundleDegree_eq_idealDegree (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] (I : Ideal A) [I.IsMaximal] : lineBundleDegree k A I = idealDegree k A I

For a maximal ideal I, the line bundle degree coincides with the ideal degree.

theorem RiemannRochGeneral.riemann_roch_rank_one_identity (d : ℤ) (g : ℕ) : d + 1 * (1 - ↑g) = d + 1 - ↑g

Algebraic identity used in rank-one Riemann–Roch: d + 1·(1 - g) = d + 1 - g.

theorem RiemannRochGeneral.lineBundleDegree_bot (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra k A] : lineBundleDegree k A ⊥ = Module.finrank k A

The zero ideal has line bundle degree dim_k A.