explicit polynomials

Stream: maths

[Jon Eugster]

import linear_algebra.finite_dimensional
import ring_theory.integral_closure
import ring_theory.localization -- for fraction_ring

-- Note: This says basically that we can have `(↑d⁻¹:A)`.
class equal_char_zero (R : Type*) [add_monoid R] [has_one R] extends char_zero R :=
  (has_lift: has_lift ℚ R)
  (cast_injective': function.injective (coe : ℚ → R))

def div_endo_linear_map (K: Type*) [field K] (d:ℚ): K →ₗ[K] K :=
  {
    to_fun := λx, (d⁻¹)*x,
    map_add' :=
    begin
      intros x y,
      exact mul_add (↑d)⁻¹ x y,
    end,
    map_smul' :=
    begin
      intros m x,
      exact mul_smul_comm m (↑d)⁻¹ x,
    end,
  }

lemma div_endo_linear_map.is_integral {A: Type*} [integral_domain A] (d:ℚ) (hd: d≠0)
{y:(fraction_ring A)} (h:is_integral A y) [equal_char_zero A]:
is_integral A ((div_endo_linear_map (fraction_ring A) d) y) :=
begin
  cases h with p hp,
  /-
  Steps:
  1) If `p = a_n X^n + ... + a_0`, then create the polynomial
     `q = (a_n/d^n) X^n + ... + (a_0/d^0)`
  2) since `p(y) = 0`, we should get that `q(d*y) = 0`
  3) `q' = d^n*q` is monic with `q'(d*y) = 0`.
  -/
  sorry
end

I looked through the file defining polynomials but I don't fully understand them. Could somebody give me a hint how to construct explicit polynomials (i.e. by modifying each coefficient of another polynomial).

Above I try to prove that if $y$ is integral over $A$ then so is $dy$ (where $d$ is essentially a unit in $A$). The way of doing that is to explicitly construct an annihilating polynomial. I think I could work out step 2) and 3) once I got step 1).

Thanks for the help!

[Thomas Browning]

In this case, could you use polynomial.comp, where you compose p with (1/d) * X?

[Eric Rodriguez]

that'd also need a lemma explaining how the leading coeff changes with .comp, which I don't think exists