ModuleGenusOneDivisors.lean
Nyll.AlgebraicCurves.Cohomology.RiemannRoch.GenusOneDivisors
4 declarations indexed from sourceView source ↗ Module documentation
Degree-one divisor classes in genus one
Riemann--Roch supplies a nonzero section of every degree-one divisor. Its effective divisor is a single place. The same dimension calculation proves uniqueness: a function with at most one simple pole must be constant.
Declarations
AlgebraicCurve.Divisor.exists_single_of_effective_degree_one
DocumentationAn effective divisor of degree one over an algebraically closed constant field is the divisor of a single place.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
[IsCurveOver K F]
AlgebraicCurve.ell_eq_one_of_genus_one_degree_one
DocumentationIn genus one, every degree-one divisor has exactly one independent section.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
[IsCurveOver K F]
variable [Algebra.EssFiniteType K F]
AlgebraicCurve.eq_of_single_sub_single_principal_of_genus_one
DocumentationTwo places on a genus-one function field cannot differ by a principal divisor unless they are the same place.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
[IsCurveOver K F]
variable [Algebra.EssFiniteType K F]
AlgebraicCurve.existsUnique_place_principal_sub_of_genus_one
DocumentationEvery degree-one divisor on a genus-one function field is linearly equivalent to exactly one place. Neither an effective representative nor its uniqueness is input.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
[IsCurveOver K F]
variable [Algebra.EssFiniteType K F]