Zulip Chat Archive

Stream: general

Topic: Diamond in number_field


David Ang (Feb 25 2022 at 18:46):

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 (Feb 25 2022 at 19:20):

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 (Feb 25 2022 at 20:03):

I guess it's the scalar action that disagrees?

Eric Wieser (Feb 25 2022 at 20:04):

Unfortunately our clever new ext lemmas make this harder to debug

Eric Wieser (Feb 25 2022 at 20:05):

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 (Feb 27 2022 at 17:21):

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 (Feb 27 2022 at 17:22):

The first goal unfolds to:

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

Anne Baanen (Feb 27 2022 at 17:24):

Which congrs to:

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

Anne Baanen (Feb 27 2022 at 17:25):

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 (Feb 27 2022 at 17:26):

(c.f. #12331)

Eric Wieser (Feb 27 2022 at 17:53):

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 (Feb 27 2022 at 17:53):

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

Eric Wieser (Feb 27 2022 at 17:54):

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

Eric Wieser (Feb 27 2022 at 17:55):

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


Last updated: Dec 20 2023 at 11:08 UTC