central localizations

Stream: general

[Reid Barton]

It would be useful to generalize our theory of localizations of commutative monoids to localizations of arbitrary monoids at a central submonoid. This is nicely written up in this nlab page.
How should we manage the "central" hypothesis though? Do we have anything like this already, perhaps in the context of polynomials?

[Reid Barton]

Possibilities include using bundled central submonoids (but this sounds sort of annoying in the common case of a commutative ring?) or a type class is_central {M : Type*} [monoid M] (S : submonoid M) (but we always seem to change our minds about using type classes eventually?)

[Kevin Buzzard]

We bundled normal subgroups as well as subgroups when we made the group theory game

[Reid Barton]

OK, good example because every subgroup of an abelian group is also normal.

[Kevin Buzzard]

I was expecting it to be annoying but it wasn't too bad

[Reid Barton]

so currently in group_theory.quotient_group I see

variables {G : Type u} [group G] (N : subgroup G) [nN : N.normal]

[Kevin Buzzard]

yeah

[Reid Barton]

where normal is apparently a structure-class

[Kevin Buzzard]

but over the summer some students and I proved Sylow 1 from scratch

[Kevin Buzzard]

like literally our own definition of group

[Reid Barton]

with an instance lemma normal_of_comm {G : Type*} [comm_group G] (H : subgroup G) : H.normal

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/group-theory-game

[Kevin Buzzard]

and in that repo we bundled normal subgroups.

[Reid Barton]

ah, I see

[Kevin Buzzard]

and so we could have subgroup.comap and normal.comap

[Reid Barton]

For that matter, I wonder what the odd order formalization did here

[Reid Barton]

It could be that there are very few places currently where we actually build a submonoid that will end up getting passed to localization

[Johan Commelin]

Probably in the construction of fraction fields, localisation at a prime, ..., and that's it?

[Reid Barton]

There's also inverting a single element. That one would need the element to be central, and I guess the two you mentioned need a commutative ring to be sensible.

[Reid Barton]

OK, so the bundled option seems painless enough...

[Reid Barton]

Is it worth doing https://ncatlab.org/nlab/show/Ore+localization? I don't have any use for it currently but I was vaguely aware of its existence (it's somewhat related to homotopy categories).

[Kevin Buzzard]

It shows up in non-abelian Iwasawa theory as well