AlgebraicCurve.weilOfKaehler_mem_omegaSpace_of_residueTheorem
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehlerMemOmegaSpace
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.weilOfKaehler_mem_omegaSpace_of_residueTheorem {K F : Type*} [Field
K] [Field F] [Algebra K F] [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F
:= F)] [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]] [HasPrincipalDivisors K F]
(hRT : ResidueTheorem K F) {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
weilOfKaehler K F hω ∈ omegaSpace (canonicalDivisorOf hω)