Zulip Chat Archive

Stream: maths

Topic: nonsingleton


view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 09:23):

In #3283, the need for a typeclass expressing that a vector space is not trivial shows up. 4 possible solutions given by @Yury G. Kudryashov, who also suggests it should be discussed on Zulip:

  • (a) add a typeclass "has at least two elements";
  • (b) use [fact (0 < ...)] and let the user declare a local instance fact ....
  • (a'): modify nonzero to say ∃ x, x ≠ 0 instead of 0 ≠ 1. In a monoid_with_zero this is equivalent to the old typeclass but makes more sense for vector spaces
  • (a'') introduce nonsingleton : ∃ x y, x ≠ y and use it instead of nonzero in algebra/group_with_zero.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 09:24):

For what it's worth, I vote for (a'') (and I'm ready to give it a try if there is a consensus)

view this post on Zulip Patrick Massot (Jul 04 2020 at 09:32):

The link should be #3282

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:33):

nonzero (i.e. containing an element other than 0) is an important concept in ring theory -- for example integral domains and fields are non-zero, in analogy with 1 not being a prime. For rings it's equivalent to 0 \ne 1.

But I am confused why the zero ring isn't a normed algebra. When I was working with p-adic normed algebras I allowed the zero ring.

view this post on Zulip Patrick Massot (Jul 04 2020 at 09:33):

How do you suggest to name the type class in a''? It can't be nonzero, and this will obfuscate all the algebraic applications.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:34):

superdoubleton

view this post on Zulip Patrick Massot (Jul 04 2020 at 09:34):

Do you have other application in minds (where nonzero wouldn't be a good name)?

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:34):

I would like to hear why the idea is important for nonzero vector spaces.

view this post on Zulip Patrick Massot (Jul 04 2020 at 09:35):

Even if you do, I think I still prefer to use a' for algebra and add another type class for the other applications.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:40):

I'm going to suggest that your definition of normed algebra is wrong if it doesn't allow the zero algebra. I've just looked at how I set this up in the p-adic setting. If K is a normed field (the norm is real-valued and |1| = 1) then a normed K-algebra was for me a ring A equipped with a ring homomophism K -> A and a real-valued norm, satisfying |1|<=1, |x| = 0 iff x = 0, |ab|<=|a||b|, and |ka|=|k||a|, and a triangle inequality.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:41):

The axioms imply that either |1|=0 and A=0, or |1|=1 and then the map K->A is injective and the norm on A extends the norm on K

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:41):

In particular it looks like I have gone out of my way to allow A=0

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:42):

I'm pretty sure I didn't invent this stuff myself, I'll dig out a source

view this post on Zulip Patrick Massot (Jul 04 2020 at 09:42):

The question is then: how painful would it be to go this road. Clearly on paper you can just pretend everything holds because the algebra you are currently caring about is obviously non-zero.

view this post on Zulip Patrick Massot (Jul 04 2020 at 09:43):

Google says the answer should be in Théories spectrales: Chapitre 1

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:49):

I've traced my definition back to Bosch-Guenzer-Remmert (written in the 80s), which assumes commutative and nonarchimedean (|a+b|<=max{|a|,|b|}). Maybe things are different in the noncommutative or archimedean (|a+b|<=|a|+|b|) case? But in nonarchimedean geometry it is crucial that zero normed algebras are allowed; we want the empty set to be affinoid and so we need a normed algebra with no maximal ideals.
bgr.png

view this post on Zulip Johan Commelin (Jul 04 2020 at 09:49):

I quite like the semantics of a', but I'm sure that I could get used to a'' as well.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:53):

@Patrick Massot Théories spectrales refers to TG IX p37 def 9 for the definition

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:54):

tg.png

view this post on Zulip Patrick Massot (Jul 04 2020 at 09:55):

No condition at all on norm of 1 then.

view this post on Zulip Johan Commelin (Jul 04 2020 at 09:56):

But we're now mixing two discussions, right? The correct definition of normed algebra is orthogonal to how we want to say "this vector space is non-trivial"

view this post on Zulip Johan Commelin (Jul 04 2020 at 09:56):

And I'm sure that we will want to say "non-trivial" quite often.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:57):

I am challenging this notion, that's all

view this post on Zulip Patrick Massot (Jul 04 2020 at 09:57):

It's not, because this is the only example so far when we need this class.

view this post on Zulip Johan Commelin (Jul 04 2020 at 09:57):

Aah, ok

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 09:57):

We have got this far without having to say non-trivial for anything other than classes with a 0 and a 1

view this post on Zulip Johan Commelin (Jul 04 2020 at 09:58):

I'm going on a hike, I'll see if I can cook up something in the mean time. See you!

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:00):

The reason this is relevant is that it helps us to distinguish between (a) and (a')

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:00):

Having nontrivial vector spaces shows up for many statements. Browsing randomly mathlib, I find

theorem interior_closed_ball' [normed_space  E] (x : E) (r : ) (hE :  z : E, z  0) :
  interior (closed_ball x r) = ball x r

or

/-- If a space is non-trivial, then the norm of the identity equals `1`. -/
lemma norm_id (h :  x : E, x  0) : id 𝕜 E = 1 :=

or

lemma norm_pos (h :  x : E, x  0) : 0 < (e : E L[𝕜] F) :=

So, independently of the application to normed algebras, it is probably a good think to have.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:01):

interior_closed_ball' -- is this not true for the zero space?

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:01):

Good. What about an example where we need to different elements in a type and none of them is 0?

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:02):

Kevin think of r = 0

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:03):

This is a silly version of the lemma, hence the '. But I guess it's still used somewhere.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:03):

I'm fine with a' or a''. With a slight preference for nonsingletonbecause it would apply potentially to non-algebraic situations. I say potentially because I don't have an example at hand, but I can't exclude it would show up some day for someone.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:04):

I say we can still add a class if the need ever arise, and keep readability of what we already have.

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 10:04):

I would also prefer a'' over a', simply because a' is too specific for no good reason. However the name nonsingleton is a bit misleading, as it is not ¬ singleton.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:05):

But stuff like norm_id -- this is a corollary of "|1| = 1 if A is nonzero" (with A=End(E)), but if norm_id is useful then it's evidence that we need the class.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:06):

nontrivial? (just half-joking)

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:06):

Patrick Massot said:

Kevin think of r = 0

Are there any applications of this lemma where r<=0? Isn't r>0 easier to prove than E!=0? But this is secondary.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:06):

That's why I say it's silly.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:07):

Yes, this one is silly, but norm_id is not.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:07):

So the question has become something like: do we want a nonsubsingleton class or just a has-something-other-than-zero [extends has_zero] class.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:08):

And note this lemma is only used once, to prove the silly analogue for frontier, which itself is never used.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:09):

Right. The argument against is that more typeclasses mean more noise, and do we need it? On the other hand this seems like a rarely used typeclass which I guess can't do much harm

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:10):

Even with this semiconservative approach, does it mean we'll need a lemma saying that if a ring is nonzero in this vague sense then 101 \neq 0 and then keep invoking this lemma in all proofs that currently used the existing nonzero class?

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:10):

That would mean much more noise than having two classes.

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 10:11):

Oh wow, I didn't realize we already had a nonzero class. Then I'd vote to just remove the gratuitous has_zero and has_one arguments there.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:13):

@Gabriel Ebner this nonzero class is used a lot in the algebra heirarchy, for rings (and now more generally for monoid_with_zero. In a ring, 010\not=1 is equivalent to the ring being non-zero, which is an important concept in ring theory. Patrick is suggesting that ripping out the nonzero class and replacing it with a more general class just means that then we'll have 1000 applications of the lemma saying that in a non-zero ring we must have 010\not=1 (which is the thing which is actually used).

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:15):

We have

/-- Proves that a semiring that contains at least two distinct elements is nonzero. -/
theorem nonzero.of_ne [semiring α] {x y : α} (h : x  y) : nonzero α :=

but it is only used once. nonzero is used literally hundreds of times in mathlib.

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 10:15):

Right, but the new lemma can be called zero_ne_one and just have different type-class arguments than the current one. This shouldn't break much.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:15):

What about a class nonsubsingleton, an abbreviation nonzero, and a lemma saying that in a ring, nonzero, one has 010 \ne 1.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:15):

Gabriel just beat me to it.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:16):

This is really obfuscation by gratuitous over-engineering.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:16):

I thought that was mathlib's motto!

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:16):

Usually we try to do it only when there are at least one application of the general thing.

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:17):

"Why can't we prove the derivative of x^2 is 2x?" "because we didn't do the Bochner integral yet"

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 10:17):

I think Sébastien posted three applications of the general thing.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:17):

However I need to go, and I don't care so much.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:17):

No, he posted application of the intermediate idea.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:17):

The one that still mention 0

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 10:18):

and I don't know enough about typeclasses to contribute any more

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:18):

and would allow to keep the exact same readable name nonzero

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:18):

I really want to have this for vector spaces, but I don't care to have this in full generality.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:18):

That one is clearly a good idea, and allows to keep lemmas zero_ne_one with the exact same statement.

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 10:19):

I don't care about the name at all. I'm fine with calling it nonzero even though there is no zero anywhere. But having a class for ∃ x, x ≠ 0 is just introducing a dependency on 0 for no reason at all.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:19):

So, here are the two proposals. Please vote here, and I'll try to implement the one that get the most votes.

view this post on Zulip Patrick Massot (Jul 04 2020 at 10:19):

Calling it nonzero without having zero seems a bit confusing to me.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:20):

A class nonzero extending has_zero, and requiring the existence of an element different from 0.

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 10:21):

Or, a class nonsubsingleton, requiring two different elements, and an abbreviation called nonzero and requiring the typeclass has_zero.

view this post on Zulip Heather Macbeth (Jul 04 2020 at 10:37):

Here's a statement I wrote recently (normed_space/hahn_banach), which would benefit from one of the new typeclasses.

theorem exists_dual_vector' (h : 0 < vector_space.dim  E) (x : E) :
   g : E L[] , g = 1  g x = x

On the other hand, I did not use this lemma for anything!

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 10:54):

Another example that does not mention 0 (though the assumption looks suspicious):

@[simp] lemma adjugate_zero (h : 1 < fintype.card n) : adjugate (0 : matrix n n α) = 0 :=

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 10:57):

Another vote for nonsubsingleton:

lemma sign_surjective ( : 1 < fintype.card α) : function.surjective (sign : perm α  units )

view this post on Zulip Mario Carneiro (Jul 04 2020 at 11:01):

I actually prefer the 1 < fintype.card α in that example

view this post on Zulip Mario Carneiro (Jul 04 2020 at 11:03):

also, just because a theorem has this hypothesis doesn't mean it should be inferred by typeclass inference

view this post on Zulip Mario Carneiro (Jul 04 2020 at 11:04):

so far the only one that actually needs it to be a class is the original example with nonzero vector spaces, as well as the various kinds of nonzero rings

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 11:11):

And these all have zeros

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 11:13):

No, the adjugate_zero example does not have a zero.

view this post on Zulip Patrick Massot (Jul 04 2020 at 11:24):

I want to say that, although I still think nonzero makes more sense, I do see that Gabriel seem to find this important. I think that Gabriel (or any other maintainer or very active contributor) can have two votes if he feels strongly about something.

view this post on Zulip Patrick Massot (Jul 04 2020 at 11:25):

(The number 2 or the voting thing shouldn't be taken too literally here, I hope the idea is clear)

view this post on Zulip Patrick Massot (Jul 04 2020 at 11:26):

And lunch is calling

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 11:32):

I'm not asking for extra votes. :smiley: But I'm a bit perplexed that we're adding an unused argument to nonzero here. There is something to be said for requiring both 0 and 1, because we can then get 0 ≠ 1 without any extra assumptions. But all other variants are exactly equivalent to "cardinality greater than 1" (the choice of 0 being completely irrelevant).

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 11:33):

There is also a small technical argument to be made for dropping the unused argument: the terms become smaller, and it make the type-class cache more effective (because otherwise we'd need to do type-class search for the different has_zero instances used).

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 11:35):

I also hope that "extending has_zero" is a typo, and what Sébastien actually meant is class nonzero (α) [has_zero α] : Prop. Otherwise you get two incompatible has_zero instances in [ring α] [nonzero α].

view this post on Zulip Sebastien Gouezel (Jul 04 2020 at 11:50):

Gabriel Ebner said:

I also hope that "extending has_zero" is a typo, and what Sébastien actually meant is class nonzero (α) [has_zero α] : Prop.

Yes, sure!

view this post on Zulip Jasmin Blanchette (Jul 04 2020 at 14:13):

Are people who have trouble installing mathlib allowed to count? Anyway, I'm also against overengineering.

view this post on Zulip Gabriel Ebner (Jul 04 2020 at 14:21):

Ah I'm happy that Jasmin agrees with me, there is really no point in overengineering this by adding extra unused arguments.

view this post on Zulip Johan Commelin (Jul 04 2020 at 14:56):

I'm back from my hike: examples that I came up with are "simple Lie algebra" and "simple representation". In both cases there is a 0 (but not a 1), and really the {0} spaces is "too simple to be simple". Those would be natural candidates for a' or a''.

view this post on Zulip Johan Commelin (Jul 04 2020 at 14:56):

I would be happy with a'' if we can find a reasonable name for it.

view this post on Zulip Johan Commelin (Jul 04 2020 at 14:57):

nonsubsingleton seems to long and obfuscated, to me.

view this post on Zulip Jalex Stark (Jul 04 2020 at 15:50):

What about has_ne?

view this post on Zulip Johan Commelin (Jul 04 2020 at 15:56):

The Walpiri, for example, only has words for “one”, “two”, and “many”

How about subsingleton, unique, and many?

:stuck_out_tongue_wink: :rolling_on_the_floor_laughing:

view this post on Zulip Kyle Miller (Jul 04 2020 at 21:46):

or subsingleton, singleton, supersingleton :grinning:

view this post on Zulip Floris van Doorn (Jul 05 2020 at 00:23):

I feel the basic class should state ∃x y : α, x ≠ y. I think we should call this class already nonzero or nontrivial, and just use this class directly when talking about rings/vector spaces (and then there will be a theorem stating that if you have enough structure (semiring?) zero_ne_one : 0 ≠ 1 assuming this type class.

At some point we'll probably want to use a type class on groups saying that the group is nontrivial, right? It would be nice to use the same class then.

Then again, I don't feel strongly about this.

view this post on Zulip Scott Morrison (Jul 05 2020 at 00:33):

Initially I thought the "x ne y" option was unnecessarily indirect, but I've been convinced by the later suggestions. It seems uniformity comes at little cost, as we can continue using zero_ne_one where we need it.

view this post on Zulip Sebastien Gouezel (Jul 06 2020 at 11:25):

PR at #3296.

I need some help with the linter. With the declarations

class nontrivial (α : Type*) : Prop :=
(exists_pair_ne :  (x y : α), x  y)

structure is_integral_domain (R : Type u) [ring R] extends nontrivial R : Prop :=
(mul_comm :  (x y : R), x * y = y * x)
(eq_zero_or_eq_zero_of_mul_eq_zero :  x y : R, x * y = 0  x = 0  y = 0)

the linter complains

/- The `def_lemma` linter reports: -/
/- INCORRECT DEF/LEMMA: -/
-- algebra/ring.lean
#print is_integral_domain.to_nontrivial /- is a def, should be a lemma/theorem -/

/- The `doc_blame` linter reports: -/
/- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- algebra/ring.lean
#print is_integral_domain.to_nontrivial /- def missing doc string -/

Is there something to be fixed on the linter or Lean side, or should I just silence the linter?

view this post on Zulip Alex J. Best (Jul 06 2020 at 11:30):

For the second you can add lines like

/-- An integral domain as a non-trivial Type. -/
add_decl_doc is_integral_domain.to_nontrivial

view this post on Zulip Sebastien Gouezel (Jul 06 2020 at 11:32):

Sure. The problem is that is shouldn't be a def, so it shouldn't need documentation, but Lean generates a def anyway.

view this post on Zulip Sebastien Gouezel (Jul 06 2020 at 11:33):

And even if it where a def, I don't really see the point in asking for doc in a structure extension.

view this post on Zulip Gabriel Ebner (Jul 06 2020 at 11:35):

This is old_structure_cmd, right? There are some known issues there where the linter doesn't recognize the coercions to the parent. The officially blessed solution is to attribute [nolint] them.

view this post on Zulip Sebastien Gouezel (Jul 06 2020 at 11:39):

ok, done. Thanks!

view this post on Zulip Sebastien Gouezel (Jul 06 2020 at 11:48):

Summary of the PR: I introduced a class nontrivial saying that a type has at least two elements, created a basic API, and used it instead of nonzero everywhere. It went pretty well (most changes were straightforward), although it was a little bit painful since the PR touches 63 files. I imagine this PR could conflict very quickly with everything...

view this post on Zulip Johan Commelin (Jul 06 2020 at 12:08):

@Sebastien Gouezel Thank you so much for doing this!

view this post on Zulip Johan Commelin (Jul 06 2020 at 12:09):

I would be happy with merging this right now. (I left one comments, but it asks for a lemma that can easily be added later without letting this acquire conflicts.)

view this post on Zulip Johan Commelin (Jul 06 2020 at 12:10):

Ooh, I see that Gabriel also left some comments.

view this post on Zulip Johan Commelin (Jul 06 2020 at 12:56):

@Gabriel Ebner Shall we merge this? Or would you rather have your comments dealt with first?

view this post on Zulip Gabriel Ebner (Jul 06 2020 at 12:56):

My comments are not regressions, we/I can fix them in a follow-up PR.

view this post on Zulip Johan Commelin (Jul 06 2020 at 13:04):

Right, I agree. So I've kicked it on the queue.


Last updated: May 19 2021 at 00:40 UTC