Module

Exists_mem_riemannRochSpace_forall_adicValuation_sub_le_of_forall_omegaSpace.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_forall_adicValuation_sub_le_of_forall_omegaSpace

3 declarations indexed from sourceView source ↗

Module documentation

Exists mem riemann Roch Space forall adic Valuation sub le of forall omega Space

Imports3

Imported by1

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All

theorem

single_sum_apply_of_mem

L36 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllAdicValuation.AlgebraicCurve.Theta1Sol.single_sum_apply_of_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllAdicValuation
open WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Theta1Sol
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem single_sum_apply_of_mem (T : Finset (Place K F)) {v : Place K F} (hv : v ∈ T) :
    (∑ x ∈ T, Finsupp.single x (1 : ℤ)) v = 1

theorem

single_sum_apply_of_not_mem

L43 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllAdicValuation.AlgebraicCurve.Theta1Sol.single_sum_apply_of_not_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllAdicValuation
open WithZero
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Theta1Sol
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem single_sum_apply_of_not_mem (T : Finset (Place K F)) {v : Place K F} (hv : v ∉ T) :
    (∑ x ∈ T, Finsupp.single x (1 : ℤ)) v = 0

theorem

exists_mem_riemannRochSpace_forall_adicValuation_sub_le_of_forall_omegaSpace

L53 ↗

AlgebraicCurve.exists_mem_riemannRochSpace_forall_adicValuation_sub_le_of_forall_omegaSpace

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceAllAdicValuation
open WithZero
open _root_.AlgebraicCurve AlgebraicCurve in

Lean source · statement

theorem
  _root_.AlgebraicCurve.exists_mem_riemannRochSpace_forall_adicValuation_sub_le_of_forall_omegaSpace
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (D : AlgebraicCurve.Divisor K F) (T : Finset (AlgebraicCurve.Place K F)) (g :
      AlgebraicCurve.Place K F → F)
    (hg : ∀ x ∈ T, x.adicValuation (g x) ≤ exp (D x))
    (r : ↥(AlgebraicCurve.adeleSpace K F))
    (hrT : ∀ v ∈ T, (r : AlgebraicCurve.Place K F → F) v = g v) (hr0 : ∀ v ∉ T, (r :
      AlgebraicCurve.Place K F → F) v = 0)
    (horth : ∀ μ ∈ AlgebraicCurve.omegaSpace (K := K) (F := F) (D - ∑ x ∈ T, Finsupp.single x 1),
      μ r = 0) :
    ∃ f ∈ AlgebraicCurve.riemannRochSpace (K := K) (F := F) D,
      ∀ x ∈ T, x.adicValuation (f - g x) ≤ exp (D x - 1)

Module documentation

Exists mem riemann Roch Space forall adic Valuation sub le of forall omega Space

Declarations

single_sum_apply_of_mem

single_sum_apply_of_not_mem

exists_mem_riemannRochSpace_forall_adicValuation_sub_le_of_forall_omegaSpace