NYLL
Module

Finrank_add_card_le_of_forall_exists_mem_riemannRochSpace_hasValue_mul.lean

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

Module documentation

Finrank add card le of forall exists mem riemann Roch Space has Value mul

Imports4
Imported by1

Declarations

theorem

ord_nonneg_of_mem

L38 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.AlgebraicCurve.EvalCount.hvAdd
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.AlgebraicCurve.EvalCount.hvSmul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.AlgebraicCurve.EvalCount.hvSum
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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.FinrankAddCardLeAllExistsMemRR.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.FinrankAddCardLeAllExistsMemRR
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

finrank_add_card_le_of_forall_exists_mem_riemannRochSpace_hasValue_mul

L165 ↗
AlgebraicCurve.finrank_add_card_le_of_forall_exists_mem_riemannRochSpace_hasValue_mul
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankAddCardLeAllExistsMemRR
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.finrank_add_card_le_of_forall_exists_mem_riemannRochSpace_hasValue_mul
    {k F : Type*} [Field k] [IsAlgClosed k] [Field F] [Algebra k F] [IsCurveOver k F]
    {ι : Type*} [Fintype ι]
    (E₁ E₂ : Divisor k F)
    [FiniteDimensional k ↥(riemannRochSpace E₁)] [FiniteDimensional k ↥(riemannRochSpace E₂)]
    (v₁ v₂ : ι → Place k F) (t₁ t₂ : ι → F)
    (ht₁ : ∀ i, t₁ i ≠ 0 ∧ (v₁ i).ord (t₁ i) = E₁ (v₁ i))
    (ht₂ : ∀ i, t₂ i ≠ 0 ∧ (v₂ i).ord (t₂ i) = E₂ (v₂ i))
    (lam : ι → k)
    (hsurj : ∀ c : ι → k, ∃ p ∈ riemannRochSpace E₁, ∀ i, (v₁ i).HasValue (t₁ i * p) (c i))
    (T : Submodule k (F × F))
    (hT : ∀ p, p ∈ T ↔ p.1 ∈ riemannRochSpace E₁ ∧ p.2 ∈ riemannRochSpace E₂ ∧
      ∀ i, ∃ c : k, (v₁ i).HasValue (t₁ i * p.1) (lam i * c) ∧ (v₂ i).HasValue (t₂ i * p.2) c) :
    FiniteDimensional k ↥T ∧
      Module.finrank k ↥T + Fintype.card ι ≤
        Module.finrank k ↥(riemannRochSpace E₁) + Module.finrank k ↥(riemannRochSpace E₂)

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