Zulip Chat Archive

Stream: maths

Topic: explicit polynomials


Jon Eugster (May 16 2021 at 16:26):

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: d0)
{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 yy is integral over AA then so is dydy (where dd is essentially a unit in AA). 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 (May 16 2021 at 16:53):

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

Eric Rodriguez (May 16 2021 at 17:09):

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


Last updated: Dec 20 2023 at 11:08 UTC