Module

FunctionFieldRiemannRoch_of_isAlgClosed_of_isCurveOver.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.FunctionFieldRiemannRoch_of_isAlgClosed_of_isCurveOver

1 declaration indexed from sourceView source ↗

Module documentation

Function-field Riemann-Roch for an algebraic curve over an algebraically closed field.

Imports9

Imported by14

theorem

functionFieldRiemannRoch_of_isAlgClosed_of_isCurveOver

L46 ↗

AlgebraicCurve.functionFieldRiemannRoch_of_isAlgClosed_of_isCurveOver

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs
namespace FunctionFieldRiemannRoch_of_isAlgClosed_of_isCurveOver
attribute [-instance] AlgebraicCurve.Place.instIsPrimeCenter
  AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
  AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve

Lean source · statement

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

Module documentation

Declarations

functionFieldRiemannRoch_of_isAlgClosed_of_isCurveOver