injectivity of localization map

Stream: maths

[Filippo A. E. Nuccio]

I have a domain $R$ and its field of fractions $K$ with the localization map $f\colon R\to K$ and I am trying to use its injectivity to shows that two elements $a,x\in R$ are equal knowing that they are equal in $K$, so that $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?

[Reid Barton]

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

[Filippo A. E. Nuccio]

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

[Reid Barton]

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

[Filippo A. E. Nuccio]

and If I replace f with the proof that $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
`

[Filippo A. E. Nuccio]

Ah, I see!

[Filippo A. E. Nuccio]

It makes sense with the error I get.

[Reid Barton]

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

[Filippo A. E. Nuccio]

Great! I am trying now...

[Filippo A. E. Nuccio]

YES! Thanks so much!

[Kevin Buzzard]

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.