viewing polynomials over a field as pid has issues

Stream: mathlib4

[Barry Trager]

import Mathlib

lemma test {R : Type*} [Field R] (I :   Ideal (Polynomial R)) :
    ∃ p, I = Ideal.span {p} := by
  have pid := Polynomial.instEuclideanDomain (R := R)
  apply EuclideanDomain.to_principal_ideal_domain at pid
  rw [isPrincipalIdealRing_iff] at pid
  -- cannot specialize pid at I
  specialize (pid I)

The specialize command fails. Suggestions?

[Aaron Liu]

let instead of have

import Mathlib

lemma test {R : Type*} [Field R] (I :   Ideal (Polynomial R)) :
    ∃ p, I = Ideal.span {p} := by
  let pid := Polynomial.instEuclideanDomain (R := R)
  apply EuclideanDomain.to_principal_ideal_domain at pid
  rw [isPrincipalIdealRing_iff] at pid
  specialize (pid I)
  -- unsolved goals

[Ruben Van de Velde]

Why do you need to mention it explicitly?

[Barry Trager]

Thanks Aaron! Now I have a more complicated variant of the same issue :

lemma jacobson_max_gens {R : Type*} [CommRing R] [IsJacobsonRing R] (M : Ideal (Polynomial R)) (h : M.IsMaximal) :
      ∃ (g : Polynomial R), M = Ideal.span {g} + (Ideal.comap Polynomial.C M).map Polynomial.C := by
  have max := Polynomial.isMaximal_comap_C_of_isJacobsonRing (R := R) M
  let MR :=  (Ideal.comap Polynomial.C M)
  have fi : Field (R ⧸ MR) := by apply Ideal.Quotient.field
  let pid := Polynomial.instEuclideanDomain (R := R ⧸ MR)
  apply EuclideanDomain.to_principal_ideal_domain at pid
  rw [isPrincipalIdealRing_iff] at pid
  let F := Polynomial.mapRingHom (Ideal.Quotient.mk MR)
  let MS := M.map F

  specialize (pid MS)

again, the specialization fails, how do I convert MS to a valid argument for the pid

[Weiyi Wang]

-have fi : Field (R ⧸ MR) := by apply Ideal.Quotient.field
+let fi : Field (R ⧸ MR) := by apply Ideal.Quotient.field

[Barry Trager]

yes!, thanks all, I guess I need to understand better when I need to use let

[Weiyi Wang]

I suspect there are still non-optimal things in the code. Worrying about let vs have for instances is not common

[Weiyi Wang]

lemma jacobson_max_gens {R : Type*} [CommRing R] [IsJacobsonRing R] (M : Ideal (Polynomial R)) (h : M.IsMaximal) :
      ∃ (g : Polynomial R), M = Ideal.span {g} + (Ideal.comap Polynomial.C M).map Polynomial.C := by
  have max := Polynomial.isMaximal_comap_C_of_isJacobsonRing (R := R) M
  let MR :=  (Ideal.comap Polynomial.C M)
  let fi : Field (R ⧸ MR) := by apply Ideal.Quotient.field
  obtain pid := (isPrincipalIdealRing_iff (Polynomial (R ⧸ MR))).mp inferInstance
  let F := Polynomial.mapRingHom (Ideal.Quotient.mk MR)
  let MS := M.map F

  specialize (pid MS)

A bit shorter

[Barry Trager]

nice, thanks for the suggestions

[Kenny Lau]

Barry Trager said:

yes!, thanks all, I guess I need to understand better when I need to use let

when you're making things with data, you need to use let to remember the definition

[Kenny Lau]

have forgets the definition

[Kenny Lau]

so you just know that you have an arbitrary field structure