Atlas.AlgebraicGeometryI.code.RiemannRochRiemannForm

structure RiemannRochRiemannForm.SerreDualityCurve (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) :

Bundle of Serre-duality data for a sheaf on a smooth complete curve C of class (r, d): nonnegative integers h0, h1 with χ = h0 − h1 plus an isomorphism h1 = h0_dual exhibiting Serre duality.

h0 : ℤ
h1 : ℤ
h0_dual : ℤ
chi_decomp : C.χ (r, d) = self.h0 - self.h1
serre_dual : self.h1 = self.h0_dual
h0_nonneg : self.h0 ≥ 0
h1_nonneg : self.h1 ≥ 0

Instances For

source

theorem RiemannRochRiemannForm.riemann_form_general (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) (SD : SerreDualityCurve C r d) :

SD.h0 - SD.h0_dual = d + r * (1 - C.g)

Cor 30 (Lec 24), Riemann form of Riemann–Roch: under Serre duality, h^0(ℰ) − h^0(K ⊗ ℰ*) = d + r(1 − g).

source

theorem RiemannRochRiemannForm.riemann_form_general_alt (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) (SD : SerreDualityCurve C r d) :

SD.h0 - SD.h0_dual = d - r * (C.g - 1)

Subtractive reformulation of Cor 30: h^0(ℰ) − h^0(K ⊗ ℰ*) = d − r(g − 1).

source

theorem RiemannRochRiemannForm.riemann_form_line_bundle (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) (SD : SerreDualityCurve C 1 d) :

SD.h0 - SD.h0_dual = d + 1 - C.g

Cor 30 specialized to line bundles: h^0(L) − h^0(K − L) = d + 1 − g.

source

theorem RiemannRochRiemannForm.riemann_inequality_line_bundle (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) (SD : SerreDualityCurve C 1 d) :

SD.h0 ≥ d + 1 - C.g

Riemann inequality for line bundles: h^0(L) ≥ d + 1 − g.

source

theorem RiemannRochRiemannForm.riemann_inequality_general (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) (SD : SerreDualityCurve C r d) :

SD.h0 ≥ d + r * (1 - C.g)

Riemann inequality in general rank: h^0(ℰ) ≥ d + r(1 − g).

source

theorem RiemannRochRiemannForm.riemann_roch_exact_when_h1_zero (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) (SD : SerreDualityCurve C r d) (h1_zero : SD.h1 = 0) :

SD.h0 = d + r * (1 - C.g)

When h^1 vanishes the Riemann inequality is an equality: h^0 = d + r(1 − g).

source

theorem RiemannRochRiemannForm.serre_duality_chi_rank (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) :

C.χ (r, d) + C.χ (r, r * C.degK - d) = 0

Serre-duality identity at the level of Euler characteristics in general rank: χ(r, d) + χ(r, r·deg K − d) = 0.

source

theorem RiemannRochRiemannForm.serre_duality_chi_line_bundle (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) :

C.χ (1, d) + C.χ (1, C.degK - d) = 0

Serre-duality at the level of Euler characteristics for line bundles.

source

def RiemannRochRiemannForm.serreDualClass (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) :

ℤ × ℤ

The Serre dual class of (r, d): (r, r·deg K − d).

Instances For

source

theorem RiemannRochRiemannForm.serreDualClass_line_bundle (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : ℤ) :

serreDualClass C 1 d = (1, C.degK - d)

For a line bundle, the Serre dual class is (1, deg K − d).

source

theorem RiemannRochRiemannForm.serreDualClass_degree (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d : ℤ) :

(serreDualClass C r d).2 = r * (2 * C.g - 2) - d

The degree component of the Serre dual class, using deg K = 2g − 2.

source

def RiemannRochRiemannForm.mkSerreDualityCurve (C : CanonicalSheafCurves.SmoothCompleteCurve) (r d h0 h1 h0_dual : ℤ) (hchi : C.χ (r, d) = h0 - h1) (hsd : h1 = h0_dual) (hh0 : h0 ≥ 0) (hh1 : h1 ≥ 0) :

SerreDualityCurve C r d

Smart constructor for SerreDualityCurve from raw data.

Instances For

source

theorem RiemannRochRiemannForm.serre_duality_P1_verify (n : ℤ) :

max (-n - 1) 0 = max (-2 - n + 1) 0

Numerical avatar of Serre duality on ℙ¹: max(−n − 1, 0) = max((−2 − n) + 1, 0).

source

theorem RiemannRochRiemannForm.riemann_roch_P1_max_identity (n : ℤ) :

max (n + 1) 0 - max (-n - 1) 0 = n + 1

Numerical Riemann–Roch on ℙ¹: max(n + 1, 0) − max(−n − 1, 0) = n + 1.

source

theorem RiemannRochRiemannForm.riemann_form_P1_verify (n : ℤ) :

max (n + 1) 0 - max (-n - 1) 0 = n + 1 * (1 - 0)

Riemann form of Riemann–Roch on ℙ¹ rewritten with the g = 0 rank formula n + 1 · (1 − 0).

source

theorem RiemannRochRiemannForm.riemann_inequality_P1_nonneg (n : ℤ) (hn : n ≥ 0) :

max (n + 1) 0 ≥ n + 1

For n ≥ 0, Riemann inequality on ℙ¹ is an equality: max(n + 1, 0) ≥ n + 1.

source

theorem RiemannRochRiemannForm.riemann_form_mkCurve (g : ℕ) (r d : ℤ) :

(CanonicalSheafCurves.mkCurve g).χ (r, d) = d + r * (1 - ↑g)

Riemann–Roch on the model curve mkCurve g: χ(r, d) = d + r(1 − g).

source

theorem RiemannRochRiemannForm.serre_duality_mkCurve (g : ℕ) (d : ℤ) :

(CanonicalSheafCurves.mkCurve g).χ (1, d) + (CanonicalSheafCurves.mkCurve g).χ (1, (CanonicalSheafCurves.mkCurve g).degK - d) = 0

Serre duality on the model curve mkCurve g: χ(1, d) + χ(1, deg K − d) = 0.

source

theorem RiemannRochRiemannForm.riemann_form_genus0 (d : ℤ) :

(CanonicalSheafCurves.mkCurve 0).χ (1, d) = d + 1

Riemann form for genus 0 (ℙ¹): χ(𝒪(d)) = d + 1.

source

theorem RiemannRochRiemannForm.riemann_form_genus1 (d : ℤ) :

(CanonicalSheafCurves.mkCurve 1).χ (1, d) = d

Riemann form for genus 1 (elliptic): χ(L_d) = d.

source

theorem RiemannRochRiemannForm.riemann_form_genus2 (d : ℤ) :

(CanonicalSheafCurves.mkCurve 2).χ (1, d) = d - 1

Riemann form for genus 2: χ(L_d) = d − 1.

source

theorem RiemannRochRiemannForm.algebraic_abstract_consistency {k : Type u_1} [Field k] {A : Type u_2} [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] (hrr : RiemannFormRR.SatisfiesRiemannRoch k A) (I : Ideal A) (hI : I ≠ ⊥) (g : ℤ) (hg : g = ↑(RiemannRochGeneral.arithmeticGenus k A)) :

↑(RiemannFormRR.lD k A I) - ↑(RiemannFormRR.lKD k A I) = ↑(RiemannRochGeneral.lineBundleDegree k A I) + 1 - g

Compatibility between the geometric Riemann–Roch on a smooth curve and the algebraic Riemann–Roch on a Dedekind algebra: both yield l(D) − l(K − D) = deg D + 1 − g.

source