An integral element over a localization B of a comm_ring A is a multiple of an integral element over A by a unit in B.

integral_localization.lean

import ring_theory.integral_closure
import ring_theory.localization.integer

open_locale polynomial
open polynomial
lemma eq_map_of_frange_subset_srange {A B} [semiring A] [semiring B] (f : A →+* B)
  (p : B[X]) (hp : ↑p.frange ⊆ (f.srange : set B)) :
  ∃ q : A[X], p = q.map f ∧ q.nat_degree = p.nat_degree ∧ (p.monic → q.monic) :=
begin
  classical,
  casesI subsingleton_or_nontrivial B with hB hB,
  { refine ⟨1, _, _, λ _, monic_one⟩, 
    { ext, apply subsingleton.elim },
    { rw [nat_degree_one, nat_degree_of_subsingleton] } },
  let g : B → A := λ x, if x = 0 then 0 else if x = 1 then 1 else
    if hx : x ∈ f.srange then classical.some hx else 0,
  have inv : ∀ b ∈ f.srange, f (g b) = b,
  { intros b hb, dsimp only [g], split_ifs,
    { rw h, apply map_zero }, { rw h_1, apply map_one }, { exact hb.some_spec } },
  have g0 : g 0 = 0 := if_pos rfl,
  have g1 : g 1 = 1 := (if_neg one_ne_zero).trans (if_pos rfl),
  let q : A[X] := ⟨p.to_finsupp.map_range g g0⟩,
  have qcoeff : ∀ n, q.coeff n = g (p.coeff n),
  { intro n, dsimp only [q], rw [coeff, finsupp.map_range_apply], cases p, refl },
  have eqmap : p = q.map f,
  { ext, rw [coeff_map, qcoeff],
    by_cases n ∈ p.support,
    { rw inv, exacts hp (mem_frange_iff.2 ⟨n, h, rfl⟩) },
    { rw [not_mem_support_iff.1 h, g0, map_zero] } },
  have degeq : q.nat_degree = p.nat_degree,
  { apply le_antisymm,
    { apply nat_degree_le_nat_degree,
      apply degree_mono,
      intro n, simp only [mem_support_iff],
      apply mt, intro h, rw [qcoeff, h, g0] },
    { rw eqmap, apply nat_degree_map_le } },
  dsimp only [monic, leading_coeff],
  exact ⟨q, eqmap, degeq, λ h, by rw [qcoeff, degeq, h, g1]⟩,
end

variables {A B C : Type*} [comm_ring A] [comm_ring B] [comm_ring C]
  [algebra A B] [algebra A C] [algebra B C] [is_scalar_tower A B C]

lemma frange_scale_roots_subset_srange (M : submonoid A) [is_localization M B]
  (p : B[X]) (hp : p.leading_coeff ∈ (algebra_map A B).srange) :
  ∃ d : B, is_unit d ∧ ↑(scale_roots p d).frange ⊆ ((algebra_map A B).srange : set B) :=
begin
  let d := algebra_map A B (is_localization.common_denom M p.frange id), 
  refine ⟨d, is_localization.map_units B _, λ c hc, _⟩,
  obtain ⟨n, hn, rfl⟩ := mem_frange_iff.1 hc,
  have hl := le_nat_degree_of_mem_supp n hn,
  rw coeff_scale_roots, rw nat_degree_scale_roots at hl,
  obtain hl | rfl := hl.lt_or_eq,
  { rw [← nat.succ_pred_eq_of_pos (nat.sub_pos_of_lt hl), pow_succ, ← mul_assoc, set_like.mem_coe],
    refine subsemiring.mul_mem _ _ (subsemiring.pow_mem _ ⟨_, rfl⟩ _),
    by_cases h0 : p.coeff n = 0, { rw [h0, zero_mul], apply subsemiring.zero_mem },
    split, rw mul_comm, convert algebra.smul_def _ _,
    convert is_localization.map_integer_multiple M p.frange id _,
    swap, exacts [⟨_, coeff_mem_frange p n h0⟩, rfl] },
  { rw [nat.sub_self, pow_zero, mul_one], exact hp },
end

lemma eq_smul_is_integral_of_is_localization (M : submonoid A) [is_localization M B] {x : C}
  (h : is_integral B x) : ∃ y : C, is_integral A y ∧ ∃ d : B, is_unit d ∧ x = d • y :=
begin
  obtain ⟨p, hp, h0⟩ := h,
  obtain ⟨d, hd, hs⟩ := frange_scale_roots_subset_srange M p _,
  swap, { rw hp.leading_coeff, apply subsemiring.one_mem },
  obtain ⟨q, he, -, hm⟩ := eq_map_of_frange_subset_srange (algebra_map A B) (scale_roots p d) hs,
  refine ⟨d • x, ⟨q, hm $ (monic_scale_roots_iff _).2 hp, _⟩, _⟩,
  { rw [algebra.smul_def, is_scalar_tower.algebra_map_eq A B, ← eval₂_map, ← he],
    exact scale_roots_eval₂_eq_zero _ h0  /- not applicable to [ring C] -/ },
  { use [(hd.unit⁻¹ : _), units.is_unit _], rw [smul_smul, is_unit.coe_inv_mul, one_smul] },
end