NYLL
Module

Exists_mem_riemannRochSpace_forall_hasValue_mul_of_exists_not_mem.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_forall_hasValue_mul_of_exists_not_mem
14 declarations indexed from sourceView source ↗

Module documentation

Exists mem riemann Roch Space forall has Value mul of exists not mem

Imports4
Imported by1

Declarations

theorem

ord_nonneg_of_mem

L38 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.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.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_nonneg_of_mem (v : Place K F) {f : F} (hf : f ≠ 0) (h : f ∈ v.toValuationSubring) :
    0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L42 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.mem_of_ord_nonneg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_of_ord_nonneg (v : Place K F) {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
theorem

hasValue_zero_of_ord_pos

L50 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.hasValue_zero_of_ord_pos
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hasValue_zero_of_ord_pos (v : Place K F) {f : F} (h : f = 0 ∨ 0 < v.ord f) :
    v.HasValue f 0
theorem

hasValue_zero

L67 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.hasValue_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hasValue_zero (v : Place K F) : v.HasValue (0 : F) 0
theorem

hvAdd

L70 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.hvAdd
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hvAdd {v : Place K F} {f g : F} {a b : K} (hf : v.HasValue f a) (hg : v.HasValue g b) :
    v.HasValue (f + g) (a + b)
theorem

hvSmul

L78 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.hvSmul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hvSmul {v : Place K F} {f : F} {a : K} (c : K) (hf : v.HasValue f a) :
    v.HasValue (c • f) (c * a)
theorem

hvSum

L83 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.hvSum
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hvSum {v : Place K F} {ι : Type*} (s : Finset ι) (f : ι → F) (b : ι → K)
    (h : ∀ j ∈ s, v.HasValue (f j) (b j)) :
    v.HasValue (∑ j ∈ s, f j) (∑ j ∈ s, b j)
theorem

riemannRochSpace_mono

L94 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.riemannRochSpace_mono
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem riemannRochSpace_mono {D D' : Divisor K F} (h : D ≤ D') :
    riemannRochSpace D ≤ riemannRochSpace D'
theorem

ne_zero_and_ord_add_eq_zero

L103 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.ne_zero_and_ord_add_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ne_zero_and_ord_add_eq_zero {D : Divisor K F} {f : F} {w : Place K F}
    (hf : f ∈ riemannRochSpace D) (hf' : f ∉ riemannRochSpace (D - Finsupp.single w 1)) :
    f ≠ 0 ∧ w.ord f + D w = 0
theorem

exists_mem_riemannRochSpace_not_mem_of_finrank_lt

L124 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.exists_mem_riemannRochSpace_not_mem_of_finrank_lt
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_mem_riemannRochSpace_not_mem_of_finrank_lt {D D' : Divisor K F}
    [FiniteDimensional K ↥(riemannRochSpace D')]
    (h : Module.finrank K ↥(riemannRochSpace D') < Module.finrank K ↥(riemannRochSpace D)) :
    ∃ p ∈ riemannRochSpace D, p ∉ riemannRochSpace D'
theorem

twist_mul_mem

L134 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.twist_mul_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem twist_mul_mem {E : Divisor K F} {v : Place K F} {t p : F} (ht0 : t ≠ 0) (ht : v.ord t = E v)
    (hp : p ∈ riemannRochSpace E) : t * p ∈ v.toValuationSubring
theorem

exists_hasValue_twist_mul

L144 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.exists_hasValue_twist_mul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_hasValue_twist_mul {E : Divisor K F} {v : Place K F} {t p : F}
    (hrat : Function.Surjective (algebraMap K v.ResidueField))
    (ht0 : t ≠ 0) (ht : v.ord t = E v) (hp : p ∈ riemannRochSpace E) :
    ∃ a : K, v.HasValue (t * p) a
theorem

surjective_algebraMap_residueField

L155 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul.AlgebraicCurve.EvalCount.surjective_algebraMap_residueField
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace EvalCount
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Closed
variable [IsAlgClosed K] [IsCurveOver K F]
Lean source · statement
theorem surjective_algebraMap_residueField (v : Place K F) :
    Function.Surjective (algebraMap K v.ResidueField)
theorem

exists_mem_riemannRochSpace_forall_hasValue_mul_of_exists_not_mem

L165 ↗
AlgebraicCurve.exists_mem_riemannRochSpace_forall_hasValue_mul_of_exists_not_mem
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllHasValueMul
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.exists_mem_riemannRochSpace_forall_hasValue_mul_of_exists_not_mem
    {k F : Type*} [Field k] [IsAlgClosed k] [Field F] [Algebra k F] [IsCurveOver k F]
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (E : Divisor k F) (v : ι → Place k F) (hv : Function.Injective v) (t : ι → F)
    (ht : ∀ i, t i ≠ 0 ∧ (v i).ord (t i) = E (v i))
    (hstep : ∀ i, ∃ g ∈ riemannRochSpace (E - ∑ j ∈ Finset.univ.erase i, Finsupp.single (v j) 1),
      g ∉ riemannRochSpace (E - ∑ j, Finsupp.single (v j) 1))
    (c : ι → k) :
    ∃ p ∈ riemannRochSpace E, ∀ i, (v i).HasValue (t i * p) (c i)

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