Documentation

Atlas.AlgebraicGeometryI.code.RiemannRochApplications

source
def RiemannRochApplications.structureSheafSD (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g β‰₯ 0) :
RiemannRochRiemannForm.SerreDualityCurve C 1 0

Serre duality package for the structure sheaf π’ͺ_C of a smooth complete curve C: h^0(π’ͺ) = 1, h^1(π’ͺ) = g.

Instances For
    source
    def RiemannRochApplications.canonicalSheafSD (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g β‰₯ 0) :
    RiemannRochRiemannForm.SerreDualityCurve C 1 C.degK

    Serre duality package for the canonical sheaf Ο‰_C: h^0(Ο‰) = g, h^1(Ο‰) = 1.

    Instances For
      source
      theorem RiemannRochApplications.corollary_29_serre_duality (C : CanonicalSheafCurves.SmoothCompleteCurve) (_hg : C.g β‰₯ 0) (h0_O h1_O h0_K : β„€) (_hchi_O : C.Ο‡ (1, 0) = h0_O - h1_O) (hSD_O : h1_O = h0_K) (_hh0_O : h0_O = 1) (hh1_O : h1_O = C.g) :
      h0_K = C.g

      Serre duality for the structure sheaf: h^0(π’ͺ_C) = 1 and h^1(π’ͺ_C) = h^0(Ο‰_C) = g.

      source
      theorem RiemannRochApplications.corollary_29 (C : CanonicalSheafCurves.SmoothCompleteCurve) (_hg : C.g β‰₯ 0) (h0_K h1_K : β„€) (hchi_K : C.Ο‡ (1, C.degK) = h0_K - h1_K) (hSD_K : h1_K = 1) :
      h0_K = C.g

      Corollary 29 (Lec 25): h^0(Ο‰_C) = g, the dimension of global sections of the canonical sheaf equals the geometric genus.

      source
      theorem RiemannRochApplications.genus_from_canonical_sections (C : CanonicalSheafCurves.SmoothCompleteCurve) (_hg : C.g β‰₯ 0) (h0_K h1_K : β„€) (hchi_K : C.Ο‡ (1, C.degK) = h0_K - h1_K) (hSD_K : h1_K = 1) (_hh0_K : h0_K β‰₯ 0) :
      h0_K = C.g

      The genus can be computed from h^0(K) and h^1(K): under Serre duality h^1(K) = 1, so h^0(K) = g.

      source
      theorem RiemannRochApplications.corollary_29_numerical (C : CanonicalSheafCurves.SmoothCompleteCurve) :
      C.Ο‡ (1, 0) = 1 - C.g ∧ C.Ο‡ (1, C.degK) = C.g - 1 ∧ C.Ο‡ (1, 0) + C.Ο‡ (1, C.degK) = 0

      Numerical Corollary 29: Ο‡(π’ͺ) = 1 - g, Ο‡(Ο‰) = g - 1, and Ο‡(π’ͺ) + Ο‡(Ο‰) = 0 (Serre duality for π’ͺ).

      source
      theorem RiemannRochApplications.serre_dual_degree (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : β„€) :
      C.degK - d = 2 * C.g - 2 - d

      The degree of the Serre dual of L (of degree d) is 2g - 2 - d, using deg K = 2g - 2.

      source
      theorem RiemannRochApplications.high_degree_serre_dual_negative (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : β„€) (hd : d > 2 * C.g - 2) :
      C.degK - d < 0

      For a line bundle of degree d > 2g - 2, the Serre dual has negative degree.

      source
      theorem RiemannRochApplications.high_degree_euler_char_dual_nonpos (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : β„€) (hd : d > 2 * C.g - 2) (hg : C.g β‰₯ 0) :
      C.Ο‡ (1, C.degK - d) ≀ 0

      For d > 2g - 2, the Euler characteristic of the Serre dual of a line bundle is non-positive.

      source
      theorem RiemannRochApplications.high_degree_exact_rr (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : β„€) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) (h1_zero : SD.h1 = 0) :
      SD.h0 = d + 1 - C.g

      In the high-degree case where h^1 = 0, Riemann–Roch is exact: h^0(L) = d + 1 - g.

      source
      theorem RiemannRochApplications.high_degree_has_sections (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : β„€) (hd : d β‰₯ 2 * C.g - 1) (_hg : C.g β‰₯ 0) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) (h1_zero : SD.h1 = 0) :
      SD.h0 β‰₯ C.g

      For d β‰₯ 2g - 1 (and h^1 = 0), h^0(L) β‰₯ g.

      source
      theorem RiemannRochApplications.very_high_degree_sections (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : β„€) (hd : d β‰₯ 2 * C.g) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) (h1_zero : SD.h1 = 0) :
      SD.h0 β‰₯ C.g + 1

      For d β‰₯ 2g, h^0(L) β‰₯ g + 1.

      source
      theorem RiemannRochApplications.genus_zero_chi_O (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) :
      C.Ο‡ (1, 0) = 1

      For a genus-0 curve (i.e., β„™ΒΉ), Ο‡(π’ͺ) = 1.

      source
      theorem RiemannRochApplications.genus_zero_deg_K (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) :
      C.degK = -2

      For a genus-0 curve, deg K = -2.

      source
      theorem RiemannRochApplications.genus_zero_point_chi (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) :
      C.Ο‡ (1, 1) = 2

      For a genus-0 curve, the Euler characteristic of π’ͺ(1) is 2.

      source
      theorem RiemannRochApplications.genus_zero_point_sections (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 1) (h1_zero : SD.h1 = 0) :
      SD.h0 = 2

      On a genus-0 curve, h^0(π’ͺ(1)) = 2 (the two sections defining the projective embedding).

      source
      theorem RiemannRochApplications.genus_zero_gives_map_to_P1 (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) :
      C.Ο‡ (1, 1) = 2 ∧ C.degK - 1 < 0

      For a genus-0 curve, the degree-1 line bundle provides a map to β„™ΒΉ, realised by Ο‡(π’ͺ(1)) = 2 together with vanishing of the Serre dual.

      source
      theorem RiemannRochApplications.genus_zero_sections (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 0) (d : β„€) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) (h1_zero : SD.h1 = 0) :
      SD.h0 = d + 1

      For a genus-0 curve and any d, when h^1 = 0, h^0(L(d)) = d + 1.

      source
      theorem RiemannRochApplications.elliptic_chi_O (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 1) :
      C.Ο‡ (1, 0) = 0

      For an elliptic curve (genus 1), Ο‡(π’ͺ) = 0.

      source
      theorem RiemannRochApplications.elliptic_K_trivial (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 1) :
      C.degK = 0

      For an elliptic curve, deg K = 0 (the canonical bundle is trivial).

      source
      theorem RiemannRochApplications.elliptic_chi (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 1) (d : β„€) :
      C.Ο‡ (1, d) = d

      For an elliptic curve, the Euler characteristic of a line bundle of degree d is d.

      source
      theorem RiemannRochApplications.elliptic_sections (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 1) (d : β„€) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) (h1_zero : SD.h1 = 0) :
      SD.h0 = d

      For an elliptic curve with h^1 = 0, h^0(L) = d.

      source
      theorem RiemannRochApplications.elliptic_cubic_embedding (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 1) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 3) (h1_zero : SD.h1 = 0) :
      SD.h0 = 3

      An elliptic curve embeds as a smooth cubic in β„™Β² via a degree-3 line bundle: h^0(π’ͺ(3)) = 3.

      source
      theorem RiemannRochApplications.genus2_deg_K (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 2) :
      C.degK = 2

      For a genus-2 curve, deg K = 2.

      source
      theorem RiemannRochApplications.genus2_canonical_sections (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 2) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 C.degK) (hSD_h1 : SD.h1 = 1) :
      SD.h0 = 2

      For a genus-2 curve, h^0(K_C) = 2.

      source
      theorem RiemannRochApplications.genus2_high_degree (C : CanonicalSheafCurves.SmoothCompleteCurve) (hg : C.g = 2) (d : β„€) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) (h1_zero : SD.h1 = 0) :
      SD.h0 = d - 1

      For a genus-2 curve and high degree (so h^1 = 0), h^0(L) = d - 1.

      source
      theorem RiemannRochApplications.P1_verify_H0_structure (k : Type) [Field k] :
      Module.finrank k (SheafCohomology.H0 k 0) = 1

      Verification: on β„™ΒΉ, dim H^0(π’ͺ) = 1.

      source
      theorem RiemannRochApplications.P1_verify_H1_structure (k : Type) [Field k] :
      Module.finrank k (SheafCohomology.H1 k 0) = 0

      Verification: on β„™ΒΉ, dim H^1(π’ͺ) = 0.

      source
      theorem RiemannRochApplications.P1_verify_euler_char_O (k : Type) [Field k] :
      ↑(Module.finrank k (SheafCohomology.H0 k 0)) - ↑(Module.finrank k (SheafCohomology.H1 k 0)) = 1

      Verification: on β„™ΒΉ, Ο‡(π’ͺ) = 1.

      source
      theorem RiemannRochApplications.P1_verify_serre_duality (k : Type) [Field k] (n : β„€) :
      Module.finrank k (SheafCohomology.H1 k n) = Module.finrank k (SheafCohomology.H0 k (-2 - n))

      Serre duality on β„™ΒΉ: dim H^1(π’ͺ(n)) = dim H^0(π’ͺ(-2 - n)).

      source
      theorem RiemannRochApplications.P1_verify_H0_degree1 (k : Type) [Field k] :
      Module.finrank k (SheafCohomology.H0 k 1) = 2

      On β„™ΒΉ, dim H^0(π’ͺ(1)) = 2.

      source
      theorem RiemannRochApplications.P1_verify_H1_degree1 (k : Type) [Field k] :
      Module.finrank k (SheafCohomology.H1 k 1) = 0

      On β„™ΒΉ, dim H^1(π’ͺ(1)) = 0.

      source
      theorem RiemannRochApplications.P1_verify_H0_nonneg (k : Type) [Field k] (n : β„€) (hn : 0 ≀ n) :
      ↑(Module.finrank k (SheafCohomology.H0 k n)) = n + 1

      On β„™ΒΉ, for n β‰₯ 0, dim H^0(π’ͺ(n)) = n + 1.

      source
      theorem RiemannRochApplications.P1_verify_H1_nonneg (k : Type) [Field k] (n : β„€) (hn : 0 ≀ n) :
      Module.finrank k (SheafCohomology.H1 k n) = 0

      On β„™ΒΉ, for n β‰₯ 0, dim H^1(π’ͺ(n)) = 0.

      source
      theorem RiemannRochApplications.P1_verify_H0_neg1 (k : Type) [Field k] :
      Module.finrank k (SheafCohomology.H0 k (-1)) = 0

      On β„™ΒΉ, dim H^0(π’ͺ(-1)) = 0.

      source
      theorem RiemannRochApplications.P1_verify_H1_neg2 (k : Type) [Field k] :
      Module.finrank k (SheafCohomology.H1 k (-2)) = 1

      On β„™ΒΉ, dim H^1(π’ͺ(-2)) = 1 (corresponding to the canonical bundle).

      source
      theorem RiemannRochApplications.P1_abstract_cech_consistency (k : Type) [Field k] (n : β„€) :
      (CanonicalSheafCurves.mkCurve 0).Ο‡ (1, n) = ↑(Module.finrank k (SheafCohomology.H0 k n)) - ↑(Module.finrank k (SheafCohomology.H1 k n))

      Consistency: for mkCurve 0 = β„™ΒΉ, the abstract Euler characteristic matches the Čech computation.

      source
      theorem RiemannRochApplications.P1_genus_consistency (k : Type) [Field k] :
      (CanonicalSheafCurves.mkCurve 0).g = ↑(Module.finrank k (SheafCohomology.H1 k 0))

      Consistency: the genus of mkCurve 0 = β„™ΒΉ equals dim H^1(π’ͺ).

      source
      theorem RiemannRochApplications.genus_from_euler_char (C : CanonicalSheafCurves.SmoothCompleteCurve) :
      C.g = 1 - C.Ο‡ (1, 0)

      The genus can be recovered from the structure sheaf's Euler characteristic: g = 1 - Ο‡(π’ͺ).

      source
      theorem RiemannRochApplications.degree_genus_formula (C : CanonicalSheafCurves.SmoothCompleteCurve) :
      C.degK + 2 = 2 * C.g

      Consequence of Cor 31 (Lec 25): deg K + 2 = 2g.

      source
      theorem RiemannRochApplications.riemann_inequality_from_SD (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : β„€) (SD : RiemannRochRiemannForm.SerreDualityCurve C 1 d) :
      d + 1 - C.g ≀ SD.h0

      The Riemann inequality from the Serre duality data: d + 1 - g ≀ h^0(L).

      source
      theorem RiemannRochApplications.serre_duality_euler_char (C : CanonicalSheafCurves.SmoothCompleteCurve) (d : β„€) :
      C.Ο‡ (1, d) + C.Ο‡ (1, C.degK - d) = 0

      Serre duality for the Euler characteristic: Ο‡(L) + Ο‡(K βŠ— L*) = 0.

      source
      theorem RiemannRochApplications.self_dual_chi_zero (C : CanonicalSheafCurves.SmoothCompleteCurve) :
      C.Ο‡ (1, C.g - 1) = 0

      For the self-dual class L = K^{1/2} (degree g - 1), the Euler characteristic is zero.

      source
      noncomputable def RiemannRochApplications.serreDualityO_fromDedekind {k : Type u_1} [Field k] (C : DedekindCurve k) :
      RiemannRochRiemannForm.SerreDualityCurve C.toSmoothCompleteCurve 1 0

      Serre duality package for π’ͺ derived from a Dedekind curve C with ddGenus providing h^1(π’ͺ).

      Instances For
        source
        noncomputable def RiemannRochApplications.serreDualityK_fromDedekind {k : Type u_1} [Field k] (C : DedekindCurve k) :
        RiemannRochRiemannForm.SerreDualityCurve C.toSmoothCompleteCurve 1 C.toSmoothCompleteCurve.degK

        Serre duality package for Ο‰_C derived from a Dedekind curve C.

        Instances For