common left/right multiples

Stream: Is there code for X?

[Hannah Fechtner]

I am wondering if there already is infrastructure to add "has common right multiples" to a class? Ex: one might have a monoid with common right multiples (for all a and b in the monoid, there exist c and d in the monoid such that ac=bd).

The only place I have seen this mentioned is in the OreSet file. (An OreSet essentially is a cancellative monoid with common multiples).

End goal: I am working on applying the Ore Localization to a braid monoid (which is a presented monoid that is cancellative and has left/right common multiples). So somehow I will need to combine presented monoid and ore set. My current thought is to do PresentedMonoid + IsCancelMul + (a new mixin I make for common multiples), but I am very open to suggestions otherwise!

[Kevin Buzzard]

(note that Zulip slightly mangled your post because you didn't quote a*b=c*d so it interpreted it as "emphasize b=c as it's a word enclosed by *s").

I don't think a prop-valued mixin is going to cause too many problems and my instinct is that it might be a nice way to solve your problem. I don't recall having seen the concept before in mathlib. If you go via the mixin route then probably you have to make an additive version too but this will just boil down to putting @[to_additive] in front of all your lemmas and writing the definition twice.

[Hannah Fechtner]

Thanks! Ideally, I'd like to make it carry data (functions which give the left-hand factors to make the common multiple), like so:

/-- A mixin for common left multiples. -/
class LeftCommonMul (G : Type u) [Mul G]  where
  cl₁ : G → G → G
  cl₂ : G → G → G
  cl_spec : ∀ (a b : G), cl₁ a b * a = cl₂ a b * b

So it cannot be a prop-valued mixin. Since it's carrying data, should it not be a mixin? Is there anywhere I can read up on this? I've been looking at Eric Wieser's thesis

[Yaël Dillies]

This looks fine as a Type-valued mixin on a purely technical point of view. However the data is highly non-canonical, right? Why do you need it to be data?

[Hannah Fechtner]

I am not certain that I do! My current thought process: I would like to make everything constructive when I can. Also, for my particular use case, there is a canonical common multiple in the braid monoid (built of delta braids, which are basically half-twists)

[Yaël Dillies]

Hannah Fechtner said:

I would like to make everything constructive when I can

That's not how we do it in mathlib :sweat_smile:

Hannah Fechtner said:

for my particular use case, there is a canonical common multiple

This might be a convincing argument, but in what exactly is it canonical?

[Hannah Fechtner]

Basically, when I proved that the braid monoid has common left multiples, I constructed the multiples. I'd prefer, if possible, not to lose that information when I prove that the braid monoid is a LeftCommonMul and then state theorems about LeftCommonMul structures. Does that make sense?

[Yaël Dillies]

I hear this, but is it not imaginable that someone one day proves that the braid monoid has left common multiples by a different choice of multiples? or maybe only different in some cases? or even equal but not definitionally so?

[Hannah Fechtner]

that is surely possible!

[Hannah Fechtner]

I am happy to switch it. I am very much out of my league in terms of understanding how this all works. Would you be able to explain why the OreSet instance looks more like "data" and this shouldn't be? Not questioning you, just confused about what mixins are!

[Hannah Fechtner]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/OreLocalization/OreSet.html#OreLocalization.OreSet

[Yaël Dillies]

(pro-tip: type docs#OreLocalization.OreSet and it will render as docs#OreLocalization.OreSet)

[Yaël Dillies]

Hannah Fechtner said:

Would you be able to explain why the OreSet instance looks more like "data" and this shouldn't be?

Hmm, no, they are very similar indeed, unless numerators and denominators in an Ore set are unique somehow? I dont think they are

[Yaël Dillies]

In that case, my concerns about non-canonicity might be unfounded

[Kevin Buzzard]

Yes when you localise there is no canonical choice of numerator or denominator in general. If R is an integral domain with field of fractions K and if x is in K then the ideal of denominators of x is the elements of R which when you multiply by x you remain in R. This is an ideal but in general it's not even principal!

[Hannah Fechtner]

so would the preferred method be to define it as

/-- A mixin for common left multiples. -/
class LeftCommonMul (G : Type u) [Mul G]  where
  common_left_mul  : ∀ (a b : G), ∃(c d : G), c * a = d * b

[Yaël Dillies]

That certainly looks safe. To be clear, your previous approach might be fine. It simply has the possibility not to be, and I can't tell you for sure whether it will or not