Documentation

TauCeti.FieldTheory.FunctionField.Place.RatFunc.Order

Orders at the finite places of the rational function field #

This file computes the order of a rational function at the finite place associated to an irreducible polynomial. For q : k[X] irreducible and nonzero f : k(X), the answer is the exponent of q in the numerator of f minus its exponent in the denominator. This complements TauCeti.Place.ord_infty and is the concrete finite-place calculation used by divisors on the rational function field.

Main results #

References #

source
theorem TauCeti.Place.ord_adicOfIrreducible_algebraMap {k : Type u_1} [Field k] {q r : Polynomial k} (hq : Irreducible q) (hr : r ≠ 0) :
(adicOfIrreducible hq).ord ((algebraMap (Polynomial k) (RatFunc k)) r) = ↑(multiplicity q r)

The order at the finite place associated to q of a nonzero polynomial r is the multiplicity of q in r.

source
theorem TauCeti.Place.ord_adicOfIrreducible_algebraMap_irreducible {k : Type u_1} [Field k] {q p : Polynomial k} (hq : Irreducible q) (hp : Irreducible p) :
(adicOfIrreducible hq).ord ((algebraMap (Polynomial k) (RatFunc k)) p) = if Associated q p then 1 else 0

An irreducible polynomial has order one at the finite place defined by an associated polynomial, and order zero at every other finite place.

source
theorem TauCeti.Place.ord_adicOfIrreducible_algebraMap_of_squarefree {k : Type u_1} [Field k] {q r : Polynomial k} (hq : Irreducible q) (hr : Squarefree r) :
(adicOfIrreducible hq).ord ((algebraMap (Polynomial k) (RatFunc k)) r) = if q ∣ r then 1 else 0

A squarefree polynomial has order one at the finite place of each of its irreducible factors, and order zero at every other finite place.

source
theorem TauCeti.Place.ord_adicOfIrreducible_X {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) :
(adicOfIrreducible hq).ord RatFunc.X = if Associated q Polynomial.X then 1 else 0

Among the finite places, X has order one at the place defined by a polynomial associated to X and order zero at every other place.

source
@[simp]
theorem TauCeti.Place.ord_adicOfIrreducible_X_self {k : Type u_1} [Field k] :
(adicOfIrreducible ⋯).ord RatFunc.X = 1

X has order one at its own finite place.

source
@[simp]
theorem TauCeti.Place.ord_adicOfIrreducible_X_of_not_associated {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) (h : ¬Associated q Polynomial.X) :
(adicOfIrreducible hq).ord RatFunc.X = 0

X has order zero at every finite place other than its own.

source
theorem TauCeti.Place.ord_adicOfIrreducible {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) {f : RatFunc k} (hf : f ≠ 0) :
(adicOfIrreducible hq).ord f = ↑(multiplicity q f.num) - ↑(multiplicity q f.denom)

The order of a nonzero rational function at the finite place associated to q is the multiplicity of q in its numerator minus its multiplicity in its denominator.

source
@[simp]
theorem TauCeti.Place.ord_adicOfIrreducible_pos_iff {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) {f : RatFunc k} (hf : f ≠ 0) :
0 < (adicOfIrreducible hq).ord f ↔ q ∣ f.num

A nonzero rational function has a zero at P_q exactly when q divides its reduced numerator.

source
@[simp]
theorem TauCeti.Place.ord_adicOfIrreducible_neg_iff {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) {f : RatFunc k} :
(adicOfIrreducible hq).ord f < 0 ↔ q ∣ f.denom

A rational function has a pole at P_q exactly when q divides its reduced denominator. This statement includes the zero rational function, whose reduced denominator is 1.

source
@[simp]
theorem TauCeti.Place.ord_adicOfIrreducible_eq_zero_iff {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) {f : RatFunc k} (hf : f ≠ 0) :
(adicOfIrreducible hq).ord f = 0 ↔ ¬q ∣ f.num ∧ ¬q ∣ f.denom

A nonzero rational function is a unit at P_q exactly when q divides neither its reduced numerator nor its reduced denominator.

The valuation ring and residue field #

source
@[simp]
theorem TauCeti.Place.valuation_ofIrreducible_le_one_iff {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) (f : RatFunc k) :
(IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc k) (IsDedekindDomain.HeightOneSpectrum.ofIrreducible hq)) f ≤ 1 ↔ ¬q ∣ f.denom

A rational function is regular at the finite place P_q exactly when q does not divide its reduced denominator. This statement includes the zero rational function.

source
theorem TauCeti.Place.forall_ord_adicOfIrreducible_nonneg_iff {k : Type u_1} [Field k] {f : RatFunc k} :
(∀ (q : Polynomial k) (hq : Irreducible q), 0 ≤ (adicOfIrreducible hq).ord f) ↔ ∃ (p : Polynomial k), (algebraMap (Polynomial k) (RatFunc k)) p = f

A rational function is a polynomial exactly when it has no pole at any finite place. The finite places of k(x) are the places of the height-one primes of k[X], so this is the Dedekind-domain fact that k[X] is the intersection of its localizations at them (IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one), read in place vocabulary.

source
theorem TauCeti.Place.residue_adicOfIrreducible_eq_zero_iff {k : Type u_1} [Field k] {q : Polynomial k} (hq : Irreducible q) (f : ↥(adicOfIrreducible hq).integers) :
(IsLocalRing.residue ↥(adicOfIrreducible hq).integers) f = 0 ↔ q ∣ (↑f).num

A function regular at P_q has zero residue exactly when q divides its reduced numerator.