Zulip Chat Archive

Stream: maths

Topic: ore localization

Jakob von Raumer (Dec 27 2021 at 11:38):

I've been formalizing the notion of ore sets and ore localizations together with some other people and I was wondering if that should find a place in mathlib eventually. The formalization works on right ore sets instead of left ore sets. It's a generalization of group_theory.monoid_localization but I'm not sure if it should replace it since it's a bit more "out there" and there are other generalizations as well...

Johan Commelin (Dec 27 2021 at 12:10):

@Reid Barton was also working on this about a year ago, I think.

Johan Commelin (Dec 27 2021 at 12:10):

No idea if his attempts were on some branch, or on a separate project.

Yaël Dillies (Dec 27 2021 at 12:11):

branch#rwbarton-ore

Jakob von Raumer (Dec 27 2021 at 12:14):

Oh, I probably should have asked beforehand ^^

Jakob von Raumer (Dec 27 2021 at 14:05):

Nevertheless, the question still stands, should I make it a PR, maybe taking into account some of the things @Reid Barton did differently? I see that he defined the ore property as data instead of a proposition, which we chose not to, in order to make it a well-behaved type class

Yaël Dillies (Dec 27 2021 at 14:12):

What do you mean by "in order to make it a well-behaved type class"?

Jakob von Raumer (Dec 27 2021 at 14:17):

The choice of witnesses in the ore condition is very much non-unique and sometimes non-canonical, but it also doesn't seem interesting to study different ore conditions on the same submonoid