Evaluation of curve divisors

DefinitionEvaluation of divisors as a group homomorphism#✓fully proved

For a commutative group \(G\) and a function \(f : C \to G\), this is the monoid homomorphism from the group of divisors on \(C\), written multiplicatively, to \(G\) that sends a divisor \(D\) to the finite product \(\prod_{P \in \operatorname{supp} D} f(P)^{D(P)}\).

noncomputable def evalMonoidHom (f : C → G) : Multiplicative (CurveDivisor C) →* G where
  toFun D := D.toAdd.prod fun P n ↦ f P ^ n
  map_one' := by simp
  map_mul' D₁ D₂ :=
    Finsupp.prod_add_index' (fun P ↦ zpow_zero (f P))
      (fun P n₁ n₂ ↦ zpow_add (f P) n₁ n₂)

Uses 1 · Used by 4

Statement usesDivisors on a curve

Used byEvaluation of a divisor against a function · Evaluation is multiplicative · The zero divisor evaluates to one · Evaluation of an integer multiple

DefinitionEvaluation of a divisor against a function#✓fully proved

For a commutative group \(G\), a function \(f : C \to G\) and a divisor \(D\) on \(C\), the evaluation of \(D\) against \(f\) is the element \(f(D) = \prod_{P \in \operatorname{supp} D} f(P)^{D(P)}\) of \(G\).

noncomputable def eval (f : C → G) (D : CurveDivisor C) : G :=
  evalMonoidHom f (Multiplicative.ofAdd D)

Uses 2 · Used by 5

Statement usesDivisors on a curve · Evaluation of divisors as a group homomorphism

Used byEvaluation is multiplicative · Evaluation is a product over the support · Evaluation of a one-point divisor · The zero divisor evaluates to one · Evaluation of an integer multiple

TheoremEvaluation is a product over the support#✓fully proved

For a commutative group \(G\), every function \(f : C \to G\) and every divisor \(D\) on \(C\), the evaluation of \(D\) against \(f\) equals \(\prod_{P \in \operatorname{supp} D} f(P)^{D(P)}\), the product over the points in the support of \(D\).

theorem eval_eq_prod (f : C → G) (D : CurveDivisor C) :
    eval f D = D.prod (fun P n ↦ f P ^ n)

Uses 2 · Used by 1

Statement usesDivisors on a curve · Evaluation of a divisor against a function

Used byEvaluation of a one-point divisor

TheoremThe zero divisor evaluates to one#✓fully proved

For a commutative group \(G\) and every function \(f : C \to G\), the evaluation of the zero divisor on \(C\) against \(f\) is the identity element \(1\) of \(G\).

@[simp]
theorem eval_zero (f : C → G) : eval f (0 : CurveDivisor C) = 1

Uses 3

Statement usesDivisors on a curve · Evaluation of a divisor against a function

Proof usesEvaluation of divisors as a group homomorphism

TheoremEvaluation of a one-point divisor#✓fully proved

For a commutative group \(G\), every function \(f : C \to G\), every point \(P \in C\) and every integer \(n\), the divisor \(n \cdot P\), with coefficient \(n\) at \(P\) and \(0\) elsewhere, evaluates against \(f\) to \(f(P)^n\).

@[simp]
theorem eval_single (f : C → G) (P : C) (n : ℤ) :
    eval f (Finsupp.single P n) = f P ^ n

Uses 2

Statement usesEvaluation of a divisor against a function

Proof usesEvaluation is a product over the support

TheoremEvaluation is multiplicative#✓fully proved

For a commutative group \(G\), every function \(f : C \to G\) and all divisors \(D_1, D_2\) on \(C\), writing \(f(D)\) for the evaluation of a divisor \(D\) against \(f\), we have \(f(D_1 + D_2) = f(D_1) \, f(D_2)\).

@[simp]
theorem eval_add (f : C → G) (D₁ D₂ : CurveDivisor C) :
    eval f (D₁ + D₂) = eval f D₁ * eval f D₂

Uses 3

Statement usesDivisors on a curve · Evaluation of a divisor against a function

Proof usesEvaluation of divisors as a group homomorphism

TheoremEvaluation of an integer multiple#✓fully proved

For a commutative group \(G\), every function \(f : C \to G\), every integer \(n\) and every divisor \(D\) on \(C\), writing \(f(D)\) for the evaluation of \(D\) against \(f\), we have \(f(nD) = f(D)^n\).

@[simp]
theorem eval_zsmul (f : C → G) (n : ℤ) (D : CurveDivisor C) :
    eval f (n • D) = eval f D ^ n

Uses 3

Statement usesDivisors on a curve · Evaluation of a divisor against a function

Proof usesEvaluation of divisors as a group homomorphism

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.