Module structure diamond?

Stream: mathlib4

[David Loeffler]

I was struggling just now to get a trivial-looking lemma about polynomials to work. The culprit seems to be that we have two ways of exhibiting a ℤ-module structure on the p-adic integers ℤ_[p], and Mathlib is unable to show that they are the same. (Is this what people here call a "diamond"?)

Here's the best I can do for a MWE:

import Mathlib

example {p : ℕ} [hp : Fact p.Prime] : AddCommGroup.toIntModule ℤ_[p] = (Int.castRingHom ℤ_[p]).toModule := by rfl
/- tactic 'rfl' failed, the left-hand side
  AddCommGroup.toIntModule ℤ_[p]
is not definitionally equal to the right-hand side
  (Int.castRingHom ℤ_[p]).toModule -/

I have no idea how to fix this, and I would be grateful for any insights from the community.

(Tagging @Scott Carnahan since I ran into this while trying to implement a suggestion of his on my Mahler-basis PR.)

[Yaël Dillies]

Can you click in the infoview on the AddCommGroup.toIntModule to see what concrete instance about ℤ_[p] it is coming from?

[Yaël Dillies]

Actually, why do you have (Int.castRingHom ℤ_[p]).toModule in your goal?

[Yaël Dillies]

docs#RingHom.toModule has a big warning docstring saying it can create diamonds when used

[Yaël Dillies]

Nevermind, it doesn't. It really should! :grinning:

[Yaël Dillies]

Here is my suggestion, concretely: Go through your code, find the first mention of RingHom.toModule and try eliminating it

[David Loeffler]

Go through your code, find the first mention of RingHom.toModule and try eliminating it

I didn't introduce it myself; it crept into my goal because I had invoked the library lemma Polynomial.eval₂_eq_smeval, whose statement explicitly invokes RingHom.toModule. The code for that lemma is

theorem eval₂_eq_smeval (R : Type*) [Semiring R] {S : Type*} [Semiring S] (f : R →+* S) (p : R[X]) (x : S) :
  letI : Module R S := RingHom.toModule f
  p.eval₂ f x = p.smeval x := by
...

This lemma was added in @Scott Carnahan 's PR #10057.

[Yaël Dillies]

That lemma is indeed badly stated. You should not create the R-module structure on S on the fly, but take in an arbitrary one and assume it is equal to RingHom.toModule f

[Eric Wieser]

I would guess that f should be replaced with docs#RingHom.smulOneHom

[Yaël Dillies]

Here I guess all it takes is replacing the letI by [Module R S] (hf : ∀ r x, r • x = f r * x)

[Yaël Dillies]

... or what Eric said

[Eric Wieser]

Either approach is reasonable

[David Loeffler]

PR up at #18410