Module

Tsen.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Tsen

2 declarations indexed from sourceView source ↗

Module documentation

Tsen's theorem for separable one-variable function fields

A positive-degree homogeneous form with more variables than its degree has a nonzero zero over a finite separable extension of K(x), where K is algebraically closed.

The proof uses existing principal-divisor and Riemann--Roch results. It chooses bounded-pole functions as unknowns, bounds the resulting coefficients, and solves the coordinate equations over K by the Nullstellensatz dimension argument. Reference: Stacks Project, Theorem 59.67.10, Tag 03RD.

Imports6

Imported by2

theorem

finite_set_mem_lSpace

L32 ↗

AlgebraicCurve.finite_set_mem_lSpace

Source context 3 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicCurve

Lean source · statement

theorem finite_set_mem_lSpace
    {K F : Type*} [Field K] [Field F] [Algebra K F] [HasPrincipalDivisors K F]
    (s : Finset F) : ∃ E : Divisor K F, ∀ a ∈ s, a ∈ LSpace E

theorem

exists_ne_zero_homogeneous_zero_of_transcendental_of_finiteDimensional

L49 ↗

AlgebraicCurve.exists_ne_zero_homogeneous_zero_of_transcendental_of_finiteDimensional

Documentation

Tsen's nontrivial-zero theorem, proved from the actual function-field Riemann--Roch theorem for a finite separable extension of K(x).