Zulip Chat Archive

Stream: new members

Topic: is_regular


view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 17 2021 at 14:14):

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

view this post on Zulip Damiano Testa (Feb 17 2021 at 14:15):

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

view this post on Zulip Johan Commelin (Feb 17 2021 at 14:16):

I guess we can define this for arbitrary has_muls?

view this post on Zulip Damiano Testa (Feb 17 2021 at 14:18):

I guess so: the definition only uses multiplication!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Damiano Testa (Feb 17 2021 at 14:38):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 17 2021 at 14:40):

ra.mul_left_inj

view this post on Zulip Johan Commelin (Feb 17 2021 at 14:41):

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

view this post on Zulip 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!).

view this post on Zulip 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

view this post on Zulip Damiano Testa (Feb 17 2021 at 14:43):

And also the version with with_zero assuming non-zero!

view this post on Zulip 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

view this post on Zulip Damiano Testa (Feb 17 2021 at 14:43):

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

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Feb 17 2021 at 14:47):

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

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Feb 17 2021 at 14:48):

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

view this post on Zulip Damiano Testa (Feb 17 2021 at 14:50):

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

We should definitely keep the two then!

view this post on Zulip Damiano Testa (Feb 17 2021 at 14:55):

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

view this post on Zulip Damiano Testa (Feb 17 2021 at 15:05):

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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:05):

Right now we have the following problem:

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 17 2021 at 15:07):

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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 17 2021 at 15:12):

Johan, you mean outside the is_regular namespace, right?

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:15):

@Damiano Testa exactly

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:15):

the fully qualified name should be is_unit.is_regular

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:15):

But I made DVRs and made essentially 0 API

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:16):

and it just kind of organically grew

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:17):

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

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:18):

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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:18):

I am just asking them to prove one novel lemma

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:23):

@Kevin Buzzard does :up: make sense?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:26):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:27):

random lemmas created on zulip sometimes get PR'ed.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:27):

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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:27):

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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:27):

but it's still not there

view this post on Zulip 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"

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:31):

I completely agree with that last remark!

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:32):

and then Damiano can PR regular elements?

view this post on Zulip Johan Commelin (Feb 17 2021 at 15:33):

Damiano already did that

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:33):

nice!

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:34):

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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:34):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:37):

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

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:37):

with flat modules the experiment is over

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 15:37):

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

view this post on Zulip Johan Commelin (Feb 17 2021 at 16:15):

@Kevin Buzzard #6284

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Eric Wieser (Feb 17 2021 at 16:39):

Yes, exactly

view this post on Zulip Damiano Testa (Feb 17 2021 at 16:39):

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

view this post on Zulip Eric Wieser (Feb 17 2021 at 16:40):

And of_left_right is just \<> / is_regular.mk

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 17 2021 at 16:41):

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

view this post on Zulip 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!

view this post on Zulip Damiano Testa (Feb 17 2021 at 16:43):

Thanks a lot to all!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 18 2021 at 04:36):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 _

view this post on Zulip 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)

view this post on Zulip 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 _.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 18 2021 at 04:50):

Aah, it's about the coercion

view this post on Zulip Johan Commelin (Feb 18 2021 at 04:51):

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

view this post on Zulip Damiano Testa (Feb 18 2021 at 04:51):

Ok, I will keep this version then!

view this post on Zulip Damiano Testa (Feb 18 2021 at 04:55):

I just pushed this version!

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Feb 18 2021 at 07:02):

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

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 18 2021 at 08:42):

Also the symmetric versions are in.


Last updated: May 08 2021 at 09:11 UTC