Module

Ell_eq_zero_of_degree_neg.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_eq_zero_of_degree_neg

8 declarations indexed from sourceView source ↗

Module documentation

A divisor of negative degree has no nonzero Riemann--Roch sections.

Imports4

Imported by11

theorem

ord_nonneg_of_mem

L33 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {f : F} (hf : f ∈
    v.toValuationSubring) : 0 ≤ v.ord f

theorem

mem_of_ord_nonneg

L49 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord
    f) :
    f ∈ v.toValuationSubring

theorem

mem_iff_ord_nonneg

L58 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg.AlgebraicCurve.Place.mem_iff_ord_nonneg

Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

theorem

degree_eq_sum_support

L72 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg.AlgebraicCurve.Divisor.degree_eq_sum_support

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem Divisor.degree_eq_sum_support (D : Divisor K F) :
    Divisor.degree D = ∑ v ∈ D.support, D v * (v.deg : ℤ)

theorem

degree_nonneg_of_nonneg

L78 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg.AlgebraicCurve.Divisor.degree_nonneg_of_nonneg

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}
open scoped _root_.AlgebraicCurve.Divisor in

Lean source · statement

theorem Divisor.degree_nonneg_of_nonneg [IsCurveOver K F]
    {D : Divisor K F} (hD : ∀ v, 0 ≤ D v) : 0 ≤ Divisor.degree D

theorem

lSpace_eq_bot_of_degree_neg

L82 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg.AlgebraicCurve.lSpace_eq_bot_of_degree_neg

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem lSpace_eq_bot_of_degree_neg [IsCurveOver K F]
    (hD : Divisor.degree D < 0) : LSpace D = ⊥

theorem

ell_eq_zero_of_degree_neg_port

L98 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg.AlgebraicCurve.ell_eq_zero_of_degree_neg_port

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Ell_eq_zero_of_degree_neg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {D : Divisor K F}

Lean source · statement

theorem ell_eq_zero_of_degree_neg_port [IsCurveOver K F] (hD : Divisor.degree D < 0) :
    ell D = 0

theorem