Zulip Chat Archive

Stream: maths

Topic: irreducible top spaces


view this post on Zulip Kevin Buzzard (Jan 29 2020 at 11:46):

What is this? The empty set is irreducible? Whatever next? 1 is prime? Can I change the definition and add that the set is non-empty? I think that this is the standard convention (I just checked in Hartshorne and he has the empty set as not irreducible).

view this post on Zulip Johan Commelin (Jan 29 2020 at 11:56):

The zero ring is a field

view this post on Zulip Johan Commelin (Jan 29 2020 at 11:57):

The empty space is connected: https://github.com/leanprover-community/mathlib/blob/b36831204c0db0c18b35918b56ffd3df55707c9e/src/topology/subset_properties.lean#L512

view this post on Zulip Johan Commelin (Jan 29 2020 at 11:57):

https://ncatlab.org/nlab/show/too+simple+to+be+simple

view this post on Zulip Johan Commelin (Jan 29 2020 at 11:58):

@Kevin Buzzard I think a refactor is in order (-;

view this post on Zulip Mario Carneiro (Jan 29 2020 at 12:29):

adding a nonempty conjunct seems like it would just make proofs ugly. Maybe a rename is in order?

view this post on Zulip Mario Carneiro (Jan 29 2020 at 12:30):

Not a single one of the theorems about irreducible requires the assumption that the the set is nonempty

view this post on Zulip Mario Carneiro (Jan 29 2020 at 12:36):

I don't have much reference for irreducibility, but I am willing to defend the choice of empty set as connected

view this post on Zulip Patrick Massot (Jan 29 2020 at 12:38):

I'm not in favor of complicating definitions if there is no theorem requiring this complication. I would wait to see a theorem where we need assumptions excluding empty or zero.

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 12:48):

In my class we're proving that every Noetherian space is uniquely a union of its irreducible components

view this post on Zulip Mario Carneiro (Jan 29 2020 at 12:52):

I don't think it's a problem, since you have to state what you mean by "component" carefully anyway. If you use a partition (equivalence relation), the empty set doesn't even come up

view this post on Zulip Mario Carneiro (Jan 29 2020 at 12:55):

it looks like the difference between "singleton" and "subsingleton" to me

view this post on Zulip Johan Commelin (Jan 29 2020 at 12:55):

@Mario Carneiro So why do you require that primes are > 1, or that 1 ≠ 0 in fields?

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 12:56):

Maybe there should be subprimes?

view this post on Zulip Johan Commelin (Jan 29 2020 at 12:56):

how about prime' aka prime-prime?

view this post on Zulip Mario Carneiro (Jan 29 2020 at 12:56):

that almost sounds plausible

view this post on Zulip Mario Carneiro (Jan 29 2020 at 12:57):

I've thought about dropping 1 != 0 in domains/fields as well. I don't have a super clear idea on why it's there

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 12:57):

can someone call the moderators?

view this post on Zulip Mario Carneiro (Jan 29 2020 at 12:58):

the fact that inverses in a field explicitly talk about != 0 makes it a bit more natural, but in domains it's out of the blue

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 12:58):

I guess it's all the same answer.

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 12:59):

It's some sort of underlying principle

view this post on Zulip Mario Carneiro (Jan 29 2020 at 13:00):

I'm not a big fan of arguments that point to a classification theorem; that's just one theorem, and it's not even a particularly easy one to use most of the time. I consider it much more important to have the everyday theorems be simple

view this post on Zulip Johan Commelin (Jan 29 2020 at 15:20):

@Mario Carneiro There is a notion of spectral spaces: https://en.wikipedia.org/wiki/Spectral_space
Usually, the empty space is considered to be spectral.
Every spectral space is homeomorphic to Spec(R) for some commutative ring R.
Prime ideals are by definition not allowed to be the entire ring. If we remove this condition, then Spec(R) will never be empty.

view this post on Zulip Johan Commelin (Jan 29 2020 at 15:21):

R/(some prime ideal) is an integral domain.

view this post on Zulip Johan Commelin (Jan 29 2020 at 15:21):

Which connects back to the 1 ≠ 0 issue.

view this post on Zulip Johan Commelin (Jan 29 2020 at 15:22):

Also, Spec(Integral_domain) is irreducible. Which connects back to the irreducibility discussion.

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 15:32):

These are examples of the underlying principle.

view this post on Zulip Johan Commelin (Jan 29 2020 at 15:40):

Yes, and even though we don't really care about spectral spaces yet, in mathlib; I think if you flatten the carpet in one corner, you'll get bumps in another corner.

view this post on Zulip Johan Commelin (Jan 29 2020 at 15:40):

I'm not sure if it's worth the mental reprogramming to deviate from standard maths

view this post on Zulip Johan Commelin (Jan 29 2020 at 15:40):

x/0 and nat.sub are already causing enough headaches.

view this post on Zulip Chris Hughes (Jan 29 2020 at 16:08):

I don't think the maths headaches are ever as big as the Lean headaches, when it comes to very slightly nonstandard definitions.

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 16:09):

I don't think it's a problem, since you have to state what you mean by "component" carefully anyway. If you use a partition (equivalence relation), the empty set doesn't even come up

No. Irreducible components can overlap, they're not like connected components.

view this post on Zulip Reid Barton (Jan 29 2020 at 16:23):

What is this? The empty set is irreducible? Whatever next? 1 is prime? Can I change the definition and add that the set is non-empty? I think that this is the standard convention (I just checked in Hartshorne and he has the empty set as not irreducible).

Yes

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 16:23):

...is the correct answer.

view this post on Zulip Johan Commelin (Jan 29 2020 at 18:49):

I don't think the maths headaches are ever as big as the Lean headaches, when it comes to very slightly nonstandard definitions.

It depends on whether you want non-Lean-using mathematicians to be able to recognise the statements.

I think there is a difference between "maths says it's undefined, but Lean gives some rubbish definition anyways" and "maths says it is defined as X, but Lean says it's defined as X'".
x/0 is an example of the first kind. But changing the definition of irreducible or integral domain etc is an example of the 2nd kind.

view this post on Zulip Chris Hughes (Jan 29 2020 at 19:17):

I think it might be difficult to formalise maths without tidying it up along the way. That's part of the point of formalising it, you learn the correct definitions.

view this post on Zulip Reid Barton (Jan 29 2020 at 20:39):

For me the issue is also about choosing the correct definition, but I put more weight on the definition being used in the 6932 pages of the Stacks project than the approximately 0 uses of irreducible in mathlib.

view this post on Zulip Mario Carneiro (Jan 30 2020 at 01:58):

That's why I said to change the name. This isn't a problem if the mathlib notion isn't called "irreducible"

view this post on Zulip Mario Carneiro (Jan 30 2020 at 01:59):

also that statistic is pretty skewed. You aren't even comparing similar things (number of pages of one thing to number of uses of another)

view this post on Zulip Mario Carneiro (Jan 30 2020 at 02:01):

It is very rare to see choices like this explained in the literature. They just pick something and then you the reader are wondering why it was done that way. They go to great lengths explaining the consequences but many of them apply in other versions of the definition too so you have to do some archaeology to find out why the author chose that convention.

view this post on Zulip Mario Carneiro (Jan 30 2020 at 02:03):

I like to delay such choices until the math itself tells me the answer. After the 5th or 6th consecutive theorem that requires me to talk about nonempty irreducible spaces, I will think "hm, seems like this would be simpler to say if I had a name for this combo". But don't make guesses about this based on what is done in informal math because the details often differ

view this post on Zulip Reid Barton (Jan 30 2020 at 02:32):

I really didn't want to get dragged into a discussion here, but the guy who has written a single coherent 6000-page document summarizing an extremely popular subject that is close to 100 years old is infinitely better placed to make that kind of judgment than you or I ever could be.

view this post on Zulip Reid Barton (Jan 30 2020 at 02:34):

Surely de Jong had some reason to go to the trouble of including the extra words "XX is not empty, and" and it seems foolish to bet that in the formalization, actually, it's better to omit them.

view this post on Zulip Reid Barton (Jan 30 2020 at 02:37):

You are betting against not only the expertise of de Jong but also that of many, many others

view this post on Zulip Mario Carneiro (Jan 30 2020 at 02:39):

Maybe. If that's the case, as I said, the math (written by de Jong) will say it too

view this post on Zulip Mario Carneiro (Jan 30 2020 at 02:40):

But there are a large number of commutative algebra books that make a commutativity assumption that is irrelevant for half of the contained theorems

view this post on Zulip Mario Carneiro (Jan 30 2020 at 02:41):

This kind of thing is done, I think, to delimit the scope of thought and make it clear what the topic is, but this is a non-mathematical justification

view this post on Zulip Mario Carneiro (Jan 30 2020 at 02:44):

In all likelihood, after making it through those 6000 pages I will agree with de Jong's choice. But the refactoring is cheap, and I will be in a much better position to see what actually needs to be done once we get to that point. It's not about disagreement for the sake of it, it's about generating reasons for actions

view this post on Zulip Mario Carneiro (Jan 30 2020 at 02:49):

Keep in mind also that the "trivial" tactic is much more powerful in informal maths. There is no real cost to dealing with trivial cases in informal developments regardless of which way they fall

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 05:52):

I think this is a really interesting thread. I have long worried about this sort of stuff, from way before I got interested in computer formalisation. The first thing I think should be stressed is that, as both Reid and I and probably most of the other mathematicians here know, is that our conventions (trivial ring isn't a field or an ID, univ isn't a prime ideal or a maximal ideal, empty set isn't irreducible, 1 isn't a prime number, trivial group isn't simple...) are all globally coherent and part of a bigger picture which one could regard as a convention. Beyond some point it becomes manifestly clear that our conventions are correct in the sense that they isolate ideas which are central to the more advanced theory, e.g. the spectrum of a commutative ring is the prime ideals and this definition turns out to be of huge importance in mathematics; this observation alone makes it clear that one needs a word for what mathematicians currently call a prime ideal.

Mario is challenging the conventions, which of course is a very healthy thing to do. What I know for sure is that our chosen conventions work and make the "classification theorems" (every positive integer is uniquely the product of primes, every Noetherian topological space is uniquely a union of maximal irreducible subspaces etc) very "clean". Mario complains that classifications are hard to formalise / hard to use, or whatever, but in real life mathematics they are used everywhere; if we let 1 be a prime then we would forever be dealing with special cases, for example, even though I can see that 1 satisfies many of the basic properties of primes developed before the classification theorem (e.g. pab    pap\mid ab\implies p\mid a or pbp\mid b is true for p=1p=1 and indeed this property classifies positive integers which are either prime or 1; and these super-basic results are the kind of things which formalisers find very important because they use them all the time when building their APIs). To give another example, Mario points out that the fundamental results on mathlib-irreducible topological spaces go through very nicely even when the empty set is allowed, although we all know that the classification theorem will fail in the sense that it will have to deal with the empty set as a special case, just like the uniqueness of prime factorization would have to make a special case for factorizations involving 1.

The conclusion I want to draw is that these more primitive notions (e.g. the notion of being 1 or prime, or being mathlib-irreducible) seem to play some important role in formalisation, but ultimately the more subtle notions (the conventions which Reid and I are backing) come to the fore later on. My proposal then is simply to rename current mathlib's irreducible (which includes the empty set) as preirreducible, and then have another section of lemmas for irreducible which is defined to be preirreducible + nonempty.

view this post on Zulip Mario Carneiro (Jan 30 2020 at 06:33):

Mario complains that classifications are hard to formalise / hard to use, or whatever, but in real life mathematics they are used everywhere

To clarify, I mean to say that a classification theorem is a "heavyweight" theorem, so I tolerate a higher number of assumptions and more complex consequences in this case. This is in contrast to theorems like "a finite set is compact" where you really don't want extra side conditions in the way because they are used more frequently.

view this post on Zulip Mario Carneiro (Jan 30 2020 at 06:34):

what I call "rarely used" theorems are "frequently used" in maths, while theorems that are "frequently used" by my definition are used so commonly and implicitly in maths that they aren't mentioned at all

view this post on Zulip Mario Carneiro (Jan 30 2020 at 06:35):

I'm on board with the latter proposal for preirreducible sets

view this post on Zulip Johan Commelin (Jan 30 2020 at 06:51):

So, are we going to have preprime numbers as well?

view this post on Zulip Johan Commelin (Jan 30 2020 at 06:51):

I think this could be fun (-;

view this post on Zulip Mario Carneiro (Jan 30 2020 at 06:51):

If it is useful, sure

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 07:31):

The definition of prime in Lean always struck me as odd, it is a conjunction of two seemingly unrelated statements. On the other hand the concept of prime is clearly the right one. I could imagine seeing up the preliminaries of the theory with preprimes

view this post on Zulip Reid Barton (Jan 30 2020 at 14:36):

It is the same condition, specialized once to n = 0 and once to n = 2. It's just that we write the product of 0 things as 1 and "implies the empty disjunction" as not.

view this post on Zulip Reid Barton (Jan 30 2020 at 14:37):

For n = 1 the condition is a tautology and for n >= 3 it follows from the case n = 2 by induction, so we can omit those.

view this post on Zulip Reid Barton (Jan 30 2020 at 14:38):

It's the same story for integral domains, connected spaces, irreducible spaces, connected graphs etc.

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 15:34):

I only noticed this term that semilattice_sup_botwas precisely what you needed for all finite joins to exist: the two axioms are n=0 and n=2.


Last updated: May 19 2021 at 03:22 UTC