feat(number_theory/function_field): add place at infinity (#12245)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/polynomial/ring_division.lean

@@ -116,6 +116,16 @@ begin
   rw [nat_degree_mul h2.1 h2.2], exact nat.le_add_right _ _
 end
 
+/-- This lemma is useful for working with the `int_degree` of a rational function. -/
+lemma nat_degree_sub_eq_of_prod_eq {p₁ p₂ q₁ q₂ : polynomial R} (hp₁ : p₁ ≠ 0) (hq₁ : q₁ ≠ 0)
+  (hp₂ : p₂ ≠ 0) (hq₂ : q₂ ≠ 0) (h_eq : p₁ * q₂ = p₂ * q₁) :
+  (p₁.nat_degree : ℤ) - q₁.nat_degree = (p₂.nat_degree : ℤ) - q₂.nat_degree :=
+begin
+  rw sub_eq_sub_iff_add_eq_add,
+  norm_cast,
+  rw [← nat_degree_mul hp₁ hq₂, ← nat_degree_mul hp₂ hq₁, h_eq]
+end
+
 end no_zero_divisors
 
 section no_zero_divisors

src/field_theory/ratfunc.lean

@@ -62,6 +62,11 @@ We also have a set of recursion and induction principles:
  - `ratfunc.induction_on`: if `P` holds on `p / q` for all polynomials `p q`, then `P` holds on all
    rational functions
 
+We define the degree of a rational function, with values in `ℤ`:
+ - `int_degree` is the degree of a rational function, defined as the difference between the
+   `nat_degree` of its numerator and the `nat_degree` of its denominator. In particular,
+   `int_degree 0 = 0`.
+
 ## Implementation notes
 
 To provide good API encapsulation and speed up unification problems,
@@ -1034,6 +1039,10 @@ begin
   { exact algebra_map_ne_zero (denom_ne_zero y) }
 end
 
+lemma num_denom_neg (x : ratfunc K) :
+  (-x).num * x.denom = - x.num * (-x).denom :=
+by rw [num_mul_eq_mul_denom_iff (denom_ne_zero x), _root_.map_neg, neg_div, num_div_denom]
+
 lemma num_denom_mul (x y : ratfunc K) :
   (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom :=
 (num_mul_eq_mul_denom_iff (mul_ne_zero (denom_ne_zero x) (denom_ne_zero y))).mpr $
@@ -1123,6 +1132,15 @@ lemma lift_alg_hom_apply {L S : Type*} [field L] [comm_semiring S] [algebra S K[
   lift_alg_hom φ hφ f = φ f.num / φ f.denom :=
 lift_monoid_with_zero_hom_apply _ _ _
 
+lemma num_mul_denom_add_denom_mul_num_ne_zero {x y : ratfunc K} (hxy : x + y ≠ 0) :
+  x.num * y.denom + x.denom * y.num ≠ 0 :=
+begin
+  intro h_zero,
+  have h := num_denom_add x y,
+  rw [h_zero, zero_mul] at h,
+  exact (mul_ne_zero (num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)) h
+end
+
 end num_denom
 
 section eval
@@ -1165,6 +1183,9 @@ num_algebra_map _
 @[simp] lemma denom_X : denom (X : ratfunc K) = 1 :=
 denom_algebra_map _
 
+lemma X_ne_zero : (ratfunc.X : ratfunc K) ≠ 0 :=
+ratfunc.algebra_map_ne_zero polynomial.X_ne_zero
+
 variables {L : Type*} [field L]
 
 /-- Evaluate a rational function `p` given a ring hom `f` from the scalar field
@@ -1243,6 +1264,89 @@ end
 
 end eval
 
+section int_degree
+
+open polynomial
+
+omit hring
+
+variables [field K]
+
+/-- `int_degree x` is the degree of the rational function `x`, defined as the difference between
+the `nat_degree` of its numerator and the `nat_degree` of its denominator. In particular,
+`int_degree 0 = 0`. -/
+def int_degree (x : ratfunc K) : ℤ := nat_degree x.num - nat_degree x.denom
+
+@[simp] lemma int_degree_zero : int_degree (0 : ratfunc K) = 0 :=
+by rw [int_degree, num_zero, nat_degree_zero, denom_zero, nat_degree_one, sub_self]
+
+@[simp] lemma int_degree_one : int_degree (1 : ratfunc K) = 0 :=
+by rw [int_degree, num_one, denom_one, sub_self]
+
+@[simp] lemma int_degree_C (k : K): int_degree (ratfunc.C k) = 0 :=
+by rw [int_degree, num_C, nat_degree_C, denom_C, nat_degree_one, sub_self]
+
+@[simp] lemma int_degree_X : int_degree (X : ratfunc K) = 1 :=
+by rw [int_degree, ratfunc.num_X, polynomial.nat_degree_X, ratfunc.denom_X,
+  polynomial.nat_degree_one, int.coe_nat_one, int.coe_nat_zero, sub_zero]
+
+@[simp] lemma int_degree_polynomial {p : polynomial K} :
+  int_degree (algebra_map (polynomial K) (ratfunc K) p) = nat_degree p :=
+by rw [int_degree, ratfunc.num_algebra_map, ratfunc.denom_algebra_map, polynomial.nat_degree_one,
+  int.coe_nat_zero, sub_zero]
+
+lemma int_degree_mul {x y : ratfunc K} (hx : x ≠ 0) (hy : y ≠ 0) :
+  int_degree (x * y) = int_degree x + int_degree y :=
+begin
+  simp only [int_degree, add_sub, sub_add, sub_sub_assoc_swap, sub_sub, sub_eq_sub_iff_add_eq_add],
+  norm_cast,
+  rw [← polynomial.nat_degree_mul x.denom_ne_zero y.denom_ne_zero,
+        ← polynomial.nat_degree_mul (ratfunc.num_ne_zero (mul_ne_zero hx hy))
+          (mul_ne_zero x.denom_ne_zero y.denom_ne_zero),
+        ← polynomial.nat_degree_mul (ratfunc.num_ne_zero hx) (ratfunc.num_ne_zero hy),
+        ← polynomial.nat_degree_mul (mul_ne_zero (ratfunc.num_ne_zero hx) (ratfunc.num_ne_zero hy))
+          (x * y).denom_ne_zero, ratfunc.num_denom_mul]
+end
+
+@[simp] lemma int_degree_neg (x : ratfunc K) : int_degree (-x) = int_degree x :=
+begin
+  by_cases hx : x = 0,
+  { rw [hx, neg_zero] },
+  { rw [int_degree, int_degree, ← nat_degree_neg x.num],
+    exact nat_degree_sub_eq_of_prod_eq (num_ne_zero (neg_ne_zero.mpr hx)) (denom_ne_zero (- x))
+      (neg_ne_zero.mpr (num_ne_zero hx)) (denom_ne_zero x) (num_denom_neg x) }
+end
+
+lemma int_degree_add {x y : ratfunc K}
+  (hxy : x + y ≠ 0) : (x + y).int_degree  =
+    (x.num * y.denom + x.denom * y.num).nat_degree - (x.denom * y.denom).nat_degree :=
+nat_degree_sub_eq_of_prod_eq (num_ne_zero hxy) ((x + y).denom_ne_zero)
+    (num_mul_denom_add_denom_mul_num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)
+    (num_denom_add x y)
+
+lemma nat_degree_num_mul_right_sub_nat_degree_denom_mul_left_eq_int_degree {x : ratfunc K}
+  (hx : x ≠ 0) {s : polynomial K} (hs : s ≠ 0) :
+  ((x.num * s).nat_degree : ℤ) - (s * x.denom).nat_degree = x.int_degree :=
+begin
+  apply nat_degree_sub_eq_of_prod_eq (mul_ne_zero (num_ne_zero hx) hs)
+    (mul_ne_zero hs x.denom_ne_zero) (num_ne_zero hx) x.denom_ne_zero,
+  rw mul_assoc
+end
+
+lemma int_degree_add_le {x y : ratfunc K} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x + y ≠ 0) :
+  int_degree (x + y) ≤ max (int_degree x) (int_degree y) :=
+begin
+  rw [int_degree_add hxy,
+    ← nat_degree_num_mul_right_sub_nat_degree_denom_mul_left_eq_int_degree hx y.denom_ne_zero,
+    mul_comm y.denom,
+    ← nat_degree_num_mul_right_sub_nat_degree_denom_mul_left_eq_int_degree hy x.denom_ne_zero,
+    le_max_iff,sub_le_sub_iff_right, int.coe_nat_le, sub_le_sub_iff_right, int.coe_nat_le,
+    ← le_max_iff, mul_comm y.num],
+    exact nat_degree_add_le _ _,
+end
+
+end int_degree
+
 section laurent_series
 
 open power_series laurent_series hahn_series

src/number_theory/function_field.lean

@@ -18,6 +18,8 @@ This file defines a function field and the ring of integers corresponding to it.
    i.e. it is a finite extension of the field of rational functions in one variable over `Fq`.
  - `function_field.ring_of_integers` defines the ring of integers corresponding to a function field
     as the integral closure of `polynomial Fq` in the function field.
+ - `infty_valuation` : The place at infinity on `Fq(t)` is the nonarchimedean valuation on `Fq(t)`
+    with uniformizer `1/t`.
 
 ## Implementation notes
 The definitions that involve a field of fractions choose a canonical field of fractions,
@@ -107,4 +109,94 @@ is_integral_closure.is_dedekind_domain Fq[X] (ratfunc Fq) F _
 
 end ring_of_integers
 
+/-! ### The place at infinity on Fq(t) -/
+
+section infty_valuation
+
+variable [decidable_eq (ratfunc Fq)]
+
+/-- The valuation at infinity is the nonarchimedean valuation on `Fq(t)` with uniformizer `1/t`.
+Explicitly, if `f/g ∈ Fq(t)` is a nonzero quotient of polynomials, its valuation at infinity is
+`multiplicative.of_add(degree(f) - degree(g))`. -/
+def infty_valuation_def (r : ratfunc Fq) : with_zero (multiplicative ℤ) :=
+if r = 0 then 0 else (multiplicative.of_add r.int_degree)
+
+lemma infty_valuation.map_zero' : infty_valuation_def Fq 0 = 0 := if_pos rfl
+
+lemma infty_valuation.map_one' : infty_valuation_def Fq 1 = 1 :=
+(if_neg one_ne_zero).trans $
+  by rw [ratfunc.int_degree_one, of_add_zero, with_zero.coe_one]
+
+lemma infty_valuation.map_mul' (x y : ratfunc Fq) :
+  infty_valuation_def Fq (x * y) = infty_valuation_def Fq x * infty_valuation_def Fq y :=
+begin
+  rw [infty_valuation_def, infty_valuation_def, infty_valuation_def],
+  by_cases hx : x = 0,
+  { rw [hx, zero_mul, if_pos (eq.refl _), zero_mul] },
+  { by_cases hy : y = 0,
+    { rw [hy, mul_zero, if_pos (eq.refl _), mul_zero] },
+    { rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← with_zero.coe_mul,
+        with_zero.coe_inj, ← of_add_add, ratfunc.int_degree_mul hx hy], }}
+end
+
+lemma infty_valuation.map_add_le_max' (x y : ratfunc Fq) :
+  infty_valuation_def Fq (x + y) ≤ max (infty_valuation_def Fq x) (infty_valuation_def Fq y) :=
+begin
+  by_cases hx : x = 0,
+  { rw [hx, zero_add],
+    conv_rhs { rw [infty_valuation_def, if_pos (eq.refl _)] },
+    rw max_eq_right (with_zero.zero_le (infty_valuation_def Fq y)),
+    exact le_refl _ },
+  { by_cases hy : y = 0,
+    { rw [hy, add_zero],
+      conv_rhs { rw [max_comm, infty_valuation_def, if_pos (eq.refl _)] },
+      rw max_eq_right (with_zero.zero_le (infty_valuation_def Fq x)),
+      exact le_refl _ },
+    { by_cases hxy : x + y = 0,
+      { rw [infty_valuation_def, if_pos hxy], exact zero_le',},
+      { rw [infty_valuation_def, infty_valuation_def, infty_valuation_def, if_neg hx, if_neg hy,
+        if_neg hxy],
+        rw [le_max_iff,
+        with_zero.coe_le_coe, multiplicative.of_add_le, with_zero.coe_le_coe,
+        multiplicative.of_add_le, ← le_max_iff],
+        exact ratfunc.int_degree_add_le hx hy hxy }}}
+end
+
+@[simp] lemma infty_valuation_of_nonzero {x : ratfunc Fq} (hx : x ≠ 0) :
+  infty_valuation_def Fq x = (multiplicative.of_add x.int_degree) :=
+by rw [infty_valuation_def, if_neg hx]
+
+/-- The valuation at infinity on `Fq(t)`. -/
+def infty_valuation  : valuation (ratfunc Fq) (with_zero (multiplicative ℤ)) :=
+{ to_fun          := infty_valuation_def Fq,
+  map_zero'       := infty_valuation.map_zero' Fq,
+  map_one'        := infty_valuation.map_one' Fq,
+  map_mul'        := infty_valuation.map_mul' Fq,
+  map_add_le_max' := infty_valuation.map_add_le_max' Fq }
+
+@[simp] lemma infty_valuation_apply {x : ratfunc Fq} :
+  infty_valuation Fq x = infty_valuation_def Fq x := rfl
+
+@[simp] lemma infty_valuation.C {k : Fq} (hk : k ≠ 0) :
+  infty_valuation_def Fq (ratfunc.C k) = (multiplicative.of_add (0 : ℤ)) :=
+begin
+  have hCk : ratfunc.C k ≠ 0 := (ring_hom.map_ne_zero _).mpr hk,
+  rw [infty_valuation_def, if_neg hCk, ratfunc.int_degree_C],
+end
+
+@[simp] lemma infty_valuation.X :
+  infty_valuation_def Fq (ratfunc.X) = (multiplicative.of_add (1 : ℤ)) :=
+by rw [infty_valuation_def, if_neg ratfunc.X_ne_zero, ratfunc.int_degree_X]
+
+@[simp] lemma infty_valuation.polynomial {p : polynomial Fq} (hp : p ≠ 0) :
+  infty_valuation_def Fq (algebra_map (polynomial Fq) (ratfunc Fq) p) =
+    (multiplicative.of_add (p.nat_degree : ℤ)) :=
+begin
+  have hp' : algebra_map (polynomial Fq) (ratfunc Fq) p ≠ 0,
+  { rw [ne.def, ratfunc.algebra_map_eq_zero_iff], exact hp },
+  rw [infty_valuation_def, if_neg hp', ratfunc.int_degree_polynomial]
+end
+
+end infty_valuation
+
 end function_field