The residue of a function at a place, and its norm to the constants

A function f that is a unit at a place P has a nonzero residue f(P) in the residue field F_P, and pushing that residue down to the constants k by the field norm gives a value that does not depend on P for its home. This file builds those two maps and extends the second by 1 to a total function of the place.

The norm is what makes a product over places possible at all: f(P) lives in F_P, which varies with P, so without a common target the factors of a product like Weil reciprocity's f(div g) would live in different fields.

The norm is the classical field norm exactly when F_P is finite over k. Algebra.norm is LinearMap.det of multiplication, so on a residue field that is not module-finite over k it takes Mathlib's junk value 1 (Algebra.norm_eq_one_of_not_module_finite), and then so does normResidue. That regime never arises where this API is meant to be used: over a function field every place has finite residue degree, by TauCeti.Place.finiteDimensional_residueField. The definitions below are stated without a finiteness hypothesis for the reason TauCeti.Place.degree is — the hypothesis would be unused in the term, since Algebra.norm does not consume one — so the guarantee is recorded here rather than in the signature.

Main definitions

• TauCeti.Place.residueUnit: the residue f(P) of a function that is a unit at P, as a unit of the residue field.
• TauCeti.Place.normResidue: the norm to k of that residue, as a unit of k.
• TauCeti.Place.normResidueOrOne: the same, extended by 1 at the places where f is not a unit, so that it is a total function of the place. Totality is what lets TauCeti.Divisor.eval be a homomorphism outright.

Main results

• TauCeti.Place.coe_residueUnit and TauCeti.Place.coe_normResidue: the underlying field values of the two units: IsLocalRing.residue and the Algebra.norm of it. Both are @[simp], and are named after TauCeti.Algebra.coe_normUnits, the adjacent lemma of the same shape.
• TauCeti.Place.normResidueOrOne_of_ord_eq_zero and TauCeti.Place.normResidueOrOne_of_ord_ne_zero: the two branches of the total extension.
• TauCeti.Place.ord_mul_eq_zero, ord_inv_eq_zero and ord_div_eq_zero (in Place/Basic.lean): admissibility is a subgroup condition on Fˣ. They are public because residueUnit carries its admissibility proof as an argument, so a law about f * g, f⁻¹ or f / g has to name a proof for the composite in its own left-hand side; these are those names. The identity case needs no such lemma — ((1 : Fˣ) : F) is 1 definitionally, so TauCeti.Place.ord_one already has the right type.
• The group laws in the function: residueUnit_one, residueUnit_mul, residueUnit_inv, residueUnit_div and their normResidue counterparts, together with normResidueOrOne_one, normResidueOrOne_mul, normResidueOrOne_inv and normResidueOrOne_div for the total form. Each partial law assumes only what its inputs need — residueUnit_one and normResidue_one assume nothing at all — and derives the composite's order itself. The total form is asymmetric: normResidueOrOne_mul and normResidueOrOne_div need both arguments admissible, while normResidueOrOne_inv needs nothing, since ord_P f⁻¹ = -ord_P f vanishes exactly when ord_P f does.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8 — the local factors of the divisor evaluation used there to construct the Weil pairing.

noncomputable def TauCeti.Place.residueUnit {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : Fˣ) (hf : P.ord ↑f = 0) : P.ResidueFieldˣ

The residue f(P) of a function that is a unit at P, as a unit of the residue field. Being a unit is what makes the residue nonzero, which is what lets it be raised to a negative power in TauCeti.Divisor.eval.

This is Mathlib's ValuationSubring.unitGroupToResidueFieldUnits at the unit-group element f names, rather than a residue paired with a separate proof that it is nonzero.

Equations

• P.residueUnit f hf = P.integers.unitGroupToResidueFieldUnits (TauCeti.Place.unitGroupMk✝ P f hf)

@[simp]

theorem TauCeti.Place.coe_residueUnit {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : Fˣ) (hf : P.ord ↑f = 0) : ↑(P.residueUnit f hf) = (IsLocalRing.residue ↥P.integers) ⟨↑f, ⋯⟩

The residue field element underlying residueUnit: the residue of f in 𝒪_P / 𝔪_P.

noncomputable def TauCeti.Place.normResidue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : Fˣ) (hf : P.ord ↑f = 0) : kˣ

The norm to k of the residue of a function that is a unit at P. The residue field varies with P; the norm is what puts the value in k, the one field all the local factors of TauCeti.Divisor.eval have to share.

This is the classical field norm precisely when Module.Finite k P.ResidueField — which TauCeti.Place.finiteDimensional_residueField supplies for every place of a function field. Absent that, Algebra.norm is the junk value 1 (Algebra.norm_eq_one_of_not_module_finite), exactly as TauCeti.Place.degree is junk 0 absent the same hypothesis.

Equations

• P.normResidue f hf = (TauCeti.Algebra.normUnits k) (P.residueUnit f hf)

@[simp]

theorem TauCeti.Place.coe_normResidue {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : Fˣ) (hf : P.ord ↑f = 0) : ↑(P.normResidue f hf) = (Algebra.norm k) ↑(P.residueUnit f hf)

The element of k underlying normResidue: the norm of the residue.

noncomputable def TauCeti.Place.normResidueOrOne {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : Fˣ) : kˣ

normResidue extended by 1 where f is not a unit, making it a total function of the place. 1 is the only workable neutral value: the coefficient of a place in a divisor is an integer, so the local factor is raised to a possibly negative power, and only a value in kˣ survives that.

Equations

• P.normResidueOrOne f = if hf : P.ord ↑f = 0 then P.normResidue f hf else 1

@[simp]

theorem TauCeti.Place.normResidueOrOne_of_ord_eq_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f : Fˣ} (hf : P.ord ↑f = 0) : P.normResidueOrOne f = P.normResidue f hf

Where f is a unit at P, the total local factor is the genuine norm of the residue.

@[simp]

theorem TauCeti.Place.normResidueOrOne_of_ord_ne_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f : Fˣ} (hf : P.ord ↑f ≠ 0) : P.normResidueOrOne f = 1

Where f is not a unit at P, the total local factor is the neutral value 1.

@[simp]

theorem TauCeti.Place.residueUnit_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f g : Fˣ} (hf : P.ord ↑f = 0) (hg : P.ord ↑g = 0) : P.residueUnit (f * g) ⋯ = P.residueUnit f hf * P.residueUnit g hg

The residue is multiplicative in the function, at a place where both factors are units: (f g)(P) = f(P) · g(P).

@[simp]

theorem TauCeti.Place.normResidue_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f g : Fˣ} (hf : P.ord ↑f = 0) (hg : P.ord ↑g = 0) : P.normResidue (f * g) ⋯ = P.normResidue f hf * P.normResidue g hg

The norm of the residue is multiplicative in the function, at a place where both factors are units.

@[simp]

theorem TauCeti.Place.residueUnit_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.residueUnit 1 ⋯ = 1

The residue of the constant 1 is 1.

@[simp]

theorem TauCeti.Place.residueUnit_inv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f : Fˣ} (hf : P.ord ↑f = 0) : P.residueUnit f⁻¹ ⋯ = (P.residueUnit f hf)⁻¹

The residue inverts with the function: f⁻¹(P) = f(P)⁻¹.

@[simp]

theorem TauCeti.Place.residueUnit_zpow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f : Fˣ} (hf : P.ord ↑f = 0) (n : ℤ) : P.residueUnit (f ^ n) ⋯ = P.residueUnit f hf ^ n

The residue takes powers with the function: (f ^ n)(P) = f(P) ^ n.

@[simp]

theorem TauCeti.Place.residueUnit_div {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f g : Fˣ} (hf : P.ord ↑f = 0) (hg : P.ord ↑g = 0) : P.residueUnit (f / g) ⋯ = P.residueUnit f hf / P.residueUnit g hg

The residue divides with the function: (f / g)(P) = f(P) / g(P), at a place where both are units.

@[simp]

theorem TauCeti.Place.normResidue_inv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f : Fˣ} (hf : P.ord ↑f = 0) : P.normResidue f⁻¹ ⋯ = (P.normResidue f hf)⁻¹

The norm of the residue inverts with the function: N(f⁻¹(P)) = N(f(P))⁻¹.

@[simp]

theorem TauCeti.Place.normResidue_div {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f g : Fˣ} (hf : P.ord ↑f = 0) (hg : P.ord ↑g = 0) : P.normResidue (f / g) ⋯ = P.normResidue f hf / P.normResidue g hg

The norm of the residue divides with the function: N((f / g)(P)) = N(f(P)) / N(g(P)).

@[simp]

theorem TauCeti.Place.normResidue_zpow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f : Fˣ} (hf : P.ord ↑f = 0) (n : ℤ) : P.normResidue (f ^ n) ⋯ = P.normResidue f hf ^ n

The norm of the residue takes powers with the function: N((f ^ n)(P)) = N(f(P)) ^ n.

@[simp]

theorem TauCeti.Place.normResidueOrOne_mul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f g : Fˣ} (hf : P.ord ↑f = 0) (hg : P.ord ↑g = 0) : P.normResidueOrOne (f * g) = P.normResidueOrOne f * P.normResidueOrOne g

The total local factor is multiplicative in the function, at a place where both factors are units. The hypotheses cannot be dropped: at a place where f and g have opposite nonzero orders, f * g is a unit while neither factor is, so the left side is a genuine norm and the right side is 1.

@[simp]

theorem TauCeti.Place.normResidue_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.normResidue 1 ⋯ = 1

The residue of the constant 1 has norm 1.

theorem TauCeti.Place.normResidueOrOne_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.normResidueOrOne 1 = 1

The constant 1 has local factor 1.

@[simp]

theorem TauCeti.Place.normResidueOrOne_inv {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (f : Fˣ) : P.normResidueOrOne f⁻¹ = (P.normResidueOrOne f)⁻¹

Inversion needs no admissibility hypothesis. ord_P f⁻¹ = -ord_P f vanishes exactly when ord_P f does, so the two places of normResidueOrOne's case split correspond under inversion and both branches invert. Contrast normResidueOrOne_mul, where the hypotheses cannot be dropped: a product can leave the subgroup {ord_P = 0} open on neither factor.

@[simp]

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

Powers need no admissibility hypothesis, for the same reason as normResidueOrOne_inv: where f is not a unit neither is any nonzero power of it, and both sides are 1.

@[simp]

theorem TauCeti.Place.normResidueOrOne_div {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {f g : Fˣ} (hf : P.ord ↑f = 0) (hg : P.ord ↑g = 0) : P.normResidueOrOne (f / g) = P.normResidueOrOne f / P.normResidueOrOne g

The total local factor divides in the function, at a place where both arguments are units. Like normResidueOrOne_mul, and unlike normResidueOrOne_inv, the hypotheses cannot be dropped: a quotient can be a unit where neither argument is.