Function-field Riemann--Roch and Weil duality statements. The index formula, adelic duality and differential-space dimensions are compared.
The lower Riemann--Roch dimension bound for every divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]def RiemannInequality : PropThe Riemann index formula expressing specialty through the divisor degree and genus.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]def RiemannIndexFormula : PropAdelic Weil duality identifies specialty with the complementary canonical-divisor space.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]def WeilDualityAdelic : PropWeil duality expresses the Riemann--Roch defect as a complementary divisor-space dimension.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]def WeilDuality : PropThe differential-dual space has the dimension of the complementary canonical-divisor space.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]def WeilOmegaEllAgrees : PropThe function-field Riemann--Roch dimension formula with a nonzero differential.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]def FunctionFieldRiemannRoch : PropSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]theorem functionFieldRiemannRoch_of_riemann_and_duality
(hWD : WeilDuality K F) : FunctionFieldRiemannRoch K FSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]theorem weilDuality_of_riemannIndex_of_adelic
(hRI : RiemannIndexFormula K F) (hWD : WeilDualityAdelic K F) :
WeilDuality K F