Diamond in number_field

Stream: general

[David Ang]

Hi everyone! I'm very new to Zulip and hoping that I'm posting this in the right stream/channel/topic (?). I was playing around with the number_field library and I encountered something strange. This MWE (some people seem to be missing import algebraic_geometry.prime_spectrum.basic, but not me) works:

import number_theory.number_field
open_locale classical number_field
variables {R : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] (p : prime_spectrum R)
#check (associates.mk p.val).count -- this is ok

However, when I try to replace the general Dedekind domain R with the specific 𝓞 K I had in mind, the following complains that the synthesised instances are not definitionally equal (but are visually the same):

import number_theory.number_field
open_locale classical number_field
variables {K : Type} [field K] [number_field K] (p : prime_spectrum $ 𝓞 K)
#check (associates.mk p.val).count -- instance not defeq

I thought it was a diamond but couldn't figure out how to locate or fix it, so I asked this on the Xena Discord server, and @Kevin Buzzard reduced the problem, after playing around with implicit pp, to showing that:

example : semiring.to_monoid_with_zero (ideal (𝓞 K)) = comm_monoid_with_zero.to_monoid_with_zero (ideal (𝓞 K)) := sorry

There seems to be a diamond? Possibly unrelated to this, but recently I've been encountering many deterministic timeout and excessive memory issues specific to the number_field library (universe issues, computability issues) and can't help but feel something is slightly off with its instances (or possibly just be me being new to Lean). Can someone help out?

[Kevin Buzzard]

With current master the first example needs the extra import and doesn't work either. I don't know if David has discovered one issue or two issues. Here is at least one diamond on current master:

import number_theory.number_field
import algebraic_geometry.prime_spectrum.basic

open_locale classical number_field
variables {R : Type} [comm_ring R] [is_domain R] [is_dedekind_domain R] (p : prime_spectrum R)
#check (associates.mk p.val).count -- diamond

variables {K : Type} [field K] [number_field K]

attribute [ext] monoid_with_zero

example : semiring.to_monoid_with_zero (ideal ↥(𝓞 K)) =
  comm_monoid_with_zero.to_monoid_with_zero (ideal ↥(𝓞 K)) :=
begin
  -- not refl
  ext,
  { refl },
  { congr',
    ext,
    refl },
  { congr',
    ext,
    refl },
  { refl }
end

[Eric Wieser]

I guess it's the scalar action that disagrees?

[Eric Wieser]

Unfortunately our clever new ext lemmas make this harder to debug

[Eric Wieser]

I guess change monoid_with_zero.mk _ ... = monoid_with_zero.mk _ ...; congr' 1 gets you in the same place as the dumb ext lemmas

[Anne Baanen]

Looks like you're right about the scalar actions.

example : semiring.to_monoid_with_zero (ideal ↥(𝓞 K)) =
  comm_monoid_with_zero.to_monoid_with_zero (ideal ↥(𝓞 K)) :=
begin
  change monoid_with_zero.mk _ _ _ _ _ _ _ _ _ _ _ = monoid_with_zero.mk _ _ _ _ _ _ _ _ _ _ _,
  congr' 1; sorry
end

gives:

filter: no filter
▶ 2 goals
K : Type
_inst_4 : field K
_inst_5 : number_field K
⊢ semiring.one = comm_monoid_with_zero.one

K : Type
_inst_4 : field K
_inst_5 : number_field K
⊢ semiring.npow = comm_monoid_with_zero.npow

[Anne Baanen]

The first goal unfolds to:

(algebra.linear_map ↥(𝓞 K) ↥(𝓞 K)).range = (algebra.linear_map ↥(𝓞 K) ↥(𝓞 K)).range

[Anne Baanen]

Which congrs to:

number_field.ring_of_integers_algebra K K = algebra.id ↥(𝓞 K)

[Anne Baanen]

Aha, docs#number_field.ring_of_integers_algebra is the inclusion of 𝓞 K into 𝓞 L given an inclusion of K into L. Apparently this doesn't become defeq to the inclusion of 𝓞 K into itself.

[Eric Rodriguez]

(c.f. #12331)

[Eric Wieser]

This thread is basically the same as https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/diamond.20for.20monoid.20instance.20on.20ideals, right?

[Eric Rodriguez]

yes, I think this is the specific issue but now the discussion has converged

[Eric Wieser]

The diamond unfolds down to docs#subtype.coe_eta, which isn't true by refl: see this thread

[Eric Wieser]

The algebra_map formed by the identity function is not equal to the one that applies the identity function to the coercion and rebuilds the subtype, but the latter is the only reasonable way to have one subtype act on another