AlgebraicCurve.omegaSpace_eq_bot_of_degree_canonicalDivisorOf_lt
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.OmegaSpaceBotDegreeCanonical
attribute [-instance]
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.omegaSpace_eq_bot_of_degree_canonicalDivisorOf_lt
{K F : Type*} [Field K] [Field F] [Algebra K F] [AlgebraicCurve.IsCurveOver K F] [Nonempty
(AlgebraicCurve.Place K F)]
[FiniteDimensional K ↥(AlgebraicCurve.LSpace (0 : AlgebraicCurve.Divisor K F))]
[AlgebraicCurve.HasCanonicalDivisor (K := K) (F := F)]
[∀ v : AlgebraicCurve.Place K F, v.DCoordGenerates]
[AlgebraicCurve.HasCanonicalLocalResidueKStar K F]
{γ : ℤ} {D₀ : AlgebraicCurve.Divisor K F} (h : AlgebraicCurve.RiemannGenusReachedAt γ D₀)
(hWK : AlgebraicCurve.WeilKaehlerAgree K F) {ω : Ω[F⁄K]} (hω : ω ≠ 0) (D :
AlgebraicCurve.Divisor K F)
[FiniteDimensional K ↥(AlgebraicCurve.omegaSpace (K := K) (F := F) D)]
(hdeg : AlgebraicCurve.Divisor.degree (AlgebraicCurve.canonicalDivisorOf hω) <
AlgebraicCurve.Divisor.degree D) :
AlgebraicCurve.omegaSpace (K := K) (F := F) D = ⊥