Regular Elements

Stream: Is there code for X?

[Xavier Xarles]

I want to understand how to do a basic construction on lean4.
Given a semigroup M, it is defined that an element m is regular if multiplication by m is injective on both sides. The set of regular elements forms a subsemigroup. But if the semigroup M is a monoid, then it is a submonoid (i.e. it contains 1). So if one defines Regulars M as this subsemigroup, how can I say to lean4 that if M is a monoid, then Regulars M is a submonoid?

import Mathlib.GroupTheory.Submonoid.Membership

def Regulars (M : Type*) [Semigroup M]: Subsemigroup M where
  carrier := {x | IsRegular x}
  mul_mem' ra rb :=
    { left := IsLeftRegular.mul ra.left rb.left,right := IsRightRegular.mul ra.right rb.right }

lemma Regulars_one (M : Type*) [Monoid M]: (1:M) ∈ Regulars M:= isRegular_one

[Andrew Yang]

The idiomatic way is probably to define a separate

def Submonoid.regulars : Submonoid M where
  __ := SubSemigroup.regulars M
  one_mem' := isRegular_one

[Xavier Xarles]

Thanks. By the way, do you think it is better to call them Regulars, Cancellables, or any other option...

[Junyan Xu]

It's already called docs#IsRegular in mathlib

[Andrew Yang]

I think Regulars is good enough as it mirrors the naming convention of docs#IsUnit and docs#Units.

[Xavier Xarles]

But IsRegular is a property of the elements of a set with a multiplication, and here we are considering the set of all elements verifying this property (as a subsemigroup). That is why I suggest "Regulars", in the same way the subgroup of elements verifying IsUnit is called Units

[Andrew Yang]

Hmmm. The corresponding thing is actually called docs#IsUnit.submonoid though.

[Jireh Loreaux]

Part of the reason for this distinction is that docs#Units carries extra data around (the inverse of each element).

[Jireh Loreaux]

So docs#Units is actually not a subtype of the monoid from whence it came.

[Jireh Loreaux]

Also, this is slightly different, but closely related: we have docs#RegularNormedAlgebra

[Xavier Xarles]

Then, what it is different is docs#nonZeroDivisors (although it is true there is no IsnonZeroDivisor).

[Xavier Xarles]

So at the end probably the best option is IsRegular.subsemigroup and IsRegular.submonoid (and their Left and Right avatars also...). And may be the Add versions. :sweat_smile:

[Xavier Xarles]

By the way, with all these I can show the following result that I think it will be interesting to have in Mathlib, that characterizes when the localization map is injective (for monoids).

theorem Submonoid.LocalizationMap.injective_iff (R : Type*) (S : Type*)  [CommMonoid R]
    {M : Submonoid R} [CommMonoid S] (f : Submonoid.LocalizationMap M S):
    ( M ≤ IsLeftRegular.submonoid R) ↔  Injective (Submonoid.LocalizationMap.toMap f) := by sorry

[Yaël Dillies]

Honestly I think you should just have one Regulars type and write more and more instances on it. Subobjects are only useful for the small amount of API they provide, like "a submonoid is closed under finite products".

[Yaël Dillies]

See eg docs#UpperSet for this design

[Xavier Xarles]

I don't really understand the design you propose. In my example, how it will be?

[Yaël Dillies]

Something like Injective (Submonoid.LocalizationMap.toMap f ↔ ∀ ⦃x⦄, x ∈ M → IsLeftRegular x

[Xavier Xarles]

That's clearly a simpler result. But we will need some Regulars as a Submonoid if in the future we would like to have something like docs#FractionRing for CommSemirings, as

def FractionSemiring (R : Type*) [CommSemiring R]:=
  Localization (Regulars R)

[Xavier Xarles]

I made the PR #9531 with the Injective_iff result for Monoids, as well as some result generalizing docs#IsLocalization.isDomain_localization to MonoidsWithZero. If somebody likes to review or criticize (it is my first real proof in Mathlib4).

[Yaël Dillies]

Xavier Xarles said:

That's clearly a simpler result. But we will need some Regulars as a Submonoid if in the future we would like to have something like docs#FractionRing for CommSemirings, as

def FractionSemiring (R : Type*) [CommSemiring R]:=
  Localization (Regulars R)

That's typically the use-cases for Regulars bundled as a submonoid. But as you see it's used inside a definition and should basically rarely (if ever) leak out.

[Xavier Xarles]

Anyway, I still don't understand how to define Regulars (in a Semigroup) giving a Subsemigroup, and then be able to have instances in Monoid, for example, as Submonoid.

[Junyan Xu]

You can actually define it as a Subsemigroup but give it a docs#SubmonoidClass instance when in a Monoid, and submonoid lemmas will apply to it. You will get a Monoid structure on the coerced type too, via docs#SubmonoidClass.toMonoid. Nope, that doesn't work, unless every subsemigroup in a monoid contains 1, which is not the case ...