## Stream: new members

### Topic: Finite set

#### Jon Eugster (Feb 17 2021 at 16:55):

I'm sorry for the trivial question but how do I get the finite set $\{1, \ldots, n\}$, and where would I look such basic stuff up myself?

#### Kevin Buzzard (Feb 17 2021 at 16:57):

ooh here in computer science land we start at 0

0 to n-1 then :)

#### Kevin Buzzard (Feb 17 2021 at 16:58):

There is finset.range n which is the "finset" $\{0,1,2,\ldots,n-1\}$.

thank you!

#### Kevin Buzzard (Feb 17 2021 at 16:59):

Just to be clear, there are several ways of talking about finite subsets of types, and furthermore you might not actually want a subset at all. Do you just want an abstract type {0,1,2,...,n-1} because we have one of those too, it's called fin n.

#### Kevin Buzzard (Feb 17 2021 at 17:00):

If by "set" you mean "subset of something" (e.g. of the naturals) then you want a set or a finset but if you just want some convenient set with n elements and by set you mean "set in the sense of ZFC, i.e. something with no actual definition but just a collection of stuff" then here in dependent type theory land we suggest that instead you use a type, which is also a collection of stuff with no actual definition.

#### Kevin Buzzard (Feb 17 2021 at 17:01):

PS What is your background and what are you thinking about doing?

#### Jon Eugster (Feb 17 2021 at 17:02):

I want to define a chain of ideals, and my best guess is to define it as a map from {0, ..., n-1} to the set of all ideals and then put some conditions for each pair (i, i+1)

#### Kevin Buzzard (Feb 17 2021 at 17:02):

if you want a chain of ideals of length n then probably the best way to do this in Lean is a map fin n -> ideal R plus some hypotheses.

#### Kevin Buzzard (Feb 17 2021 at 17:03):

except that I can never remember whether that is a chain of length n or n+1 or n-1 :-)

#### Kevin Buzzard (Feb 17 2021 at 17:03):

What I know for sure is that fin n has size n.

#### Jon Eugster (Feb 17 2021 at 17:04):

Thank you fin n looks like a good idea!

PS: Im a PhD in math in Edinburgh and I'm just playing around with Lean, so at the moment I'm looking at regular rings

#### Kevin Buzzard (Feb 17 2021 at 17:04):

I think @Damiano Testa PR'ed regular sequences a day or so ago -- was it you that mentioned them before? You inspired him :-)

#### Jon Eugster (Feb 17 2021 at 17:06):

Cool, gonna have a look at that!

#### Kevin Buzzard (Feb 17 2021 at 17:07):

It's here: #6282 . Right now people are debating implementation-specific minutae about how best to say "multiplication by c is injective". Definitions need a lot of thought. Once they're in place, the fun part, namely proving theorems, can begin.

#### Jon Eugster (Feb 17 2021 at 17:14):

Not sure if this is the same "regular" This looks like left-/right-cancellation to me, I was thinking of the regular in the sense of a regular scheme (in the sense of dim. of cotangent space equals Krull dimension). They are unrelated, aren't they?

#### Jon Eugster (Feb 17 2021 at 17:18):

But fin n is great, just realised that this is defined as a set-comprehension {i : ℕ // i < n}, seems useful. Thank you @Kevin Buzzard

#### Johan Commelin (Feb 17 2021 at 17:28):

@Jon Eugster from Wiki:

More generally, let R be a regular local ring with maximal ideal m. Then any elements r1, ..., rd of m which map to a basis for m/m2 as an R/m-vector space form a regular sequence.

#### Yakov Pechersky (Feb 17 2021 at 17:28):

More precisely, it is a subtype because of a //. A set comprehension would be: {i : ℕ | i < n}

#### Johan Commelin (Feb 17 2021 at 17:28):

https://en.wikipedia.org/wiki/Regular_sequence

#### Jon Eugster (Feb 17 2021 at 17:36):

@Johan Commelin Oh I have to learn how to read github PRs, I only saw about 5 lines of code (defining left/right cancellation) instead of the entire thing, my bad!

@Yakov Pechersky Thank you for the terminology!

#### Johan Commelin (Feb 17 2021 at 17:40):

Well, to be fair, that PR doesn't do regular sequences yet.

#### Johan Commelin (Feb 17 2021 at 17:41):

But it would be a natural next step

#### Johan Commelin (Feb 17 2021 at 17:41):

Have the definition of a regular local ring has been on my mental todo list for a long time

#### Jon Eugster (Feb 17 2021 at 17:46):

Looking forward to see the result.

#### Johan Commelin (Feb 17 2021 at 17:47):

Maybe you can do it!! :smiley:

#### Kevin Buzzard (Feb 17 2021 at 17:48):

The question is: what should the definition of a regular ring or regular local ring be? There are perhaps 5 equivalent definitions of regular local ring, and one question is which one to use as our "official" definition.

#### Kevin Buzzard (Feb 17 2021 at 17:49):

Then one has to think carefully about what theorems to prove about that definition, and get them all in the right order. They say that the Bourbaki books were all written in this way, with things constantly being re-arranged etc and read and re-read until everyone was happy.

#### Johan Commelin (Feb 17 2021 at 17:51):

I guess the first step is https://en.wikipedia.org/wiki/Krull%27s_principal_ideal_theorem which doesn't require much in terms of definitions.

#### Johan Commelin (Feb 17 2021 at 17:57):

Well... I guess we need an API around the Krull dimension

#### Damiano Testa (Feb 17 2021 at 18:25):

Would it be reasonable to define chains of ideals as (strict_)monos from a (linear) order to the lattice of (prime) ideals? This might save some typing on the conditions... Maybe?

#### Kevin Buzzard (Feb 17 2021 at 18:38):

fin n is a linear order.

#### Kevin Buzzard (Feb 17 2021 at 18:38):

(at least I hope it is!)

#### Johan Commelin (Feb 17 2021 at 18:42):

@Damiano Testa It should somehow be a discrete linear order, right? You want to have a notion of the "next" element.

#### Yakov Pechersky (Feb 17 2021 at 18:44):

Kevin Buzzard said:

fin n is a linear order.

docs#fin.linear_order

#### Kevin Buzzard (Feb 17 2021 at 18:44):

I'm glad that survived the Pechershy purge!

#### Damiano Testa (Feb 17 2021 at 18:47):

I really had in mind using it for finite types, but I thought that there could be a general notion of a chain indexed by a general order of some sort and then lots of results about chains based on finite linear orders.

#### Jeremy Avigad (Feb 17 2021 at 18:47):

By the way, Lean provides a nice way of avoiding "off by 1" errors. Suppose you have a sequence of elements a : fin (n + 1) -> X, which you think of as a sequence a_0, a_1, ..., a_n. If you want to say that each one is related to the next, you say forall i : fin n, R (a i.cast_succ) (a i.succ). The library has a nice API for viewing an element i : fin n as an element of fin (n + 1).

#### Damiano Testa (Feb 17 2021 at 18:47):

A lot of the trivial results will likely only look at two comparable elements of the chain anyways...

#### Damiano Testa (Feb 17 2021 at 18:48):

Also, Kevin, my way of remembering what is the "right" index is that you are always interested in counting inclusions rather than ideals.

#### Jon Eugster (Feb 18 2021 at 11:59):

-- Lifting the partial order of ideals to a partial order on prime ideals.
instance has_le_prime_spec {A: Type*} [comm_ring A]: has_le (prime_spectrum A) :=
⟨λp q, p.val ≤ q.val⟩
instance has_lt_prime_spec {A: Type*} [comm_ring A]: has_lt (prime_spectrum A) :=
⟨λp q, p.val < q.val⟩

-- A finite chain of ideal has n+1 ideals I₀ ⊆ ... ⊆ Iₙ
structure increasing_ideal_chain (A: Type*) [comm_ring A] (n:ℕ) :=
(chain: fin (n+1) → prime_spectrum A)
(incl: ∀(i:fin n), ((chain i.cast_succ) < (chain i.succ)))


I'm still learning syntax and conventions. Could something like this look okay, or do you usually have a different approach than structure?

How would I then either take a supremum of m such that such a chain increasing_ideal_chain A m exists ? (The main thing I don't understand in general is how to build a proposition of the form "there is an element in X", or "the type X is not-empty")

#### Eric Wieser (Feb 18 2021 at 12:09):

there is an element in X

If X is a set, that's X.nonempty, docs#set.nonempty

the type X is not-empty

that's nonempty X, docs#nonempty

Thank you!

#### Jon Eugster (Feb 18 2021 at 12:19):

So could the following be an (equivalent) description of the Krull dimension? (Although probably not the desired definition)

def krull_dim (A: Type*) [comm_ring A] (n:ℕ): Prop :=
(∀ (m:ℕ) (C: increasing_ideal_chain A m), m ≤ n) ∧
(nonempty (increasing_ideal_chain A n))


#### Johan Commelin (Feb 18 2021 at 12:36):

That looks reasonable. But it specifies the Krull dimension as a relation between a ring and a nat.

#### Johan Commelin (Feb 18 2021 at 12:37):

@Jon Eugster I haven't thought about whether that's what we want, or whether it should be a function that returns a nat

#### Johan Commelin (Feb 18 2021 at 12:37):

For example char_p is set up in the same way as your Krull dim. But things like dim for vector spaces return the actual dimension, instead of being a relation.

#### Eric Wieser (Feb 18 2021 at 12:37):

Doesn't that definition mean that if krull_dim A n.succ is true then so is krull_dim A n?

#### Jon Eugster (Feb 18 2021 at 12:38):

I guess that one is more a of properties if n is the Krull dimension... and haven't thought exactly about the logic, very likely @Eric Wieser

#### Eric Wieser (Feb 18 2021 at 12:39):

I think I'm wrong, ignore me :)

#### Jon Eugster (Feb 18 2021 at 12:39):

Can I define a supremum of all m such that there is a chain of length m? Do I need to use cardinals to allow the case where the supremum is infinity?

#### Eric Wieser (Feb 18 2021 at 12:40):

Does docs#nat.find help?

#### Eric Wieser (Feb 18 2021 at 12:41):

No, that's the infimum

#### Eric Wieser (Feb 18 2021 at 12:44):

Does something like this work?

def krull_dim (A: Type*) [comm_ring A] : with_top ℕ :=
⨆ (m : ℕ) (C : increasing_ideal_chain A m), m


or perhaps

def krull_dim (A: Type*) [comm_ring A] : with_top ℕ :=
⨆ (m : ℕ) (C : nonempty \$ increasing_ideal_chain A m), m


#### Johan Commelin (Feb 18 2021 at 13:02):

You can use nat.find

#### Johan Commelin (Feb 18 2021 at 13:03):

To find the smallest n such that there is no chain of that length.

#### Damiano Testa (Feb 18 2021 at 13:10):

Every once in a while, I find myself wanting a "less stringent" condition, such as "this number is an upper bound for the [degree of a polynomial, dimension/codimenson of a variety, cardinality of a finite set]". I think that this applies more frequently in the context of Krull dimension, heights, regular sequences. At the moment, I find it a little awkward to deal with this, but maybe this is just me not being able to use the current APIs...

Still, it seems that this discussion might be a good place where to hopefully plant a seed!

#### Damiano Testa (Feb 18 2021 at 13:12):

For instance, when talking about upper-semicontinuity it is really useful to have a good way of talking about stuff that satisfies an inequality.

#### Damiano Testa (Feb 18 2021 at 13:13):

Anyway, my afternoon of teaching begins!

#### Johan Commelin (Feb 18 2021 at 13:50):

I agree. So maybe we want to have has_krull_dim_le as well as krull_dim

#### Kevin Buzzard (Feb 18 2021 at 13:51):

The concept of the degree of a polynomial being equal to something is in some sense a very unnatural one. What can you say about the set of polynomials in $\R[X]$ with degree equal to $n$? Nothing, it's not closed under anything, it's not a subthing, what it is is the difference between the submodule of polys of degree <= n and the submodule of polys of degree < n.

#### Kevin Buzzard (Feb 18 2021 at 13:53):

It's not true that the product of two polynomials of degrees a and b has degree a+b in general, but it's always true that the product of two polynomials of degrees <= a and <= b has degree <= a+b.

#### Kevin Buzzard (Feb 18 2021 at 13:53):

The interesting structure is the filtration by degree <= n

#### Johan Commelin (Feb 18 2021 at 14:04):

Sure, but the same is not true for Krull dimension...

#### Johan Commelin (Feb 18 2021 at 14:04):

There is a lot of interesting stuff to be said about varieties of dimension $n = 1$, or $n = 2$...

#### Kevin Buzzard (Feb 18 2021 at 20:16):

There's still something funny going on though because the disjoint union of a point and a curve is 1-dimensional

#### Damiano Testa (Feb 18 2021 at 20:32):

I tend to think that Kevin's observation on the degree is a reflection of using polynomials instead homogenous forms: the "loss in degree" is a consequence of "stuff running off to infinity".

The issue with Krull dimension is that it is a sup over all chains, so it is "non-local" and, due to the primality restriction, it is also strange for reducible schemes.

There is the notion of catenary, that addresses these issues somehow.

Last updated: May 14 2021 at 21:11 UTC