localization_map

Stream: general

[Kenny Lau]

LL70-76, src/group_theory/monoid_localization.lean reads:

/-- The type of add_monoid homomorphisms satisfying the characteristic predicate: if `f : M →+ N`
satisfies this predicate, then `N` is isomorphic to the localization of `M` at `S`. -/
@[nolint has_inhabited_instance] structure localization_map
  extends add_monoid_hom M N :=
(map_add_units' : ∀ y : S, is_add_unit (to_fun y))
(surj' : ∀ z : N, ∃ x : M × S, z + to_fun x.2 = to_fun x.1)
(eq_iff_exists' : ∀ x y, to_fun x = to_fun y ↔ ∃ c : S, x + c = y + c)

I'm wondering whether we could as well have just defined it as a map M →+ N that induces an isomorphism localization M S ≃+ N (expressed howsoever), or even just an isomorphism localization M S ≃+ N. What's the difference?

[Kevin Buzzard]

This is easier to use. I guess both definitions are equivalent, but these are the three properties which we have isolated as being super-useful when proving things about localisations.