Zulip Chat Archive

Stream: new members

Topic: failed to unify identical things?

Filippo A. E. Nuccio (Oct 19 2020 at 11:57):

I am very perplexed by the following error I am getting

invalid apply tactic, failed to unify
  is_integral R x
with
  is_integral R x

I can produce a mwe, but I am wondering if there might be something hidden preventing me to see that the two is_integral R x are not actually the same thing.

Anne Baanen (Oct 19 2020 at 11:57):

Have you tried set_option pp.all true?

Filippo A. E. Nuccio (Oct 19 2020 at 11:57):

Before the beginning of the lemma?

Anne Baanen (Oct 19 2020 at 11:58):

Yes

Anne Baanen (Oct 19 2020 at 11:58):

Another trick is to use the convert tactic instead of apply, then it should make a goal for the terms that don't match.

Filippo A. E. Nuccio (Oct 19 2020 at 11:59):

OK, with the set_option pp.all true I think I see that they are not equal (although the error is some 50 lines long and I can't read it). I' ll try with convert and see what happens.

Filippo A. E. Nuccio (Oct 19 2020 at 12:03):

Thanks! The situation evolved (not that I'm in an extremely nice position, now). I keep on fighting with the fact that fractional ideals are defined in terms of the localizing morphism $f$ , but the localization of $R$ at $S$ (eg at $S=R\setminus 0$ ) is not defined as an $R$ -algebra but only as a ring.

Johan Commelin (Oct 19 2020 at 12:04):

Hmm, f.codomain should have an algebra instance, I think

Filippo A. E. Nuccio (Oct 19 2020 at 12:04):

I somehow found it, I think it is ring_hom.to_algebra f.to_map.

Filippo A. E. Nuccio (Oct 19 2020 at 12:06):

Yet when I try to compare f.codomain with K they are different things when it gets to very deep coercions (at least this is how interpret the following error):

term
  A
has type
  @subalgebra R K (@comm_ring.to_comm_semiring R (@integral_domain.to_comm_ring R _inst_3))
    (@ring.to_semiring K (@division_ring.to_ring K (@field.to_division_ring K _inst_2)))
    h_KRalg
but is expected to have type
  @subalgebra R K (@comm_ring.to_comm_semiring R (@integral_domain.to_comm_ring R _inst_3))
    (@ring.to_semiring K (@division_ring.to_ring K (@field.to_division_ring K _inst_2)))
    h_RalgK

Reid Barton (Oct 19 2020 at 12:08):

Well, this one is easy for now: one of them uses h_KRalg (whatever that is) while the other uses h_RalgK (whatever that is).

Filippo A. E. Nuccio (Oct 19 2020 at 12:10):

You're right, I am messing things up. At any rate, with Anne's advice I guess I can go a bit further in understanding what I got wrong.

Last updated: Dec 20 2023 at 11:08 UTC