## Stream: maths

### Topic: injectivity of localization map

#### Filippo A. E. Nuccio (Sep 10 2020 at 12:24):

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 (Sep 10 2020 at 12:25):

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

#### Filippo A. E. Nuccio (Sep 10 2020 at 12:26):

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

#### 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.

#### Filippo A. E. Nuccio (Sep 10 2020 at 12:27):

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

Ah, I see!

#### Filippo A. E. Nuccio (Sep 10 2020 at 12:27):

It makes sense with the error I get.

#### Reid Barton (Sep 10 2020 at 12:28):

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

#### Filippo A. E. Nuccio (Sep 10 2020 at 12:30):

Great! I am trying now...

#### Filippo A. E. Nuccio (Sep 10 2020 at 12:31):

YES! Thanks so much!

#### 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