How to factor the largest power of X from a polynomial?

Stream: Is there code for X?

[Stepan Nesterov]

I am trying to prove the following lemma from commutative algebra:

lemma ideal_in_integral_extension_overlap (R S : Type*) [CommRing R] [Nontrivial R] [CommRing S]
  [IsDomain S] [Algebra R S] [Algebra.IsIntegral R S] (I : Ideal S) (hI : I ≠ ⊥) :
    ∃ a : R, a ≠ 0 ∧ (algebraMap R S) a ∈ I := by
    obtain ⟨a, ha, a_nz⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
    obtain ⟨P, P_mon, hP⟩ := Algebra.IsIntegral.isIntegral (R := R) a
    have : P = Polynomial.X ^ (Polynomial.natTrailingDegree P) *
      (P /ₘ (Polynomial.X ^ (Polynomial.natTrailingDegree P))) := by
      sorry
    rw[this] at hP
    simp only [Polynomial.eval₂_mul, Polynomial.eval₂_X_pow, mul_eq_zero, pow_eq_zero_iff', ne_eq,
      Polynomial.natTrailingDegree_eq_zero, not_or, not_not] at hP
    obtain ⟨hP, _⟩  | hP := hP
    · contradiction
    have : (P /ₘ (Polynomial.X ^ P.natTrailingDegree)).coeff 0 = P.coeff P.natTrailingDegree := by
      sorry
    have : (P /ₘ Polynomial.X ^ P.natTrailingDegree).coeff 0 ≠ 0 := by
      rw[this, Polynomial.coeff_natTrailingDegree_ne_zero]
      exact Polynomial.Monic.ne_zero_of_ne (zero_ne_one' R) P_mon
    rw[show (P /ₘ Polynomial.X ^ P.natTrailingDegree = (P /ₘ Polynomial.X ^ P.natTrailingDegree) -
      Polynomial.C ((P /ₘ Polynomial.X ^ P.natTrailingDegree).coeff 0) +
      Polynomial.C ((P /ₘ Polynomial.X ^ P.natTrailingDegree).coeff 0)) by simp] at hP
    rw[Polynomial.eval₂_add, Polynomial.eval₂_C] at hP
    obtain ⟨Q, hQ⟩ := Polynomial.X_dvd_sub_C (p := P /ₘ Polynomial.X ^ P.natTrailingDegree)
    rw[hQ] at hP
    simp only [Polynomial.eval₂_mul, Polynomial.eval₂_X] at hP
    use (P /ₘ Polynomial.X ^ P.natTrailingDegree).coeff 0
    rw[← neg_eq_iff_add_eq_zero] at hP
    rw[← hP, Submodule.neg_mem_iff]
    exact ⟨this, Ideal.IsTwoSided.mul_mem_of_left (Polynomial.eval₂ (algebraMap R S) a Q) ha⟩

At some point, I need to factor out the largest power of X in the minimal polynomial of a, and I couldn't do that. Is there a relevant theorem in mathlib?

[Andrew Yang]

Would something like docs#Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd be helpful?

[Andrew Yang]

And as a sidenote, the correct statement of your lemma should be I.comap (algebraMap R S) ≠ ⊥, and if you write it this way exact? should solve the goal.

[metakuntyyy]

@Andrew Yang Could you please elaborate on what you mean by the correct statement? Aren't yours and his equivalent?

[Andrew Yang]

I meant “the statement that you should look for in mathlib, out of all the equivalent formulations”

[metakuntyyy]

Ah, so what's the rule of thumb for something like that? Try to use map, comap instead of using quantors?

[Kenny Lau]

yes, in general prefer the lattice language over the set language

[metakuntyyy]

Yeah, I figured that out. It seems beneficial to talk about lattices, as many different concepts use different notations for top and bottom element. Seems to be very practical to use top and bottom instead of empty set, or $\{0\}$, or Set.univ

[Ruben Van de Velde]

Though Set (and Finset) are the cases where mathlib generally doesn't use lattice notation

[metakuntyyy]

Also true.