Module

Exists_ell_mul_lt_mul_ell_of_degree_pos.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_ell_mul_lt_mul_ell_of_degree_pos

1 declaration indexed from sourceView source ↗

Module documentation

The Riemann--Roch dimension inequality for Tsen's argument

For a form of degree d in n > d variables, the number of coefficients of n functions with poles bounded by mD eventually exceeds the dimension of the space containing the evaluated form, even after allowing a fixed divisor E for its coefficients. This uses the existing function-field Riemann--Roch theorem, not a genus-growth assumption. See Stacks Project, Tag 03RD.

Imports1

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Ell_eq_degree_add_one_sub_genusFF_of_isAlgClosed_of_isSeparable

Imported by2

theorem

exists_ell_mul_lt_mul_ell_of_degree_pos

L25 ↗

AlgebraicCurve.exists_ell_mul_lt_mul_ell_of_degree_pos

Documentation

The variable-versus-equation count in Tsen's proof, for any positive-degree divisor D and any fixed coefficient divisor E.

Source context 2 commands

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

noncomputable section
namespace AlgebraicCurve

Lean source · statement

theorem exists_ell_mul_lt_mul_ell_of_degree_pos
    (K : Type*) [Field K] [IsAlgClosed K] {F : Type*} [Field F] [Algebra K F]
    (x : F) (hx : Transcendental K x)
    (hfin : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hsep : Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F)
    (D E : Divisor K F) (hD : 0 < D.degree)
    (n d : ℕ) (hd : 0 < d) (hdn : d < n) :
    ∃ m : ℕ, ell (d • (m • D) + E) < n * ell (m • D)

Module documentation

The Riemann--Roch dimension inequality for Tsen's argument

Declarations

exists_ell_mul_lt_mul_ell_of_degree_pos