Module

FunctionFieldRiemannRoch_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FunctionFieldRiemannRoch_of_isAlgClosed

1 declaration indexed from sourceView source ↗

Module documentation

Function-field Riemann-Roch over an algebraically closed constant field, using the residue theorem.

Imports12

Imported by5

theorem

functionFieldRiemannRoch_of_isAlgClosed

L36 ↗

AlgebraicCurve.functionFieldRiemannRoch_of_isAlgClosed

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FunctionFieldRiemannRoch_of_isAlgClosed

Lean source · statement

theorem _root_.AlgebraicCurve.functionFieldRiemannRoch_of_isAlgClosed
    {K F : Type*} [Field K] [IsAlgClosed K]
    [Field F] [Algebra K F]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra.IsIntegral (RatFunc K) F]
    [AlgebraicCurve.HasLocalResidue K F]
    [∀ w : AlgebraicCurve.Place K F, w.FiniteResidue]
    [Nontrivial Ω[F⁄K]]
    [AlgebraicCurve.IsCurveOver K (RatFunc K)]
    [∀ u : AlgebraicCurve.Place K (RatFunc K), u.FiniteResidue]
    [AlgebraicCurve.HasCanonicalLocalResidueKStar K F]
    [Algebra.IsSeparable (RatFunc K) F]
    [Nontrivial Ω[(RatFunc K)⁄K]] [∀ v : AlgebraicCurve.Place K (RatFunc K), v.DCoordGenerates]
    [FiniteDimensional (RatFunc K) F] [AlgebraicCurve.HasSeparableResidue K F] :
    AlgebraicCurve.FunctionFieldRiemannRoch K F

Module documentation

Declarations

functionFieldRiemannRoch_of_isAlgClosed