Effective parts of curve divisors

DefinitionZero part of a divisor#✓fully proved

For a divisor \(D\) on a set of points \(C\), the zero part \(D^+\) of \(D\) is the divisor on \(C\) whose coefficient at each point \(P \in C\) is \(\max(D(P), 0)\).

noncomputable def divZeros (D : CurveDivisor C) : CurveDivisor C :=
  D⁺

Uses 1 · Used by 3

Statement usesDivisors on a curve

Used byCoefficients of the zero part · The zero part of a divisor is effective · A divisor is its zero part minus its pole part

DefinitionPole part of a divisor#✓fully proved

For a divisor \(D\) on a set of points \(C\), the pole part \(D^-\) of \(D\) is the divisor on \(C\) whose coefficient at each point \(P \in C\) is \(\max(-D(P), 0)\).

noncomputable def divPoles (D : CurveDivisor C) : CurveDivisor C :=
  D⁻

Uses 1 · Used by 3

Statement usesDivisors on a curve

Used byCoefficients of the pole part · The pole part of a divisor is effective · A divisor is its zero part minus its pole part

TheoremCoefficients of the zero part#✓fully proved

For every divisor \(D\) on a set of points \(C\) and every point \(P \in C\), the coefficient at \(P\) of the zero part \(D^+\) of \(D\) is \(\max(D(P), 0)\).

@[simp]
theorem divZeros_apply (D : CurveDivisor C) (P : C) :
    divZeros D P = max (D P) 0

Uses 2

Statement usesDivisors on a curve · Zero part of a divisor

TheoremCoefficients of the pole part#✓fully proved

For every divisor \(D\) on a set of points \(C\) and every point \(P \in C\), the coefficient at \(P\) of the pole part \(D^-\) of \(D\) is \(\max(-D(P), 0)\).

@[simp]
theorem divPoles_apply (D : CurveDivisor C) (P : C) :
    divPoles D P = max (-(D P)) 0

Uses 2

Statement usesDivisors on a curve · Pole part of a divisor

TheoremThe zero part of a divisor is effective#✓fully proved

For every divisor \(D\) on a set of points \(C\), the zero part \(D^+\) of \(D\) is effective: \(D^+(P) \ge 0\) for every point \(P \in C\).

@[simp]
theorem divZeros_nonneg (D : CurveDivisor C) : 0 ≤ divZeros D

Uses 2

Statement usesDivisors on a curve · Zero part of a divisor

TheoremThe pole part of a divisor is effective#✓fully proved

For every divisor \(D\) on a set of points \(C\), the pole part \(D^-\) of \(D\) is effective: \(D^-(P) \ge 0\) for every point \(P \in C\).

@[simp]
theorem divPoles_nonneg (D : CurveDivisor C) : 0 ≤ divPoles D

Uses 2

Statement usesDivisors on a curve · Pole part of a divisor

TheoremA divisor is its zero part minus its pole part#✓fully proved

For every set of points \(C\) and every divisor \(D\) on \(C\), let \(D^+\) be its zero part, with coefficient \(\max(D(P), 0)\) at each point \(P\), and \(D^-\) its pole part, with coefficient \(\max(-D(P), 0)\) at each point \(P\). Then \(D^+ - D^- = D\).

@[simp]
theorem divZeros_sub_divPoles (D : CurveDivisor C) :
    divZeros D - divPoles D = D

Uses 3

Statement usesDivisors on a curve · Pole part of a divisor · Zero part of a divisor

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.