Regression theorems via Riemann–Roch

Sanity checks on k(t) and spot checks for the specialty index table.

theorem FunctionField.Chart.genus_ratFunc_via_corollaries (k : Type u_1) [Field k] : genus k (RatFunc k) = 0

genus (RatFunc k) = 0 revisited through the corollary package.

theorem FunctionField.Chart.deg_canonical_ratFunc (k : Type u_1) [Field k] {W : DivisorA k (RatFunc k)} (hW : IsCanonical k (RatFunc k) W) : deg k (RatFunc k) W = -2

When g = 0, a canonical divisor has degree −2.

theorem FunctionField.Chart.ell_neg_deg_ratFunc (k : Type u_1) [Field k] (D : DivisorA k (RatFunc k)) (h : deg k (RatFunc k) D < 0) : ell k (RatFunc k) D = 0

Spot check: negative degree forces ℓ(D) = 0 on RatFunc k.

theorem FunctionField.Chart.ell_large_deg_ratFunc (k : Type u_1) [Field k] {W : DivisorA k (RatFunc k)} (hW : IsCanonical k (RatFunc k) W) (D : DivisorA k (RatFunc k)) (h : deg k (RatFunc k) D ≥ -1) : ↑(ell k (RatFunc k) D) = deg k (RatFunc k) D + 1

Spot check: large degree forces ℓ(D) = deg D + 1 when g = 0.