Divisors on a curve

AbbreviationDivisors on a curve#✓fully proved

For a set \(C\) (the points of a curve), a divisor on \(C\) is a finitely supported function \(D \colon C \to \mathbb{Z}\). Its support is the finite set of points \(P \in C\) with \(D(P) \neq 0\).

abbrev CurveDivisor (C : Type*) := C →₀ ℤ

Used by 14

Used byCoefficient of a divisor at a point · Pole part of a divisor · Coefficients of the pole part · The pole part of a divisor is effective · Zero part of a divisor · Coefficients of the zero part · The zero part of a divisor is effective · A divisor is its zero part minus its pole part · Evaluation of a divisor against a function · Evaluation is multiplicative · Evaluation is a product over the support · Evaluation of divisors as a group homomorphism · The zero divisor evaluates to one · Evaluation of an integer multiple

DefinitionCoefficient of a divisor at a point#✓fully proved

For a divisor \(D\) on a set of points \(C\) and a point \(P \in C\), the coefficient of \(D\) at \(P\) is the integer \(D(P)\).

def coeff (D : CurveDivisor C) (P : C) : ℤ := D P

Uses 1

Statement usesDivisors on a curve

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.