NYLL
Module

RROpens_exists_forall_hasValue_forall_ord_nonneg.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.RROpens_exists_forall_hasValue_forall_ord_nonneg
11 declarations indexed from sourceView source ↗

Module documentation

RROpens exists forall has Value forall ord nonneg

Imports7
Imported by1

Declarations

theorem

ord_nonneg_of_mem'

L45 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Priv
variable {K : Type u} {F : Type v} [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'

L62 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Priv
variable {K : Type u} {F : Type v} [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

add'

L76 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd.AlgebraicCurve.Place.HasValue.add'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Priv
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open scoped _root_.AlgebraicCurve.Place.HasValue in
Lean source · statement
theorem HasValue.add' {g g' : F} {a a' : K} (h : v.HasValue g a) (h' : v.HasValue g' a') :
    v.HasValue (g + g') (a + a')
theorem

hasValue_zero_of_ord_pos'

L84 ↗
AlgebraicCurve.Place.hasValue_zero_of_ord_pos'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Priv
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValue_zero_of_ord_pos' {g : F} (hg0 : g ≠ 0) (hg : 0
  < v.ord g) :
    v.HasValue g 0
theorem

hasValue_sum'

L98 ↗
AlgebraicCurve.Place.hasValue_sum'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Priv
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValue_sum' {ι : Type*} (s : Finset ι) (f : ι → F) (a
  : ι → K)
    (h : ∀ i ∈ s, v.HasValue (f i) (a i)) :
    v.HasValue (∑ i ∈ s, f i) (∑ i ∈ s, a i)
theorem

finite_lSpace

L118 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd.AlgebraicCurve.RROpensInterpImpl.finite_lSpace
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensInterpImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finite_lSpace [IsAlgClosed K] [IsCurveOver K F] {Kc : Divisor K F} {g : ℕ}
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (P : Place K F) (D : Divisor K F) : Module.Finite K (LSpace D)
theorem

coeff_aux

L148 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd.AlgebraicCurve.RROpensInterpImpl.coeff_aux
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensInterpImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
open Classical in
Lean source · full declaration
theorem coeff_aux (n : ℕ) (P₀ : Place K F) (A : Finset (Place K F)) (w : Place K F) :
    (((n : ℤ) • Finsupp.single P₀ (1 : ℤ) - ∑ a ∈ A, Finsupp.single a (1 : ℤ) : Divisor K F) w)
      = (if P₀ = w then (n : ℤ) else 0) - (if w ∈ A then 1 else 0) := by
  rw [Finsupp.sub_apply, Finsupp.smul_apply, Finsupp.single_apply, Finsupp.finsetSum_apply]
  simp only [Finsupp.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero]
  rw [Finset.sum_ite_eq']
theorem

ell_aux

L155 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd.AlgebraicCurve.RROpensInterpImpl.ell_aux
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensInterpImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ell_aux [IsAlgClosed K] [IsCurveOver K F] {Kc : Divisor K F} {g : ℕ}
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (P₀ : Place K F) (A : Finset (Place K F)) (n : ℕ) (hA : A.card + 2 * g ≤ n + 1) :
    (ell (((n : ℤ)) • Finsupp.single P₀ (1 : ℤ) - ∑ a ∈ A, Finsupp.single a (1 : ℤ)) : ℤ)
      = n - A.card + 1 - g
theorem

exists_section_aux

L195 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd.AlgebraicCurve.RROpensInterpImpl.exists_section_aux
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensInterpImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_section_aux [IsAlgClosed K] [IsCurveOver K F] {Kc : Divisor K F} {g : ℕ}
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (E : Finset (Place K F)) (P₀ : Place K F) (hP₀ : P₀ ∉ E) (e : Place K F) (he : e ∈ E) :
    ∃ u : F, u ≠ 0 ∧ e.ord u = 0 ∧ (∀ e' ∈ E, e' ≠ e → 0 < e'.ord u) ∧
      ∀ w : Place K F, w ≠ P₀ → 0 ≤ w.ord u
theorem

exists_forall_hasValue_forall_ord_nonneg_impl

L268 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd.AlgebraicCurve.RROpensInterpImpl.exists_forall_hasValue_forall_ord_nonneg_impl
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
noncomputable section
open IsLocalRing Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RROpensInterpImpl
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_forall_hasValue_forall_ord_nonneg_impl [IsAlgClosed K] [IsCurveOver K F]
    (Kc : Divisor K F) (g : ℕ)
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (E : Finset (Place K F)) (c : Place K F → K) (hc : ∀ e ∈ E, c e ≠ 0)
    (P₀ : Place K F) (hP₀ : P₀ ∉ E) :
    ∃ h : F, h ≠ 0 ∧ (∀ e ∈ E, e.HasValue h (c e)) ∧
      ∀ v : Place K F, v ≠ P₀ → 0 ≤ v.ord h
theorem

exists_forall_hasValue_forall_ord_nonneg

L340 ↗
AlgebraicCurve.RROpens.exists_forall_hasValue_forall_ord_nonneg
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsAllHasValueAllOrd
universe u v
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.RROpens.exists_forall_hasValue_forall_ord_nonneg
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F] [IsAlgClosed K]
    [IsCurveOver K F] (Kc : Divisor K F) (g : ℕ)
    (hRR : ∀ D : Divisor K F, (ell D : ℤ) - ell (Kc - D) = Divisor.degree D + 1 - g)
    (E : Finset (Place K F)) (c : Place K F → K) (hc : ∀ e ∈ E, c e ≠ 0)
    (P₀ : Place K F) (hP₀ : P₀ ∉ E) :
    ∃ h : F, h ≠ 0 ∧ (∀ e ∈ E, e.HasValue h (c e)) ∧
      ∀ v : Place K F, v ≠ P₀ → 0 ≤ v.ord h

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