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

ℓ(D) := dim_k Hom_A(I, A), the dimension of the space of regular sections of the line bundle attached to a divisor with associated ideal I.

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

ℓ(K − D) := dim_k Hom_A(I, Ω[A/k]), the dimension of regular sections of the differential twist K − D, the Serre dual.

noncomputable def RiemannFormRR.divisorEulerChar (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] (I : Ideal A) : ℤ

The Euler characteristic ℓ(D) − ℓ(K−D), the left-hand side of the Riemann–Roch formula.

def RiemannFormRR.SatisfiesRiemannRoch (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : Prop

Predicate: A satisfies Riemann–Roch (Cor 30) — for every nonzero ideal I the Euler characteristic equals deg D + 1 − g.

theorem RiemannFormRR.SatisfiesRiemannRoch.rr_formula {k : Type u_1} [Field k] {A : Type u_2} [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (h : SatisfiesRiemannRoch k A) (I : Ideal A) (hI : I ≠ ⊥) : divisorEulerChar k A I = ↑(RiemannRochGeneral.lineBundleDegree k A I) + 1 - ↑(RiemannRochGeneral.arithmeticGenus k A)

Unfolding the Riemann–Roch predicate: extracting the formula at a fixed nonzero ideal I.

def RiemannFormRR.homTopEquiv (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] (M : Type u_3) [AddCommGroup M] [Module A M] [Module k M] [SMulCommClass A k M] : (↥⊤ →ₗ[A] M) ≃ₗ[k] M

Identification Hom_A(A, M) ≃ M: the case I = ⊤ of the Hom-bundle, used to compute ℓ(⊤) = dim_k A.

theorem RiemannFormRR.lD_top (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] : lD k A ⊤ = Module.finrank k A

ℓ(⊤) = dim_k A: trivial-divisor specialization of lD.

theorem RiemannFormRR.lKD_top (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] : lKD k A ⊤ = Module.finrank k Ω[A⁄k]

ℓ(K − ⊤) = dim_k Ω[A/k] = g, the arithmetic genus.

theorem RiemannFormRR.riemann_roch_field (k : Type u_1) [Field k] (I : Ideal k) (hI : I ≠ ⊥) : divisorEulerChar k k I = ↑(RiemannRochGeneral.lineBundleDegree k k I) + 1 - ↑(RiemannRochGeneral.arithmeticGenus k k)

Sanity check: the Riemann–Roch formula holds for the trivial Dedekind domain A = k, where g = 0, deg D = 0, and Euler characteristic equals 1 = 0 + 1 − 0.