IsIntegral.exists_multiple_integral_of_isAlgebraic

Stream: Is there code for X?

[Kevin Buzzard]

Do we have this? If an integral domain A is a subring of a ring L, and if x in L is algebraic over A, then there's some nonzero a such that $ax$ is integral over A. The maths proof: if $\sum_{i=0}^dp_ix^i=0$ is a nonzero poly of degree $d$ then use a=p_d and multiply the previous equation by a^{d-1} to see what is obviously a monic polynomial in ax. I found it quite painful:

import Mathlib.RingTheory.Localization.NormTrace

open Algebra Polynomial

open scoped BigOperators nonZeroDivisors

variable (A : Type*) [CommRing A] (L : Type*) [Ring L] [Algebra A L]

theorem IsIntegral.exists_multiple_integral_of_isAlgebraic
    (hinj : Function.Injective (algebraMap A L))
    {x : L} (hx : IsAlgebraic A x) : ∃ m : A, m ≠ 0 ∧ IsIntegral A (m • x) := by
  obtain ⟨p, hp0, hpx⟩ := hx
  have := leadingCoeff_ne_zero.mpr hp0
  refine ⟨p.leadingCoeff, this, ?_⟩
  have this : 0 < p.natDegree := by
    exact natDegree_pos_of_aeval_root hp0 hpx (fun x hx ↦ hinj <| hx ▸ by simp)
  obtain ⟨n, hn⟩ : ∃ n, p.natDegree = n + 1 := Nat.exists_eq_add_of_le' this
  rw [aeval_eq_sum_range] at hpx
  apply_fun ((p.leadingCoeff)^n • .) at hpx
  rw [smul_zero, Finset.smul_sum] at hpx
  use monomial p.natDegree 1 +  ∑ i ∈ Finset.range p.natDegree, Polynomial.monomial i ((p.leadingCoeff)^ (n - i) * (p.coeff i))
  refine ⟨?_, ?_⟩
  · apply monic_of_natDegree_le_of_coeff_eq_one p.natDegree
    · rw [natDegree_add_le_iff_right _ _ (natDegree_monomial_le 1)]
      refine natDegree_sum_le_of_forall_le _ _ (fun i hi ↦ ?_)
      exact le_trans (natDegree_monomial_le _) (Finset.mem_range.1 hi).le
    · simp [coeff_monomial]
  · rw [Finset.sum_range_succ, add_comm] at hpx
    simp only [Submonoid.mk_smul, eval₂_add, eval₂_monomial, map_one, one_mul, eval₂_finset_sum,
      map_mul, map_pow, ← hpx, hn]
    congr 1
    · simp only [leadingCoeff, hn, smul_pow, smul_smul]
      ring_nf
    · apply Finset.sum_congr rfl
      intro i hi
      rw [Finset.mem_range_succ_iff] at hi
      rw [smul_pow, ← map_pow, ← map_mul, smul_def, ← mul_assoc, ← map_mul, ← smul_assoc,
          smul_eq_mul, smul_def, mul_assoc, mul_comm (p.coeff i), ← mul_assoc,
          pow_sub_mul_pow p.leadingCoeff hi]

The reason I want this is because I think the AKLB people have missed a trick. They are trying to move from stuff involving K,L (e.g. Aut(L/K)) directly to stuff involving A,B (e.g. Aut(B/A); see docs#galRestrict . I think all of this stuff factors through the (A,L) picture (e.g. Aut(L/A) ) and I think this will clear the proofs up a lot. I needed the above lemma because I wanted to replace the assumption "K is the field of fractions of A and L is finite-dimensional over K" by an assumption which didn't involve K at all, and Algebraic A L works great, but now I need to prove that if L is algebraic then some multiple is integral, and the proof I'm mimicking unnecessarily goes through K when it could go via the above.

[Junyan Xu]

You almost guessed the name: docs#exists_integral_multiple
I Moogled and it appears as the 8th result

[Johan Commelin]

In the root namespace :see_no_evil: :grinning: