feat(data/polynomial/denominators): add file denominators (#5587)

The main goal of this PR is to establish that `b^deg(f)*f(a/b)` is an expression not involving denominators.

The first lemma, `induction_with_nat_degree_le` is an induction principle for polynomials, where the inductive hypothesis has a bound on the degree of the polynomial.  This allows to build the proof by tearing apart a polynomial into its monomials, while remembering the overall degree of the polynomial itself.  This lemma might be a better fit for the file `data.polynomial.induction`.

Author: adomani

src/data/polynomial/denoms_clearable.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2020 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import data.polynomial.erase_lead
+/-!
+# Denominators of evaluation of polynomials at ratios
+
+Let `i : R → K` be a homomorphism of semirings.  Assume that `K` is commutative.  If `a` and
+`b` are elements of `R` such that `i b ∈ K` is invertible, then for any polynomial
+`f ∈ polynomial R` the "mathematical" expression `b ^ f.nat_degree * f (a / b) ∈ K` is in
+the image of the homomorphism `i`.
+-/
+
+open polynomial finset
+
+section denoms_clearable
+
+variables {R K : Type*} [semiring R] [comm_semiring K] {i : R →+* K}
+variables {a b : R} {bi : K}
+-- TODO: use hypothesis (ub : is_unit (i b)) to work with localizations.
+
+/-- `denoms_clearable` formalizes the property that `b ^ N * f (a / b)`
+does not have denominators, if the inequality `f.nat_degree ≤ N` holds.
+
+In the implementation, we also use provide an inverse in the existential.
+-/
+def denoms_clearable (a b : R) (N : ℕ) (f : polynomial R) (i : R →+* K) : Prop :=
+  ∃ (D : R) (bi : K), bi * i b = 1 ∧ i D = i b ^ N * eval (i a * bi) (f.map i)
+
+lemma denoms_clearable_zero (N : ℕ) (a : R) (bu : bi * i b = 1) :
+  denoms_clearable a b N 0 i :=
+⟨0, bi, bu, by simp only [eval_zero, ring_hom.map_zero, mul_zero, map_zero]⟩
+
+lemma denoms_clearable_C_mul_X_pow {N : ℕ} (a : R) (bu : bi * i b = 1) {n : ℕ} (r : R)
+  (nN : n ≤ N) : denoms_clearable a b N (C r * X ^ n) i :=
+begin
+  refine ⟨r * a ^ n * b ^ (N - n), bi, bu, _⟩,
+  rw [C_mul_X_pow_eq_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, eval_mul, eval_pow, eval_C],
+  rw [ring_hom.map_mul, ring_hom.map_mul, ring_hom.map_pow, ring_hom.map_pow, eval_X, mul_comm],
+  rw [← nat.sub_add_cancel nN] {occs := occurrences.pos [2]},
+  rw [pow_add, mul_assoc, mul_comm (i b ^ n), mul_pow, mul_assoc, mul_assoc (i a ^ n), ← mul_pow],
+  rw [bu, one_pow, mul_one],
+end
+
+lemma denoms_clearable.add {N : ℕ} {f g : polynomial R} :
+  denoms_clearable a b N f i → denoms_clearable a b N g i → denoms_clearable a b N (f + g) i :=
+λ ⟨Df, bf, bfu, Hf⟩ ⟨Dg, bg, bgu, Hg⟩, ⟨Df + Dg, bf, bfu,
+  begin
+    rw [ring_hom.map_add, polynomial.map_add, eval_add, mul_add, Hf, Hg],
+    congr,
+    refine @inv_unique K _ (i b) bg bf _ _;
+    rwa mul_comm,
+  end ⟩
+
+lemma denoms_clearable_of_nat_degree_le (N : ℕ) (a : R) (bu : bi * i b = 1) :
+  ∀ (f : polynomial R), f.nat_degree ≤ N → denoms_clearable a b N f i :=
+induction_with_nat_degree_le N
+  (denoms_clearable_zero N a bu)
+  (λ N_1 r r0, denoms_clearable_C_mul_X_pow a bu r)
+  (λ f g fN gN df dg, df.add dg)
+
+/-- If `i : R → K` is a ring homomorphism, `f` is a polynomial with coefficients in `R`,
+`a, b` are elements of `R`, with `i b` invertible, then there is a `D ∈ R` such that
+`b ^ f.nat_degree * f (a / b)` equals `i D`. -/
+theorem denoms_clearable_nat_degree
+  (i : R →+* K) (f : polynomial R) (a : R) (bu : bi * i b = 1) :
+  denoms_clearable a b f.nat_degree f i :=
+denoms_clearable_of_nat_degree_le f.nat_degree a bu f le_rfl
+
+end denoms_clearable

src/data/polynomial/erase_lead.lean

@@ -159,4 +159,30 @@ end
 
 end erase_lead
 
+/-- An induction lemma for polynomials. It takes a natural number `N` as a parameter, that is
+required to be at least as big as the `nat_degree` of the polynomial.  This is useful to prove
+results where you want to change each term in a polynomial to something else depending on the
+`nat_degree` of the polynomial itself and not on the specific `nat_degree` of each term. -/
+lemma induction_with_nat_degree_le {R : Type*} [semiring R] {P : polynomial R → Prop} (N : ℕ)
+  (P_0 : P 0)
+  (P_C_mul_pow : ∀ n : ℕ, ∀ r : R, r ≠ 0 → n ≤ N → P (C r * X ^ n))
+  (P_C_add : ∀ f g : polynomial R, f.nat_degree ≤ N → g.nat_degree ≤ N → P f → P g → P (f + g)) :
+  ∀ f : polynomial R, f.nat_degree ≤ N → P f :=
+begin
+  intros f df,
+  generalize' hd : card f.support = c,
+  revert f,
+  induction c with c hc,
+  { exact λ f df f0, by rwa (finsupp.support_eq_empty.mp (card_eq_zero.mp f0)) },
+  { intros f df f0,
+    rw ← erase_lead_add_C_mul_X_pow f,
+    refine P_C_add f.erase_lead _ (erase_lead_nat_degree_le.trans df) _ _ _,
+    { exact (nat_degree_C_mul_X_pow_le f.leading_coeff f.nat_degree).trans df },
+    { exact hc _ (erase_lead_nat_degree_le.trans df) (erase_lead_card_support f0) },
+    { refine P_C_mul_pow _ _ _ df,
+      rw [ne.def, leading_coeff_eq_zero],
+      rintro rfl,
+      exact not_le.mpr c.succ_pos f0.ge } }
+end
+
 end polynomial