Diamond in `Algebra.Generators`

Stream: mathlib4

[Christian Merten]

I am encountering the following instance diamond, induced by the algebra instance docs#Algebra.Generators.instRing:

import Mathlib.RingTheory.Generators

open Algebra MvPolynomial

variable {R ι : Type} [CommRing R] (I : Ideal (MvPolynomial ι R))

abbrev ring : Type := MvPolynomial ι R ⧸ I

lemma quotient_mk_comp_X_surjective : Function.Surjective (aeval (R := R) (Ideal.Quotient.mk I ∘ X)) := by
  rw [show aeval (Ideal.Quotient.mk I ∘ X) = Ideal.Quotient.mkₐ R I by ext; simp]
  exact Ideal.Quotient.mkₐ_surjective R I

noncomputable abbrev gens : Generators R (ring I) where
  vars := ι
  val i := Ideal.Quotient.mk I (X i)
  σ' x := (quotient_mk_comp_X_surjective I x).choose
  aeval_val_σ' x := (quotient_mk_comp_X_surjective I x).choose_spec

example : (gens I).instRing = Ideal.Quotient.algebra (gens I).Ring := rfl

I think this will be a very common use case of the generators (and in particular of the upcoming Algebra.Presentation) API. Can we make that instance non-default and define all data in terms of aeval P.val for P : Generators R S?

[Christian Merten]

(probably @Andrew Yang has an opinion?)

[Christian Merten]

(Note that there is docs#Algebra.Generators.ofAlgHom, which can be used to define gens like so

noncomputable abbrev gens : Generators R (ring I) :=
  Generators.ofAlgHom (Ideal.Quotient.mkₐ R I) (Ideal.Quotient.mkₐ_surjective R I)

which hides the Algebra (gens I).ring (MvPolynomial ι R) instance needed for Ideal.Quotient.algebra. But this also means hiding (gens I).vars which creates more issues in my application)

[Kevin Buzzard]

I was also having troubles with quotients being algebras here.

[Andrew Yang]

The right thing to do here is to make Algebra.Generators.Ring a def not abbrev I think.