Module

Exists_forall_adicValuation_sub_le_of_riemannGenusReachedAt.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_forall_adicValuation_sub_le_of_riemannGenusReachedAt

2 declarations indexed from sourceView source ↗

Module documentation

Approximation with a prescribed valuation bound from a place where the Riemann genus is reached.

Imports9

Imported by4

theorem

strongApprox_aux

L36 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.Exists_forall_adicValuation_sub_le_of_riemannGenusReachedAt.AlgebraicCurve.strongApprox_aux

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace Exists_forall_adicValuation_sub_le_of_riemannGenusReachedAt
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem strongApprox_aux {K F : Type*} [Field K] [Field F] [Algebra K F] [IsCurveOver K F]
    [FiniteDimensional K ↥(LSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (h : RiemannGenusReachedAt γ D₀)
    (S : Set (Place K F)) {v₀ : Place K F} (hv₀ : v₀ ∉ S) (D : Divisor K F)
    (α : Place K F → F) (hα : {v | ¬ v.adicValuation (α v) ≤ WithZero.exp (D v)}.Finite) :
    ∃ f : F, ∀ v ∈ S, v.adicValuation (α v - f) ≤ WithZero.exp (D v)

theorem