NYLL
Module

RROpens_exists_mem_riemannRochSpace_sub_hasValue_mul_zpow_neg_forall_hasValue.lean

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

Module documentation

RROpens exists mem riemann Roch Space sub has Value mul zpow neg forall has Value

Imports7
Imported by1

Declarations

theorem

hasValue_zero

L37 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.hasValue_zero
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hasValue_zero (v : Place K F) : v.HasValue (0 : F) 0
theorem

hasValue_add

L40 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.hasValue_add
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hasValue_add {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

hasValue_const_mul

L49 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.hasValue_const_mul
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hasValue_const_mul {v : Place K F} {f : F} {a : K} (hf : v.HasValue f a) (c : K) :
    v.HasValue (algebraMap K F c * f) (c * a)
theorem

hasValue_sum

L53 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.hasValue_sum
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hasValue_sum {ι : Type*} (v : Place K F) (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

hasValue_zero_of_one_le_ord

L63 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.hasValue_zero_of_one_le_ord
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem hasValue_zero_of_one_le_ord (v : Place K F) {f : F} (hf : f ≠ 0) (h : 1 ≤ v.ord f) :
  v.HasValue f 0
theorem

exists_hasValue_ne_zero

L74 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.exists_hasValue_ne_zero
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_hasValue_ne_zero (v : Place K F) (hv : v.IsRational) {f : F} (hf : f ≠ 0) (h :
  v.ord f = 0) :
    ∃ a : K, a ≠ 0 ∧ v.HasValue f a
theorem

isRational_of_isAlgClosed

L81 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.isRational_of_isAlgClosed
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isRational_of_isAlgClosed [IsAlgClosed K] [IsCurveOver K F] (v : Place K F) : v.IsRational
theorem

ord_ge_of_mem_lSpace

L87 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.ord_ge_of_mem_lSpace
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_ge_of_mem_lSpace {D : Divisor K F} {f : F} (hf : f ∈ LSpace D) (hf0 : f ≠ 0) (v :
  Place K F) :
    -D v ≤ v.ord f
theorem

ne_zero_of_notMem

L94 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.ne_zero_of_notMem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ne_zero_of_notMem {D : Divisor K F} {f : F} (hf : f ∉ LSpace D) : f ≠ 0
theorem

ord_eq_of_mem_of_notMem

L97 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas.InterpSol.ord_eq_of_mem_of_notMem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RROpensExistsMemRRSpaceSubHas
universe u v
open AlgebraicCurve IsLocalRing
namespace InterpSol
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_eq_of_mem_of_notMem {D : Divisor K F} {P : Place K F} {f : F}
    (hf : f ∈ LSpace D) (hf' : f ∉ LSpace (D - Finsupp.single P 1)) : P.ord f = -D P
theorem

exists_mem_riemannRochSpace_sub_hasValue_mul_zpow_neg_forall_hasValue

L122 ↗
AlgebraicCurve.RROpens.exists_mem_riemannRochSpace_sub_hasValue_mul_zpow_neg_forall_hasValue
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurve.RROpens
universe u v
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs in
open RROpensExistsMemRRSpaceSubHas.InterpSol in
Lean source · statement
theorem exists_mem_riemannRochSpace_sub_hasValue_mul_zpow_neg_forall_hasValue
    {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)
    (D : Divisor K F)
    (Z : Finset (Place K F)) (hZ : ∀ z ∈ Z, D z = 0) (c : Place K F → K)
    (P₀ : Place K F) (hP₀Z : P₀ ∉ Z) (hP₀D : D P₀ = 0)
    (x : F) (hx : P₀.ord x = 1) (m : ℕ) (c₀ : K)
    (hdeg : 2 * (g : ℤ) + m + Z.card ≤ Divisor.degree D) :
    ∃ f : F, f ∈ riemannRochSpace (D - Finsupp.single P₀ (m : ℤ)) ∧
      P₀.HasValue (f * x ^ (-(m : ℤ))) c₀ ∧ ∀ z ∈ Z, z.HasValue f (c z)

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