Zulip Chat Archive

Stream: maths

Topic: localization.of


view this post on Zulip Johan Commelin (Feb 26 2019 at 15:11):

At some point there was some discussion about this (maybe on Github). Anyway, currently we have in ring_theory/localization.lean
https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/localization.lean#L71
a line reading

def of (r : α) (s : S) : loc α S := (r, s)

But we don't have an explicit name for the ring morphism from R to localization R S. Currently the file uses \lam x, of x 1 which is not very user friendly. I would expect that this ring morphism would be called localization.of. What are others opinions on this? Would it be OK to rename the current of to mk?

view this post on Zulip Chris Hughes (Feb 26 2019 at 15:17):

I would rename of to mk

view this post on Zulip Johan Commelin (Feb 26 2019 at 15:18):

Do you want a PR?

view this post on Zulip Johan Commelin (Feb 26 2019 at 15:18):

@Kenny Lau What is your opinion?

view this post on Zulip Kenny Lau (Feb 26 2019 at 15:21):

just PR what you want :}

view this post on Zulip Kevin Buzzard (Feb 26 2019 at 17:09):

I independently ran into this the other day. I definitely vote for a name other than of x 1.

view this post on Zulip Johan Commelin (Feb 26 2019 at 18:59):

On the other hand, should S be an explicit parameter of of? (S is the submonoid at which we localise.)

view this post on Zulip Chris Hughes (Feb 26 2019 at 19:58):

It's inferred by the type of s

view this post on Zulip Johan Commelin (Feb 26 2019 at 19:59):

s = 1

view this post on Zulip Johan Commelin (Feb 26 2019 at 19:59):

For mk I agree


Last updated: May 19 2021 at 02:10 UTC