Zulip Chat Archive

Stream: maths

Topic: injectivity of localization map


view this post on Zulip Filippo A. E. Nuccio (Sep 10 2020 at 12:24):

I have a domain RR and its field of fractions KK with the localization map f ⁣:RKf\colon R\to K and I am trying to use its injectivity to shows that two elements a,xRa,x\in R are equal knowing that they are equal in KK, so that f(a)=f(x)f(a)=f(x). But I guess I am poorly using the command submonoid.localization_map.to_map_injective. Indeed, If I apply apply submonoid.localization_map.to_map_injective f I get the error `type mismatch at application

submonoid.localization_map.to_map_injective f

term f has type

fraction_map R K : Type (max u_1 u_2)

but is expected to have type

?m_6.to_map = ?m_7.to_map : Prop`

If I try to read the error, it seems to me that it wants a proof that two things are equal, but the syntax seems to suggest that it wants a proof that two localization maps coincide. Is it the case?

view this post on Zulip Reid Barton (Sep 10 2020 at 12:25):

based on the error message, what if you just delete f?

view this post on Zulip Filippo A. E. Nuccio (Sep 10 2020 at 12:26):

invalid apply tactic, failed to unify
a = x
with
?m_6 = ?m_7

view this post on Zulip Reid Barton (Sep 10 2020 at 12:27):

Oh, this is not the lemma you want--it says that the function assigning to a localization_map its underlying function is injective.

view this post on Zulip Filippo A. E. Nuccio (Sep 10 2020 at 12:27):

and If I replace f with the proof that f(x)=f(x)f(x)=f(x) (called haxf) it becomes

`type mismatch at application

submonoid.localization_map.to_map_injective haxf

term haxf

has type
⇑(localization_map.to_map f) a = ⇑(localization_map.to_map f) x
but is expected to have type
?m_6.to_map = ?m_7.to_map
`

view this post on Zulip Filippo A. E. Nuccio (Sep 10 2020 at 12:27):

Ah, I see!

view this post on Zulip Filippo A. E. Nuccio (Sep 10 2020 at 12:27):

It makes sense with the error I get.

view this post on Zulip Reid Barton (Sep 10 2020 at 12:28):

Looks like the one you want is docs#fraction_map.injective

view this post on Zulip Filippo A. E. Nuccio (Sep 10 2020 at 12:30):

Great! I am trying now...

view this post on Zulip Filippo A. E. Nuccio (Sep 10 2020 at 12:31):

YES! Thanks so much!

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 13:33):

Everything is set up in perhaps a slightly confusing way for people who think about stuff like fields of fractions in a very concrete way. We've seen situations where we want isomorphic non-equal things to both be "the" field of fractions of something in mathematics, so we have a concrete story where we give an example field of fractions and also a universal theory where we develop some of the theory for anything satisfying the universal property.


Last updated: May 10 2021 at 08:14 UTC