nonsingleton

Stream: maths

[Sebastien Gouezel]

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]

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

[Patrick Massot]

The link should be #3282

[Kevin Buzzard]

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]

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]

superdoubleton

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

tg.png

[Patrick Massot]

No condition at all on norm of 1 then.

[Johan Commelin]

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]

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

[Kevin Buzzard]

I am challenging this notion, that's all

[Patrick Massot]

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

[Johan Commelin]

Aah, ok

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

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]

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

[Patrick Massot]

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

[Patrick Massot]

Kevin think of r = 0

[Patrick Massot]

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

[Sebastien Gouezel]

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]

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

[Gabriel Ebner]

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]

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]

nontrivial? (just half-joking)

[Kevin Buzzard]

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]

That's why I say it's silly.

[Sebastien Gouezel]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

That would mean much more noise than having two classes.

[Gabriel Ebner]

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]

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

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]

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]

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

[Sebastien Gouezel]

Gabriel just beat me to it.

[Patrick Massot]

This is really obfuscation by gratuitous over-engineering.

[Kevin Buzzard]

I thought that was mathlib's motto!

[Patrick Massot]

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

[Kevin Buzzard]

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

[Gabriel Ebner]

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

[Patrick Massot]

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

[Patrick Massot]

No, he posted application of the intermediate idea.

[Patrick Massot]

The one that still mention 0

[Kevin Buzzard]

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

[Patrick Massot]

and would allow to keep the exact same readable name nonzero

[Sebastien Gouezel]

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

[Patrick Massot]

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

[Gabriel Ebner]

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]

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

[Patrick Massot]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Heather Macbeth]

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]

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]

Another vote for nonsubsingleton:

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

And these all have zeros

[Gabriel Ebner]

No, the adjugate_zero example does not have a zero.

[Patrick Massot]

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]

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

[Patrick Massot]

And lunch is calling

[Gabriel Ebner]

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]

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]

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]

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]

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

[Gabriel Ebner]

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

[Johan Commelin]

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]

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

[Johan Commelin]

nonsubsingleton seems to long and obfuscated, to me.

[Jalex Stark]

What about has_ne?

[Johan Commelin]

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]

or subsingleton, singleton, supersingleton :grinning:

[Floris van Doorn]

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.

[Scott Morrison]

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]

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]

For the second you can add lines like

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

[Sebastien Gouezel]

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]

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

[Gabriel Ebner]

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]

ok, done. Thanks!

[Sebastien Gouezel]

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]

@Sebastien Gouezel Thank you so much for doing this!

[Johan Commelin]

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]

Ooh, I see that Gabriel also left some comments.

[Johan Commelin]

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

[Gabriel Ebner]

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

[Johan Commelin]

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