NYLL
Module

RROpens_exists_degree_eq_sub_one_and_ell_eq_zero.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_degree_eq_sub_one_and_ell_eq_zero
13 declarations indexed from sourceView source ↗

Module documentation

RROpens exists degree eq sub one and ell eq zero

Imports4
Imported by2

Declarations

theorem

adicValuation_algebraMap_eq_one

L46 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.adicValuation_algebraMap_eq_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Val
variable (v : Place K F)
Lean source · statement
theorem adicValuation_algebraMap_eq_one {c : K} (hc : c ≠ 0) : v.adicValuation (algebraMap K F c)
  = 1
theorem

mem_valuationSubring_of_adicValuation_le_one

L51 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.mem_valuationSubring_of_adicValuation_le_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Val
variable (v : Place K F)
Lean source · statement
theorem mem_valuationSubring_of_adicValuation_le_one {x : F} (hx : v.adicValuation x ≤ 1) :
    x ∈ v.toValuationSubring
theorem

ord_pos_of_adicValuation_lt_one

L75 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.ord_pos_of_adicValuation_lt_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Val
variable (v : Place K F)
Lean source · statement
theorem ord_pos_of_adicValuation_lt_one {f : F} (hf : f ≠ 0) (h : v.adicValuation f < 1) : 0 <
  v.ord f
theorem

adicValuation_lt_one_of_ord_pos

L80 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.adicValuation_lt_one_of_ord_pos
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Val
variable (v : Place K F)
Lean source · statement
theorem adicValuation_lt_one_of_ord_pos {f : F} (hf : f ≠ 0) (h : 0 < v.ord f) : v.adicValuation f
  < 1
theorem

degree_eq_sum

L89 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.degree_eq_sum
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Deg
Lean source · full declaration
theorem degree_eq_sum (D : Divisor K F) : Divisor.degree D = D.sum fun w n => n * (w.deg : ℤ) := by
  simp [Divisor.degree]
theorem

degree_pos_of_nonneg

L92 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.degree_pos_of_nonneg
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Deg
Lean source · statement
theorem degree_pos_of_nonneg {D : Divisor K F} (h : ∀ w, 0 ≤ D w) {v : Place K F} (hv : 0 < D v)
    (hdeg : ∀ w : Place K F, w.deg = 1) : 0 < Divisor.degree D
theorem

exists_pos_of_degree_eq_zero

L102 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.exists_pos_of_degree_eq_zero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Deg
Lean source · statement
theorem exists_pos_of_degree_eq_zero {D : Divisor K F} (h0 : Divisor.degree D = 0) {w : Place K F}
  (hw : D w < 0)
    (hdeg : ∀ w : Place K F, w.deg = 1) : ∃ z, 0 < D z
theorem

mem_lSpace_zero_iff

L121 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.mem_lSpace_zero_iff
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Constants
variable [IsAlgClosed K] [IsCurveOver K F]
omit [IsAlgClosed K] [IsCurveOver K F] in
Lean source · statement
theorem mem_lSpace_zero_iff {f : F} : f ∈ LSpace (0 : Divisor K F) ↔ ∀ w : Place K F,
  w.adicValuation f ≤ 1
theorem

constantsAreBase

L126 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.constantsAreBase
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Constants
variable [IsAlgClosed K] [IsCurveOver K F]
Lean source · statement
theorem constantsAreBase [Nonempty (Place K F)] : ConstantsAreBase K F
theorem

exists_zero_sub_const

L164 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.exists_zero_sub_const
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Inf
variable [IsAlgClosed K] [IsCurveOver K F]
Lean source · statement
theorem exists_zero_sub_const {f₀ : F} (hf₀ : f₀ ∉ LSpace (0 : Divisor K F)) (c : K) :
    ∃ z : Place K F, z.adicValuation (f₀ - algebraMap K F c) < 1
theorem

infinite_place

L186 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.infinite_place
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
section Inf
variable [IsAlgClosed K] [IsCurveOver K F]
Lean source · statement
theorem infinite_place {f₀ : F} (hf₀ : f₀ ∉ LSpace (0 : Divisor K F)) : Infinite (Place K F)
theorem

main

L204 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero.AlgebraicCurve.GenericVanishSol.main
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
noncomputable section
open _root_.AlgebraicCurve
open _root_.WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace GenericVanishSol
open _root_.AlgebraicCurve
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem main [IsAlgClosed K] [IsCurveOver K F] [Nonempty (Place K F)] (Kc : Divisor K F) (g : ℕ)
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g) :
    ∃ D : Divisor K F, Divisor.degree D = (g : ℤ) - 1 ∧ ell D = 0
theorem

exists_degree_eq_sub_one_and_ell_eq_zero

L285 ↗
AlgebraicCurve.RROpens.exists_degree_eq_sub_one_and_ell_eq_zero
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsDegreeSubOneEllZero
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
  ModularCurve.coeffMap_single
universe u v
open _root_.AlgebraicCurve AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.RROpens.exists_degree_eq_sub_one_and_ell_eq_zero
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] [IsAlgClosed K]
    [IsCurveOver K F] [Nonempty (Place K F)] (Kc : Divisor K F) (g : ℕ)
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g) :
    ∃ D : Divisor K F, Divisor.degree D = (g : ℤ) - 1 ∧ ell D = 0

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.