Stream: general

Topic: Correct way to set up an instance with non-class parameters

Paul Lezeau (Dec 18 2022 at 16:25):

I'm currently trying to prove the following theorem

import ring_theory.adjoin_root

open polynomial localization

variables {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S]
[is_domain S] [is_integrally_closed R]

example (a : S) (ha : is_integral R a) : minpoly (fraction_ring R)  (algebra_map S
(fraction_ring S) a)  ∣ (map_ring_hom (algebra_map R (fraction_ring R)) (minpoly R a)) :=
sorry


but for the statement to work I need the instance algebra (fraction_ring R ) (fraction_ring S). I wasn't able to find it in mathlib so I've tried to make my own, which yields the following MWE:

import ring_theory.adjoin_root

open polynomial localization

variables {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S]
[is_domain S]

noncomputable def frac_algebra_of_inj (h : function.injective (algebra_map R S)):
algebra (fraction_ring R) (fraction_ring S) :=
ring_hom.to_algebra (is_fraction_ring.map h)

noncomputable instance problematic_instance (h : function.injective (algebra_map R S)):
algebra (fraction_ring R) (fraction_ring S) :=
frac_algebra_of_inj h

#lint /- IMPOSSIBLE INSTANCES FOUND.
These instances have an argument that cannot be found during type-class resolution,
and therefore can never succeed. Either mark the arguments with square brackets
(if it is a class), or don't make it an instance. -/


Since this instance is wrong according to lint, what should I do?

Eric Wieser (Dec 18 2022 at 16:28):

Change h to a fact

Eric Wieser (Dec 18 2022 at 16:30):

But note that this instance might bad for reasons not found by the linter; it likely creates a diamond for the action of fraction_ring R on fraction_ring (fraction_ring R))

Kevin Buzzard (Dec 18 2022 at 16:32):

If anyone ever creates fraction_ring (fraction_ring R)) then they deserve the pain.

Paul Lezeau (Dec 18 2022 at 16:37):

Eric Wieser said:

Change h to a fact

Ok thanks, I'll try that!

Paul Lezeau (Dec 18 2022 at 16:37):

Eric Wieser said:

But note that this instance might bad for reasons not found by the linter; it likely creates a diamond for the action of fraction_ring R on fraction_ring (fraction_ring R))

Yeah I was planning on making it into a local attribute once I managed to get it work!

Last updated: Dec 20 2023 at 11:08 UTC