Module

Canonical.lean

Nyll.AlgebraicCurves.Divisors.Canonical

5 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Canonical divisors, their divisor classes, and the genus obtained from the order of a nonzero differential.

Imports1

Nyll.AlgebraicCurves.Differentials.Order

Imported by80

class

HasCanonicalDivisor

L31 ↗

AlgebraicCurve.HasCanonicalDivisor

Documentation

Every nonzero differential has a divisor recording its order at every place.

Source context 4 commands

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]

Lean source · full declaration

class HasCanonicalDivisor : Prop where
  /-- A divisor exists whose coefficients are the orders of the given nonzero differential. -/
  exists_divisor : ∀ ω : Ω[F⁄K], ω ≠ 0 → ∃ D : Divisor K F,
    ∀ v : Place K F, D v = v.ordDifferential ω

def

canonicalDivisorOf

L37 ↗

AlgebraicCurve.canonicalDivisorOf

Documentation

A chosen divisor representing the orders of the given nonzero differential.

Source context 4 commands

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]

Lean source · statement

def canonicalDivisorOf [HasCanonicalDivisor (K := K) (F := F)]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) : Divisor K F

theorem

canonicalDivisorOf_apply

L41 ↗

AlgebraicCurve.canonicalDivisorOf_apply

Source context 4 commands

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]

Lean source · statement

theorem canonicalDivisorOf_apply [HasCanonicalDivisor (K := K) (F := F)]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) (v : Place K F) :
    canonicalDivisorOf hω v = v.ordDifferential ω

def

canonicalClass

L48 ↗

AlgebraicCurve.canonicalClass

Documentation

The divisor class of a chosen nonzero differential, or zero if no nonzero differential exists.

Source context 4 commands

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]

Lean source · statement

def canonicalClass (K F : Type*) [Field K] [Field F] [Algebra K F]
    [HasCanonicalDivisor (K := K) (F := F)] : Pic K F

def

genus

L56 ↗

AlgebraicCurve.genus

Documentation

The natural-number genus computed from the degree of a canonical divisor, or zero when all differentials vanish.

Source context 4 commands

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]

Lean source · statement

def genus (K F : Type*) [Field K] [Field F] [Algebra K F]
    [HasCanonicalDivisor (K := K) (F := F)] : ℕ

Module documentation

Differentials, residues, and divisor correspondences

Declarations

HasCanonicalDivisor

canonicalDivisorOf

canonicalDivisorOf_apply

canonicalClass

genus