Evaluating a function on a divisor

For a function f and a divisor D whose support avoids the zeros and poles of f, the classical quantity

f(D) = ∏_{P ∈ supp D} N_{F_P/k}(f(P)) ^ (coeff D P)

is what Weil reciprocity f(div g) = g(div f) compares. This file defines it. The local factors N_{F_P/k}(f(P)) are TauCeti.Place.normResidueOrOne, built in FieldTheory/FunctionField/Place/Residue.lean.

The construction is total on Fˣ — every nonzero function, at every divisor — and classical where both the admissibility and the finiteness conditions below hold: at a place whose residue field is module-finite over k. TauCeti.Place.finiteDimensional_residueField supplies that at every place of an algebraic function field; absent it, Algebra.norm is the junk value 1 and the factor drops out silently, which is the convention TauCeti.Place.degree already follows (junk 0 under the same hypothesis). No result below is stated only in the classical regime — the divisor and function laws are formal and hold for every F.

Main definitions

• TauCeti.Divisor.eval: f(D), as a unit of k.
• TauCeti.Divisor.IsUnitAtSupport: the admissibility condition — f is a unit at every place of D. This is exactly disjointness of D from the divisor of f (isUnitAtSupport_iff_disjoint).

Main results

• TauCeti.Divisor.eval_add, eval_neg, eval_sub, eval_zero: f(-) is a homomorphism from the additive group of divisors to kˣ, unconditionally.
• TauCeti.Divisor.eval_eq_prod_normResidue: on an admissible divisor, the textbook product formula.
• TauCeti.Divisor.eval_one, eval_inv, eval_mul and eval_div: the group laws in the function variable. The bundled homomorphism supplies the divisor variable; these supply the other one, and the two together are the bilinearity Weil reciprocity is stated against. Note the asymmetry: eval_one and eval_inv need no hypothesis, while eval_mul and eval_div need admissibility for both arguments.
• Admissibility is a subgroup condition in each variable, which is what makes those laws usable together: isUnitAtSupport_one, IsUnitAtSupport.mul, isUnitAtSupport_inv_iff and IsUnitAtSupport.div in the function, and isUnitAtSupport_zero, IsUnitAtSupport.add, isUnitAtSupport_neg_iff and IsUnitAtSupport.sub in the divisor. The divisor side is what moving a divisor within its class to obtain disjoint support needs.

Implementation notes

Three choices are load-bearing, and each rules out an alternative that does not work.

Functions are taken in Fˣ, not F. The admissibility condition is P.ord f = 0, and P.ord 0 = 0 by the junk-value convention on ord; so over F the condition would declare f = 0 admissible at every place. Taking f : Fˣ excludes that, and it matches TauCeti.Divisor.principal, which is already stated for Fˣ.

Values are taken in kˣ, not k, and the neutral value is 1, not 0. The coefficient of a place is an integer, so the local factor is raised to a possibly negative power, and the divisor law has to survive that. With 0 as the neutral value in k it does not: at a place where f is not a unit, eval (single P 1) * eval (single P (-1)) would be 0 while eval 0 = 1. In kˣ every zpow identity holds unconditionally and the law is automatic.

The definition is total, with admissibility carried by the theorems. Admissibility depends on the divisor, so a definition that demanded it could not be a homomorphism on the divisor group: it would be one on the subgroup of divisors admissible for that particular f — a domain that shrinks with each f, which IsUnitAtSupport.zero, .add, isUnitAtSupport_neg_iff and .sub below describe. Instead Place.normResidueOrOne is total, eval is a homomorphism on the whole group, and eval_eq_prod_normResidue recovers the textbook formula wherever admissibility holds.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8 — evaluation of a function on a divisor of disjoint support is the prerequisite of the divisor construction of the Weil pairing given there (III.8.1).

noncomputable def TauCeti.Divisor.eval {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (f : Fˣ) : kˣ

The value f(D) of a function on a divisor.

Two conditions separate this from the classical quantity, and both have to hold. f must be a unit at every place of D (TauCeti.Divisor.IsUnitAtSupport): the local factor is total, so at a zero or pole of f it is 1 rather than a norm, and that factor silently disappears. And every residue field involved must be module-finite over k, or Algebra.norm degenerates to 1 for the same reason (Algebra.norm_eq_one_of_not_module_finite). TauCeti.Place.finiteDimensional_residueField supplies the second at every place of an algebraic function field, so in the intended setting only admissibility is a real hypothesis — but it is one. See TauCeti.Place.normResidue for the full statement of the finiteness convention, which is the one TauCeti.Place.degree already follows.

Equations

• D.eval f = (TauCeti.Divisor.evalHom✝ f) (Multiplicative.ofAdd D)

theorem TauCeti.Divisor.eval_eq_finsuppProd {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (f : Fˣ) : D.eval f = Finsupp.prod D fun (P : Place k F) (n : ℤ) => P.normResidueOrOne f ^ n

f(D) is the product over the support of the local factors, each raised to its coefficient.

@[simp]

theorem TauCeti.Divisor.eval_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (f : Fˣ) : eval 0 f = 1

f(0) = 1: the empty product.

@[simp]

theorem TauCeti.Divisor.eval_add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (f : Fˣ) : (D + E).eval f = D.eval f * E.eval f

f(D + E) = f(D) · f(E): adding divisors multiplies values.

@[simp]

theorem TauCeti.Divisor.eval_neg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (f : Fˣ) : (-D).eval f = (D.eval f)⁻¹

f(-D) = f(D)⁻¹: negating a divisor inverts the value.

@[simp]

theorem TauCeti.Divisor.eval_sub {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) (f : Fˣ) : (D - E).eval f = D.eval f / E.eval f

f(D - E) = f(D) / f(E).

@[simp]

theorem TauCeti.Divisor.eval_zpow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (f : Fˣ) (n : ℤ) : D.eval (f ^ n) = D.eval f ^ n

Raising the function to a power raises the value to that power: f ^ n (D) = f(D) ^ n. Like eval_inv, and unlike eval_mul, this needs no admissibility hypothesis.

@[simp]

theorem TauCeti.Divisor.eval_zsmul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (n : ℤ) (D : Divisor k F) (f : Fˣ) : (n • D).eval f = D.eval f ^ n

Scaling a divisor raises the value to that power: f(n • D) = f(D) ^ n. This is what the N(P) − N(O) divisors of the Weil pairing are evaluated through.

@[simp]

theorem TauCeti.Divisor.eval_single {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℤ) (f : Fˣ) : eval (Finsupp.single P n) f = P.normResidueOrOne f ^ n

On a single place with multiplicity, f(n·P) is the local factor raised to n.

def TauCeti.Divisor.IsUnitAtSupport {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (f : Fˣ) : Prop

f is a unit at every place of D — the condition under which no local factor is replaced by 1, and the one Weil reciprocity is stated against. It is what makes f(D) a product of genuine norms; those norms are the classical ones under the separate finiteness condition recorded on TauCeti.Divisor.eval.

Equations

• D.IsUnitAtSupport f = ∀ P ∈ D.support, P.ord ↑f = 0

@[simp]

theorem TauCeti.Divisor.isUnitAtSupport_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : Fˣ} : D.IsUnitAtSupport f ↔ ∀ P ∈ D.support, P.ord ↑f = 0

IsUnitAtSupport D f is exactly the pointwise condition P.ord f = 0 at every place of D, in both directions.

theorem TauCeti.Divisor.eval_eq_prod_normResidue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : Fˣ} (h : D.IsUnitAtSupport f) : D.eval f = ∏ P : ↥D.support, (↑P).normResidue f ⋯ ^ AlgebraicGeometry.WeilDivisor.coeff D ↑P

On an admissible divisor, f(D) is the product ∏ N(f(P)) ^ n_P of local norms. This is the textbook formula when the residue fields are module-finite over k, which TauCeti.Place.finiteDimensional_residueField gives for an algebraic function field; without that the factors are Algebra.norm's junk value and the identity still holds, but of the formal product rather than of the classical one.

theorem TauCeti.Divisor.isUnitAtSupport_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (f : Fˣ) : IsUnitAtSupport 0 f

Every function is admissible for the zero divisor, which has empty support.

theorem TauCeti.Divisor.IsUnitAtSupport.add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {f : Fˣ} (hD : D.IsUnitAtSupport f) (hE : E.IsUnitAtSupport f) : (D + E).IsUnitAtSupport f

Admissibility is closed under sums of divisors: (D + E).support ⊆ D.support ∪ E.support.

theorem TauCeti.Divisor.isUnitAtSupport_neg_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : Fˣ} : (-D).IsUnitAtSupport f ↔ D.IsUnitAtSupport f

Admissibility is invariant under negating the divisor, not merely closed under it: (-D).support = D.support.

theorem TauCeti.Divisor.IsUnitAtSupport.sub {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} {f : Fˣ} (hD : D.IsUnitAtSupport f) (hE : E.IsUnitAtSupport f) : (D - E).IsUnitAtSupport f

Admissibility is closed under differences of divisors.

theorem TauCeti.Divisor.isUnitAtSupport_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : D.IsUnitAtSupport 1

1 is admissible for every divisor.

theorem TauCeti.Divisor.IsUnitAtSupport.mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f g : Fˣ} (hf : D.IsUnitAtSupport f) (hg : D.IsUnitAtSupport g) : D.IsUnitAtSupport (f * g)

Admissibility is closed under products of functions.

theorem TauCeti.Divisor.IsUnitAtSupport.zsmul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : Fˣ} (hf : D.IsUnitAtSupport f) (n : ℤ) : (n • D).IsUnitAtSupport f

Admissibility is closed under scaling the divisor: n • D has no places D does not.

theorem TauCeti.Divisor.isUnitAtSupport_inv_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : Fˣ} : D.IsUnitAtSupport f⁻¹ ↔ D.IsUnitAtSupport f

Admissibility is invariant under inversion, not merely closed under it: ord_P f⁻¹ vanishes exactly when ord_P f does.

theorem TauCeti.Divisor.IsUnitAtSupport.zpow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f : Fˣ} (hf : D.IsUnitAtSupport f) (n : ℤ) : D.IsUnitAtSupport (f ^ n)

Admissibility is closed under integer powers of the function.

theorem TauCeti.Divisor.IsUnitAtSupport.div {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f g : Fˣ} (hf : D.IsUnitAtSupport f) (hg : D.IsUnitAtSupport g) : D.IsUnitAtSupport (f / g)

Admissibility is closed under quotients of functions.

theorem TauCeti.Divisor.eval_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f g : Fˣ} (hf : D.IsUnitAtSupport f) (hg : D.IsUnitAtSupport g) : D.eval (f * g) = D.eval f * D.eval g

f(D) is multiplicative in the function, on a divisor admissible for both factors: (f g)(D) = f(D) · g(D). This is the half of the divisor/function bilinearity that the bundled homomorphism behind eval does not give for free: it is a homomorphism in D, and this is the statement in f.

Both hypotheses are needed. At a place where f and g have opposite nonzero orders their product is a unit while neither factor is, so the left side sees a genuine norm there and the right side sees 1 twice.

@[simp]

theorem TauCeti.Divisor.eval_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) : D.eval 1 = 1

f(D) at the constant function 1, needing no hypothesis.

@[simp]

theorem TauCeti.Divisor.eval_inv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) (f : Fˣ) : D.eval f⁻¹ = (D.eval f)⁻¹

f(D) inverts with no hypothesis, unlike eval_mul: admissibility is invariant under inversion (isUnitAtSupport_inv_iff), and off the admissible places both sides are 1.

theorem TauCeti.Divisor.eval_div {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} {f g : Fˣ} (hf : D.IsUnitAtSupport f) (hg : D.IsUnitAtSupport g) : D.eval (f / g) = D.eval f / D.eval g

f(D) respects quotients of functions, on a divisor admissible for both. Like eval_mul and unlike eval_inv, this needs both hypotheses: f / g can be admissible where neither f nor g is.

theorem TauCeti.Divisor.isUnitAtSupport_iff_disjoint {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) (f : Fˣ) : D.IsUnitAtSupport f ↔ Disjoint D.support (principal hF f).support

Admissibility is disjointness from the divisor of f. This is the form the Weil-reciprocity statement uses, where the two divisors are the principal divisors of the two functions.