## Stream: new members

### Topic: is_regular

#### Damiano Testa (Feb 17 2021 at 14:11):

Any preference for which one is left and which one is right?

Also, should the ambidextrous property be the conjunction of the other two or does it not matter?

I.e., should it be

def is_regular {R : Type*} [semiring R] (c : R) : Prop := is_left_regular c ∧ is_right_regular c


#### Johan Commelin (Feb 17 2021 at 14:14):

We could also use structures, then you can name the fields

#### Damiano Testa (Feb 17 2021 at 14:15):

I might even define them as is_lregular and is_rregular or this is too much?

#### Johan Commelin (Feb 17 2021 at 14:16):

I guess we can define this for arbitrary has_muls?

#### Damiano Testa (Feb 17 2021 at 14:18):

I guess so: the definition only uses multiplication!

#### Damiano Testa (Feb 17 2021 at 14:20):

I updated the definition above to only require has_mul. I will now think about what it means that we can use classes!

With classes now.

#### Johan Commelin (Feb 17 2021 at 14:33):

Hmm, it's better to use structure instead of class. Because you don't want to use typeclass inference, presumably.

#### Johan Commelin (Feb 17 2021 at 14:34):

And you can use dot-notation is_regular.is_left_regular if you name the lemmas appropriately

#### Damiano Testa (Feb 17 2021 at 14:38):

structure instead of class and dot-notation (if I understood correctly)!

#### Damiano Testa (Feb 17 2021 at 14:40):

Does this mean that if I then assume {a : R} (ra : is_regular a) I can access the two properties by cases ra?

#### Johan Commelin (Feb 17 2021 at 14:40):

ra.mul_left_inj

#### Johan Commelin (Feb 17 2021 at 14:41):

Maybe splitting into left and right should wait until we see a need for it.

#### Damiano Testa (Feb 17 2021 at 14:42):

Are you suggesting to remove the two or to leave them in, but not use them very much? It does seem like a good way of halving the length of the first few lemmas (at the price of doubling the number of lemmas, of course!).

#### Johan Commelin (Feb 17 2021 at 14:42):

I think what we need now is

lemma is_unit.is_regular

lemma is_regular_of_cancel_semigroup [cancel_semigroup G] (g : G) : is_regular g := -- find correct typeclass name

lemma is_regular_of_integral_domain


#### Damiano Testa (Feb 17 2021 at 14:43):

And also the version with with_zero assuming non-zero!

#### Johan Commelin (Feb 17 2021 at 14:43):

Damiano Testa said:

Are you suggesting to remove the two or to leave them in, but not use them very much? It does seem like a good way of halving the length of the first few lemmas (at the price of doubling the number of lemmas, of course!).

I don't really know. I guess it doesn't matter too much which aproach we take

#### Damiano Testa (Feb 17 2021 at 14:43):

You put the zero in, to immediately exclude it...

#### Damiano Testa (Feb 17 2021 at 14:44):

But this is definitely a case that I care about: non-zero elements being regular is definitely a case that I want to be able to talk about easily!

#### Johan Commelin (Feb 17 2021 at 14:47):

The nice thing about this definition is that it automatically excludes 0.

#### Yakov Pechersky (Feb 17 2021 at 14:47):

Of course, if it is just an and, then is_regular.left and is_regular.right still works!

#### Johan Commelin (Feb 17 2021 at 14:48):

Ooh, that's a sort of sweet hack (-;

#### Damiano Testa (Feb 17 2021 at 14:50):

Aaaahh!! Yakov, I really like this observation!!

We should definitely keep the two then!

#### Damiano Testa (Feb 17 2021 at 14:55):

I added a proof that a unit is a regular element. (Not the bundled version, though.)

#### Damiano Testa (Feb 17 2021 at 15:05):

I might PR what is above: does this seem like a good idea?

#### Kevin Buzzard (Feb 17 2021 at 15:05):

Right now we have the following problem:

#### Kevin Buzzard (Feb 17 2021 at 15:06):

People interested in commutative algebra show up, say "I'm interested in formalising flat modules / projective modules / regular sequences / regular local rings" and we say "yeah sure thing beginner, go ahead! By the way, definitions are really hard, you don't actually stand a chance"

#### Kevin Buzzard (Feb 17 2021 at 15:07):

If we just got some of these definitions into Lean, then when people show up and say "have you got flat modules?" we say "yeah sure! Feel free to prove a theorem about them" and this is _much_ easier.

#### Damiano Testa (Feb 17 2021 at 15:07):

Ok, so you are in favour of PRing this, right? Ahaha

#### Adam Topaz (Feb 17 2021 at 15:08):

I guess this has to be balanced with the fact that "every definition should come with a comprehensive API"

#### Johan Commelin (Feb 17 2021 at 15:11):

@Damiano Testa If you call the lemma is_unit.is_regular, then you can write hu.is_regular if hu : is_unit u.

#### Damiano Testa (Feb 17 2021 at 15:12):

Johan, you mean outside the is_regular namespace, right?

#### Johan Commelin (Feb 17 2021 at 15:15):

@Damiano Testa exactly

#### Johan Commelin (Feb 17 2021 at 15:15):

the fully qualified name should be is_unit.is_regular

#### Kevin Buzzard (Feb 17 2021 at 15:16):

and it just kind of organically grew

#### Johan Commelin (Feb 17 2021 at 15:17):

We want API to make sure that we chose usable defn's that allow us to develop the API without too much struggle.

#### Johan Commelin (Feb 17 2021 at 15:17):

If we are confident that the definitions are right, then the API could come later.

#### Johan Commelin (Feb 17 2021 at 15:17):

And with "right" I don't just mean maths-right. I mean "right for setting up API afterwards".

#### Kevin Buzzard (Feb 17 2021 at 15:18):

e.g. just PR flat modules anyway, and write in the module doc what needs to be done to make progress

#### Kevin Buzzard (Feb 17 2021 at 15:18):

I have students who are looking for simple projects to pass my course

#### Kevin Buzzard (Feb 17 2021 at 15:18):

I am just asking them to prove one novel lemma

#### Johan Commelin (Feb 17 2021 at 15:19):

I think there is still a lot of commutative algebra that can be done without making new definitions.

#### Damiano Testa (Feb 17 2021 at 15:21):

Ok, for the moment, here is the PR: #6282. From now on, I will concentrate on not making new definitions!

#### Damiano Testa (Feb 17 2021 at 15:22):

(At the moment, my goal is to prove that "transcendental over \Z" implies "transcendental over \Q" and for this, I was proving that you can "clear denominators in polynomials" and non-zero divisors are useful in this setting)

#### Johan Commelin (Feb 17 2021 at 15:22):

Here's another gut feeling: we always say that definitions are hard, but I think we can be more precise.

• defining a new algebraic structure can be easy. There is only one sensible definition of monoid, once mathlib has settled on the semi-bundled typeclass approach
• defining other sorts of new data can be tricky to get right. (E.g. finset, finsupp, polynomial, whatever)
• defining a predicate on terms is not so hard. You typically don't run into DTT traps there.
• defining a predicate over types can be tricky. E.g. flat, because you don't want to quantify over universes.

#### Johan Commelin (Feb 17 2021 at 15:23):

@Kevin Buzzard does :up: make sense?

#### Kevin Buzzard (Feb 17 2021 at 15:25):

If someone comes along and says "I want to prove a theorem about flat modules" we can just then ask them what their maths proof is and find the next lemma which isn't in mathlib

#### Kevin Buzzard (Feb 17 2021 at 15:26):

and then maybe they'll end up proving a lemma which mathlib wants

#### Kevin Buzzard (Feb 17 2021 at 15:26):

but with definitions we never go anywhere. At least two people have shown up here saying "I want to do flat modules" and there was no definition so they could do nothing

#### Kevin Buzzard (Feb 17 2021 at 15:27):

random lemmas created on zulip sometimes get PR'ed.

#### Kevin Buzzard (Feb 17 2021 at 15:27):

but if we're still bikeshedding about the defiinition nothing will go anywhere.

#### Kevin Buzzard (Feb 17 2021 at 15:27):

Johan already figured out what the Lean definition of a flat module was

#### Kevin Buzzard (Feb 17 2021 at 15:27):

but it's still not there

#### Kevin Buzzard (Feb 17 2021 at 15:28):

we want newcomers to go away saying "I helped to prove a theorem", not "I found out that these people can't even define flat modules witthout a lot of work"

#### Johan Commelin (Feb 17 2021 at 15:31):

I completely agree with that last remark!

#### Kevin Buzzard (Feb 17 2021 at 15:32):

so you'll PR flat module definition plus those comments about how we need Z[X] tensor R = R[X] etc?

#### Kevin Buzzard (Feb 17 2021 at 15:32):

and then Damiano can PR regular elements?

nice!

#### Kevin Buzzard (Feb 17 2021 at 15:34):

The CS people are edgy about definitions but by now we know what we're doing.

#### Kevin Buzzard (Feb 17 2021 at 15:34):

e.g. we know you have the right definition of flat

#### Kevin Buzzard (Feb 17 2021 at 15:36):

I made a definition of DVR and remarked that there were 10 other definitions in wikipedia and left it at that. Two months later I came back because I needed equivalence of it with another one, and you had filled in a ton of API because of the Witt vector work.

#### Johan Commelin (Feb 17 2021 at 15:36):

we still don't know the right definition of chain complex... even though it is in mathlib

#### Kevin Buzzard (Feb 17 2021 at 15:37):

that's a different story though, there we are actively experimenting and we know it

#### Kevin Buzzard (Feb 17 2021 at 15:37):

with flat modules the experiment is over

#### Kevin Buzzard (Feb 17 2021 at 15:37):

I am still scared of definitions but I will prove theorems in my spare time

#### Johan Commelin (Feb 17 2021 at 16:15):

@Kevin Buzzard #6284

#### Damiano Testa (Feb 17 2021 at 16:24):

Btw, in the meantime, I pushed proofs that elements of (left/right_)cancel_monoids and non-zero elements of integral_domains are all regular.

#### Damiano Testa (Feb 17 2021 at 16:39):

If I understand correctly, with Eric's definition below, I no longer need to define left and right, ... right?

def is_left_regular [has_mul R] (c : R) := function.injective ((*) c))
def is_right_regular [has_mul R] (c : R) := function.injective (* c))

structure is_regular [has_mul R] (c : R) :=
(left : is_left_regular c)
(right : is_right_regular c)


Yes, exactly

#### Damiano Testa (Feb 17 2021 at 16:39):

Ok, thank you! The more I look at this definition, the more I like it!

#### Eric Wieser (Feb 17 2021 at 16:40):

And of_left_right is just \<> / is_regular.mk

#### Eric Wieser (Feb 17 2021 at 16:41):

You can then change the types of docs#mul_left_injective (which I think already exists) to be the is_left_regular etc

#### Eric Wieser (Feb 17 2021 at 16:41):

This raises a question - should is_regular apply to the additive case too?

#### Damiano Testa (Feb 17 2021 at 16:43):

I am not sure that I understand the mul_left_injective comment, and I need to go now!

I will look at it later, likely tomorrow or Friday!

#### Damiano Testa (Feb 17 2021 at 16:43):

Thanks a lot to all!

#### Kevin Buzzard (Feb 17 2021 at 16:43):

It's not really a thing for additive things, there's nothing stopping someone adding a to_additive but then you'll have to think of a name for the additive version and because it doesn't really exist in real life this will just sort of be adding junk.

#### Damiano Testa (Feb 18 2021 at 04:34):

It seems that the remaining wrinkle on the PRed part of regular elements is what to do with the lemma below. There are two proposed versions for it. Which one should stay? Should they both go? Also, any further suggestions (golfing, naming,...) are as always welcome!

Thanks!

-- version 1
lemma of_mul_eq_one_mul_eq_one {a ai : R} (hr : a * ai = 1) (hl : ai * a = 1) : is_regular a :=
of_left_right (left_of_mul_eq_one hl) (right_of_mul_eq_one hr)

-- version 2
lemma unit.is_regular (a : units R) : is_regular (a : R) :=
⟨left_of_mul_eq_one a.inv_mul,  right_of_mul_eq_one a.mul_inv⟩


#### Johan Commelin (Feb 18 2021 at 04:36):

The snd version can be proved by applying is_regular_of_cancel_monoid, right?

#### Damiano Testa (Feb 18 2021 at 04:39):

Maybe it can, but I am failing to do that. Lean does not like that a : units R since it expects a : R. I will try to break a : units R apart.

#### Johan Commelin (Feb 18 2021 at 04:40):

I'm confused. units R is a group. And you have a lemma about "groups" (or something similar/weaker) a few lines up, right?

#### Damiano Testa (Feb 18 2021 at 04:42):

I had forgotten to add the cancel_monoid assumption... It does work!

/-- An element admitting a left and a right inverse is regular. -/
lemma unit.is_regular {G : Type*} [cancel_monoid G] (a : units G) : is_regular (a : G) :=
is_regular_of_cancel_monoid _


#### Damiano Testa (Feb 18 2021 at 04:43):

So, this means that if we keep one version, it is the other one, right?

-- only contender left
lemma of_mul_eq_one_mul_eq_one {a ai : R} (hr : a * ai = 1) (hl : ai * a = 1) : is_regular a :=
of_left_right (left_of_mul_eq_one hl) (right_of_mul_eq_one hr)


#### Johan Commelin (Feb 18 2021 at 04:49):

Hmm, but --version 2 doesn't need the [cancel_monoid] assumption? In that case --version 2 seems useful to keep around.
Note that it should be units.is_regular, because the type of a is units _.

#### Damiano Testa (Feb 18 2021 at 04:50):

Looking back at this, the new version is silly.

Johan, I am also confused. If I assume that R is a monoid, then the lemma

/-- An element admitting a left and a right inverse is regular. -/
lemma unit.is_regular {G : Type*} [monoid G] (a : units G) : is_regular (a : G) :=
is_regular_of_cancel_monoid _


says

type mismatch, term
is_regular_of_cancel_monoid ?m_3
has type
is_regular ?m_3
but is expected to have type
is_regular ↑a


#### Johan Commelin (Feb 18 2021 at 04:51):

Ok, I'm convinced, keeping --version 2 around is useful.

#### Damiano Testa (Feb 18 2021 at 04:51):

Ok, I will keep this version then!

#### Damiano Testa (Feb 18 2021 at 04:55):

I just pushed this version!

#### Damiano Testa (Feb 18 2021 at 04:56):

I created several sections that only contain one lemma: the idea is that more lemmas can come in, so it feels a little overkill at the moment, but it might make more sense if there are more lemmas in each section, right?

#### Damiano Testa (Feb 18 2021 at 06:35):

Eric, Johan, you really helped a lot with this file and I think that you should also be authors of it. However, I do not want to forcefully add you! So, let me know if you want to be added as authors (or directly add yourselves), or if you prefer not to!

#### Johan Commelin (Feb 18 2021 at 07:02):

I really don't care. You did the actual work.

#### Damiano Testa (Feb 18 2021 at 07:49):

Ok, in any case, I guess that git remembers the various contributions anyways.

On a separate note, I added some saturation properties for left/right_regular elements. It is a common idiom to say "products of non-zero divisors are non-zero divisors" or "a * b is a non-zero divisor implies a and b are non-zero divisors". The asymmetric versions are in. I am going to add the symmetric ones, though I will assume commutativity of multiplication for this.

#### Damiano Testa (Feb 18 2021 at 08:42):

Also the symmetric versions are in.

Last updated: May 08 2021 at 09:11 UTC