eq_map_of_dvd.lean

import ring_theory.integrally_closed
import field_theory.splitting_field
open_locale polynomial
open polynomial

theorem roots_mem_integral_closure {R A} [comm_ring R] [comm_ring A] [is_domain A] [algebra R A]
  {f : R[X]} (hf : f.monic) {a : A} (ha : a ∈ (f.map $ algebra_map R A).roots) :
  a ∈ integral_closure R A :=
⟨f, hf, (eval₂_eq_eval_map _).trans $ (mem_roots $ (hf.map _).ne_zero).1 ha⟩

theorem coeff_mem_subring_of_splits {K} [field K] {f : K[X]}
  (hs : f.splits $ ring_hom.id _) (hm : f.monic) (T : subring K)
  (hr : ∀ a ∈ f.roots, a ∈ T) (n : ℕ) : f.coeff n ∈ T :=
begin
  rw (_ : f = (f.roots.pmap (λ a h, X - C (⟨a, h⟩ : T)) hr).prod.map T.subtype),
  { rw coeff_map, apply set_like.coe_mem },
  conv_lhs { rw [eq_prod_roots_of_splits_id hs, hm.leading_coeff, C_1, one_mul] },
  rw [polynomial.map_multiset_prod, multiset.map_pmap],
  congr, convert (f.roots.pmap_eq_map _ _ hr).symm,
  ext1, ext1, rw [polynomial.map_sub, map_X, map_C], refl,
end

theorem frange_subset_integral_closure {R K} [comm_ring R] [field K] [algebra R K]
  {f : R[X]} (hf : f.monic) {g : K[X]} (hg : g.monic) (hd : g ∣ f.map (algebra_map R K)) :
  (g.frange : set K) ⊆ (integral_closure R K).to_subring :=
begin
  haveI : is_scalar_tower R K g.splitting_field := splitting_field_aux.is_scalar_tower _ _ _ _,
  have := coeff_mem_subring_of_splits ((splits_id_iff_splits _).2 $ splitting_field.splits g)
    (hg.map _) (integral_closure R _).to_subring (λ a ha, roots_mem_integral_closure hf _),
  { intros a ha, obtain ⟨n, -, rfl⟩ := mem_frange_iff.1 ha,
    obtain ⟨p, hp, he⟩ := this n, use [p, hp],
    rw [is_scalar_tower.algebra_map_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he,
    rw eval₂_eq_eval_map, apply (injective_iff_map_eq_zero _).1 _ _ he,
    { apply ring_hom.injective } },
  rw [is_scalar_tower.algebra_map_eq R K _, ← map_map],
  refine multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero _) ha,
  { apply_instance },
  { exact map_dvd (algebra_map K g.splitting_field) hd },
  { apply splitting_field_aux.is_scalar_tower },
end

theorem eq_map_of_dvd {R} [comm_ring R] [is_domain R] [is_integrally_closed R]
  {f : R[X]} (hf : f.monic) (g : (fraction_ring R)[X]) (hg : g.monic)
  (hd : g ∣ f.map (algebra_map R _)) : ∃ g' : R[X], g'.map (algebra_map R _) = g :=
begin
  let algeq := (subalgebra.equiv_of_eq _ _ $
    is_integrally_closed.integral_closure_eq_bot R _).trans
    (algebra.bot_equiv_of_injective $ is_fraction_ring.injective R $ fraction_ring R),
  have : (algebra_map R _).comp algeq.to_alg_hom.to_ring_hom =
    (integral_closure R _).to_subring.subtype,
  { ext, conv_rhs { rw ← algeq.symm_apply_apply x }, refl },
  refine ⟨map algeq.to_alg_hom.to_ring_hom _, _⟩,
  use g.to_subring _ (frange_subset_integral_closure hf hg hd),
  rw [map_map, this], apply g.map_to_subring,
end