is_regular

Stream: new members

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Johan Commelin]

I guess we can define this for arbitrary has_muls?

[Damiano Testa]

I guess so: the definition only uses multiplication!

[Damiano Testa]

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]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

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]

ra.mul_left_inj

[Johan Commelin]

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

[Damiano Testa]

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]

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]

And also the version with with_zero assuming non-zero!

[Johan Commelin]

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]

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

[Damiano Testa]

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]

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

[Yakov Pechersky]

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

[Johan Commelin]

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

[Damiano Testa]

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

We should definitely keep the two then!

[Damiano Testa]

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

[Damiano Testa]

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

[Kevin Buzzard]

Right now we have the following problem:

[Kevin Buzzard]

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]

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]

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

[Adam Topaz]

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

[Johan Commelin]

@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]

Johan, you mean outside the is_regular namespace, right?

[Johan Commelin]

@Damiano Testa exactly

[Johan Commelin]

the fully qualified name should be is_unit.is_regular

[Kevin Buzzard]

But I made DVRs and made essentially 0 API

[Kevin Buzzard]

and it just kind of organically grew

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I am just asking them to prove one novel lemma

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

(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]

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]

@Kevin Buzzard does :up: make sense?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

random lemmas created on zulip sometimes get PR'ed.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

but it's still not there

[Kevin Buzzard]

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]

I completely agree with that last remark!

[Kevin Buzzard]

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

[Kevin Buzzard]

and then Damiano can PR regular elements?

[Johan Commelin]

Damiano already did that

[Kevin Buzzard]

nice!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

with flat modules the experiment is over

[Kevin Buzzard]

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

[Johan Commelin]

@Kevin Buzzard #6284

[Damiano Testa]

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]

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)

[Eric Wieser]

Yes, exactly

[Damiano Testa]

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

[Eric Wieser]

And of_left_right is just \<> / is_regular.mk

[Eric Wieser]

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]

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

[Damiano Testa]

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]

Thanks a lot to all!

[Kevin Buzzard]

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]

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]

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

[Damiano Testa]

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]

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]

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]

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]

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]

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]

Aah, it's about the coercion

[Johan Commelin]

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

[Damiano Testa]

Ok, I will keep this version then!

[Damiano Testa]

I just pushed this version!

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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]

Also the symmetric versions are in.