Stream: maths

Topic: nonsingleton

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.

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)

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.

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.

Kevin Buzzard (Jul 04 2020 at 09:34):

superdoubleton

Patrick Massot (Jul 04 2020 at 09:34):

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

Kevin Buzzard (Jul 04 2020 at 09:34):

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

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.

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.

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

Kevin Buzzard (Jul 04 2020 at 09:41):

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

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

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.

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

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.

Kevin Buzzard (Jul 04 2020 at 09:53):

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

tg.png

Patrick Massot (Jul 04 2020 at 09:55):

No condition at all on norm of 1 then.

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"

Johan Commelin (Jul 04 2020 at 09:56):

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

Kevin Buzzard (Jul 04 2020 at 09:57):

I am challenging this notion, that's all

Patrick Massot (Jul 04 2020 at 09:57):

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

Aah, ok

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

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!

Kevin Buzzard (Jul 04 2020 at 10:00):

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

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.

Kevin Buzzard (Jul 04 2020 at 10:01):

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

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?

Patrick Massot (Jul 04 2020 at 10:02):

Kevin think of r = 0

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.

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.

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.

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.

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.

Sebastien Gouezel (Jul 04 2020 at 10:06):

nontrivial? (just half-joking)

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.

Patrick Massot (Jul 04 2020 at 10:06):

That's why I say it's silly.

Sebastien Gouezel (Jul 04 2020 at 10:07):

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

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.

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.

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

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 $1 \neq 0$ and then keep invoking this lemma in all proofs that currently used the existing nonzero class?

Patrick Massot (Jul 04 2020 at 10:10):

That would mean much more noise than having two classes.

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.

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, $0\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 $0\not=1$ (which is the thing which is actually used).

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.

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.

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 $0 \ne 1$.

Sebastien Gouezel (Jul 04 2020 at 10:15):

Gabriel just beat me to it.

Patrick Massot (Jul 04 2020 at 10:16):

This is really obfuscation by gratuitous over-engineering.

Kevin Buzzard (Jul 04 2020 at 10:16):

I thought that was mathlib's motto!

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.

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"

Gabriel Ebner (Jul 04 2020 at 10:17):

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

Patrick Massot (Jul 04 2020 at 10:17):

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

Patrick Massot (Jul 04 2020 at 10:17):

No, he posted application of the intermediate idea.

Patrick Massot (Jul 04 2020 at 10:17):

The one that still mention 0

Kevin Buzzard (Jul 04 2020 at 10:18):

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

Patrick Massot (Jul 04 2020 at 10:18):

and would allow to keep the exact same readable name nonzero

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.

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.

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.

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.

Patrick Massot (Jul 04 2020 at 10:19):

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

Sebastien Gouezel (Jul 04 2020 at 10:20):

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

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.

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!

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 :=


Gabriel Ebner (Jul 04 2020 at 10:57):

Another vote for nonsubsingleton:

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


Mario Carneiro (Jul 04 2020 at 11:01):

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

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

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

Kevin Buzzard (Jul 04 2020 at 11:11):

And these all have zeros

Gabriel Ebner (Jul 04 2020 at 11:13):

No, the adjugate_zero example does not have a zero.

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.

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)

Patrick Massot (Jul 04 2020 at 11:26):

And lunch is calling

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).

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).

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 α].

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!

Jasmin Blanchette (Jul 04 2020 at 14:13):

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

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.

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''.

Johan Commelin (Jul 04 2020 at 14:56):

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

Johan Commelin (Jul 04 2020 at 14:57):

nonsubsingleton seems to long and obfuscated, to me.

Jalex Stark (Jul 04 2020 at 15:50):

What about has_ne?

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:

Kyle Miller (Jul 04 2020 at 21:46):

or subsingleton, singleton, supersingleton :grinning:

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.

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.

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?

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. -/


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.

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.

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.

Sebastien Gouezel (Jul 06 2020 at 11:39):

ok, done. Thanks!

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...

Johan Commelin (Jul 06 2020 at 12:08):

@Sebastien Gouezel Thank you so much for doing this!

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.)

Johan Commelin (Jul 06 2020 at 12:10):

Ooh, I see that Gabriel also left some comments.

Johan Commelin (Jul 06 2020 at 12:56):

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

Gabriel Ebner (Jul 06 2020 at 12:56):

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

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