Finite set

Stream: new members

[Jon Eugster]

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]

ooh here in computer science land we start at 0

[Jon Eugster]

0 to n-1 then :)

[Kevin Buzzard]

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

[Jon Eugster]

thank you!

[Kevin Buzzard]

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]

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]

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

[Jon Eugster]

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]

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]

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

[Kevin Buzzard]

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

[Jon Eugster]

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]

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]

Cool, gonna have a look at that!

[Kevin Buzzard]

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]

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]

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]

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

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

[Johan Commelin]

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

[Jon Eugster]

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

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

[Johan Commelin]

But it would be a natural next step

[Johan Commelin]

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

[Jon Eugster]

Looking forward to see the result.

[Johan Commelin]

Maybe you can do it!! :smiley:

[Kevin Buzzard]

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]

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]

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]

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

[Damiano Testa]

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]

fin n is a linear order.

[Kevin Buzzard]

(at least I hope it is!)

[Johan Commelin]

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

[Yakov Pechersky]

Kevin Buzzard said:

fin n is a linear order.

docs#fin.linear_order

[Kevin Buzzard]

I'm glad that survived the Pechershy purge!

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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]

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

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

[Jon Eugster]

Thank you!

[Jon Eugster]

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]

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

[Johan Commelin]

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

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]

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

[Jon Eugster]

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]

I think I'm wrong, ignore me :)

[Jon Eugster]

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]

Does docs#nat.find help?

[Eric Wieser]

No, that's the infimum

[Eric Wieser]

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]

You can use nat.find

[Johan Commelin]

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

[Damiano Testa]

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]

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]

Anyway, my afternoon of teaching begins!

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

The interesting structure is the filtration by degree <= n

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Damiano Testa]

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.