irreducible top spaces

Stream: maths

[Kevin Buzzard]

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

[Johan Commelin]

The zero ring is a field

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Kevin Buzzard]

Maybe there should be subprimes?

[Johan Commelin]

how about prime' aka prime-prime?

[Mario Carneiro]

that almost sounds plausible

[Mario Carneiro]

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

[Kevin Buzzard]

can someone call the moderators?

[Mario Carneiro]

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

[Kevin Buzzard]

I guess it's all the same answer.

[Kevin Buzzard]

It's some sort of underlying principle

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Which connects back to the 1 ≠ 0 issue.

[Johan Commelin]

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

[Kevin Buzzard]

These are examples of the underlying principle.

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Kevin Buzzard]

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.

[Reid Barton]

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

[Kevin Buzzard]

...is the correct answer.

[Johan Commelin]

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.

[Chris Hughes]

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.

[Reid Barton]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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)

[Mario Carneiro]

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.

[Mario Carneiro]

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

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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. $p\mid ab\implies p\mid a$ or $p\mid b$ is true for $p=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.

[Mario Carneiro]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

I think this could be fun (-;

[Mario Carneiro]

If it is useful, sure

[Kevin Buzzard]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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

[Kevin Buzzard]

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.