Canonical injection into the localization

Stream: Is there code for X?

[Yaël Dillies]

What is the idiomatic way to spell the canonical injection from a cancellative commutative monoid α to its localization localization s at a submonoid s? I'm really confused reading file#group_theory/monoid_localization.

[Eric Rodriguez]

I mean, it's not always injective

[Yaël Dillies]

Edited the crucial word in

[Adam Topaz]

Isn’t it just docs#localization_map ?

[Adam Topaz]

Modulo namespaces

[Adam Topaz]

If you use rings, then it would be an algebra_map but it seems you want to localize multiplicative monoids?

[Adam Topaz]

Btw I think it can be noninjective even for cancellative monoids

[Yaël Dillies]

Too bad, I proved it was injective in #18724!

[Yaël Dillies]

It's also "just" docs#localization.monoid_of or "just" docs#localization.mk. What I don't know is what's preferred.

[Adam Topaz]

Too bad. You didn’t say commutative in your original post.

[Yaël Dillies]

The correct amount of qualifiers should be inferred from the context :sweat_smile:

[Yaël Dillies]

For my defence, the entire file is about commutative monoids.

[Adam Topaz]

@Yaël Dillies in case you're curious: https://link.springer.com/article/10.1007/BF01571659

[Adam Topaz]

so are you saying that we can't localize noncommutative monoids (with current mathlib)?

[Yaël Dillies]

Indeed, that's my understanding.

[Johan Commelin]

We have Ore localizations, I think

[Yaël Dillies]

Oh right! I know nothing of those.

[Yaël Dillies]

... not that I care, because my result (#18724) only holds for commutative semigroups.

[Johan Commelin]

src/ring_theory/ore_localization/basic.lean

[Eric Wieser]

Do the notions coincide in the commutative case?

[Riccardo Brasca]

Eric Wieser said:

Do the notions coincide in the commutative case?

Yep

[Reid Barton]

semigroups? I'm confused

[Reid Barton]

Looking at the PR it doesn't use semigroups, so now I am less confused.

[Reid Barton]

BTW Ore localizations also exist for monoids even though they are in the ring_theory subdirectory for some reason--it's calculus of fractions stuff.

[Yaël Dillies]

Yeah, my result holds for nonempty semigroups but I can't state it as such with current mathlib.

[Reid Barton]

I think the empty semigroup also embeds in an ordered group. :upside_down:

[Yaël Dillies]

Yeah, but its Grothendieck group isn't a group!

[Reid Barton]

Surely, if the "Grothendieck group" of a semigroup means something, then then it is a group. The question is how to define it, how to compute it, and whether, if I start with a monoid, the Grothendieck group changes if I regard it instead as a semigroup.

[Yaël Dillies]

The paper I'm following defines localization (⊤ : subsemigroup α) and then claims it's a group without mentioning the possibility of it being empty.

[Johan Commelin]

Where α has an ambient structure of semigroup, or something stronger?

[Yaël Dillies]

comm_semigroup α is what the paper claims is sufficient (and I believe it, except for adding nonempty α)

[Johan Commelin]

Every map from an empty (comm)semigroup α to a group G factors uniquely via a group with one element. So do you really need to add that assumption?

[Yaël Dillies]

Am I right in saying that localization (⊤ : subsemigroup empty) is empty? If so, yes I do need that assumption to follow the paper's argument.

[Yaël Dillies]

I'm sure there's a separate argument that works for empty semigroups, just not the one that the paper is offering.

[Reid Barton]

I am not sure a priori that localization of semigroups makes sense at all.

[Yaël Dillies]

Read the paper :wink:

[Reid Barton]

Because "invertibility" of elements of a semigroup is not preserved by homomorphisms, like it is for monoids.

[Johan Commelin]

Yaël Dillies said:

Am I right in saying that localization (⊤ : subsemigroup empty) is empty? If so, yes I do need that assumption to follow the paper's argument.

That depends on what localization means. Despite suggestively writing it between backticks, I don't think Lean can answer that question in the current context.

[Reid Barton]

You are confusing the construction and the definition. I totally agree that the same construction used to define the Grothendieck group of a commutative monoid can also be applied to a commutative semigroup provided that the semigroup is nonempty.

[Reid Barton]

But I don't know what it means (if anything) to say that the result is the "localization of the semigroup" at all its elements.

[Reid Barton]

A thing you can definitely do is consider the universal abelian group with a map of semigroups from your original commutative semigroup A, and I believe it will be the thing in the paper if A is nonempty and the zero group if A is empty.

[Yaël Dillies]

Yeah that's probably the correct answer in general