Zulip Chat Archive

Stream: new members

Topic: Dependent and non dependent finsupp


view this post on Zulip Andre Knispel (Aug 12 2020 at 16:08):

I need dfinsupp for graded rings, modules, etc, but polynomial is implemented with finsupp, so to construct the polynomial ring as an example for a graded ring, I need an isomorphism between those in the non dependent case. Is there one somewhere? I've looked for some time but couldn't find anything.

view this post on Zulip Andre Knispel (Aug 12 2020 at 16:11):

I guess this would be trivial if finsupp was implemented using dfinsupp. Is there a reason why this isn't the case?

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 17:18):

@Kenny Lau you sometimes complain about polynomial. How should we fix it?

view this post on Zulip Kenny Lau (Aug 12 2020 at 17:55):

Andre Knispel said:

I guess this would be trivial if finsupp was implemented using dfinsupp. Is there a reason why this isn't the case?

When I wrote dfinsupp I cared about computability so I made sure that everything was computable, and finsupp wasn't computable.

view this post on Zulip Reid Barton (Aug 12 2020 at 17:56):

So what's your opinion now that you no longer care about computability? :upside_down:

view this post on Zulip Kenny Lau (Aug 12 2020 at 17:57):

well if dfinsupp were to be constructed using finsupp then we would need to map it to some sort of wedged disjoint union?

view this post on Zulip Kenny Lau (Aug 12 2020 at 17:57):

this doesn't sound very beautiful to me

view this post on Zulip Reid Barton (Aug 12 2020 at 17:57):

Other way around

view this post on Zulip Kenny Lau (Aug 12 2020 at 17:57):

oh

view this post on Zulip Kenny Lau (Aug 12 2020 at 17:58):

then this would make finsupp computable? :P

view this post on Zulip Reid Barton (Aug 12 2020 at 17:58):

Oh dang, can't have that!

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 18:16):

that would make polynomials worse, right?

view this post on Zulip Kenny Lau (Aug 12 2020 at 18:23):

the implementation shouldn't matter!

view this post on Zulip Andre Knispel (Aug 12 2020 at 19:54):

hm, I guess I'll just redefine the polynomial ring using dfinsupp then for now. Should I open an issue for the larger issue of making these compatible?

view this post on Zulip Reid Barton (Aug 12 2020 at 20:10):

Andre Knispel said:

redefine the polynomial ring using dfinsupp

Could you explain what you mean by this?

view this post on Zulip Andre Knispel (Aug 12 2020 at 20:12):

def polynomial (α : Type*) [comm_semiring α] := Π₀ _ : ℕ, α

view this post on Zulip Reid Barton (Aug 12 2020 at 20:20):

Why would this be necessary to make polynomials an example of a graded ring?

view this post on Zulip Andre Knispel (Aug 12 2020 at 20:22):

it's not necessary, but I need it to be at least isomorphic to this type

view this post on Zulip Andre Knispel (Aug 12 2020 at 20:24):

I've tried to construct this isomorphism and got stuck on some details that I don't really want to mess with, so this seems easier

view this post on Zulip Reid Barton (Aug 12 2020 at 20:24):

Redefining a structure to make it an example of something doesn't seem sustainable--what happens when the next person wants to make it an example of something else?

view this post on Zulip Andre Knispel (Aug 12 2020 at 20:27):

well, what I really want is for finsupp and dfinsupp to be compatible, but that's too much work for me right now. I just want to take the path of least resistance to construct the projective space as a scheme

view this post on Zulip Reid Barton (Aug 12 2020 at 20:44):

I really don't think the path of least resistance can be to redefine polynomial. The API already characterizes it up to isomorphism, so if you manage to avoid breaking all the users then this is tantamount to constructing the isomorphism you are interested in anyways.

view this post on Zulip Andre Knispel (Aug 12 2020 at 20:52):

true, but I don't intend to actually redefine polynomial, just to have an equivalent definition for that single use case.

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:35):

@Andre Knispel I am going to challenge your assertion that you "need" dfinsupp for graded rings, modules etc. What do you mean by this? I can't imagine why I would need any particular implementation to make the specification for graded rings and modules.

view this post on Zulip Andre Knispel (Aug 12 2020 at 21:38):

Well, I need to form a direct sum over a family indexed by a monoid. So I don't necessarily need exactly dfinsupp, but at least something equivalent

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:40):

Aah I see -- you don't have a 0 so you can't use finsupp?

view this post on Zulip Andre Knispel (Aug 12 2020 at 21:41):

No, the modules I'm summing need to depend on the index

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:43):

Oh I see -- I am finally on your wavelength.

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:44):

oh but if you do it this way then you're going to end up in dependent type theory hell aren't you? Did you see the CDGA thread? Maybe you should do some trick with sigma types?

view this post on Zulip Andre Knispel (Aug 12 2020 at 21:46):

No, do you have a link to that thread?

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:46):

PS you know schemes aren't yet in mathlib, right? Somehow people decided to do sheafification using category theory and this has slowed the process up

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:47):

Andre Knispel said:

No, do you have a link to that thread?

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/CDGAs/near/167848869

view this post on Zulip Andre Knispel (Aug 12 2020 at 21:47):

yes, I intend to build on lean-scheme and maybe make a PR when I'm done

view this post on Zulip Andre Knispel (Aug 12 2020 at 21:52):

Thanks! One advantage I see in this simpler case is that there is an actual ring structure to build on top of, so most of the axioms are free

view this post on Zulip Andre Knispel (Aug 12 2020 at 21:55):

I already have definitions for graded rings and homogeneous modules over them that seem to work fine, though I haven't proved anything yet with them

view this post on Zulip Andre Knispel (Aug 12 2020 at 21:56):

maybe I should just construct the functor mapping regular rings to graded rings concentrated in degree 0 for an easier example...

view this post on Zulip Kevin Buzzard (Aug 12 2020 at 21:57):

I think this is a really interesting and worthwhile project. I think that @Kenny Lau tried to construct PR1\mathbb{P}^1_R before but by explicitly glueing two copies of affine 1-space.

view this post on Zulip Andre Knispel (Aug 12 2020 at 22:06):

I looked a little bit at that, but I don't think there is much I can take from there to make it easier for me

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:14):

theoretically you can show that finsupp and dfinsupp are isomorphic by using their universal properties

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:16):

@Kenny Lau how would you set up graded rings and modules?

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:17):

definitely not by requiring that every graded ring / module be a dfinsupp

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:17):

but merely isomorphic to one

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:17):

Oh yes this is a crucial point.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:19):

Because someone will come along with some completely different construction and then in the literature it will say "hence we see R is a graded ring" and it's crucial that it can become an instance of graded_ring

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:20):

exactly

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:21):

implementation (of the ring) should not matter at all

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:22):

So it should be a predicate on a pair consisting of a ring and a map from nat to the subsets of the ring?

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:23):

or something mathematically equivalent, yes

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:23):

Or instead of nat you can use any add_comm_monoid or something

view this post on Zulip Kenny Lau (Aug 13 2020 at 07:23):

but never equality

view this post on Zulip Andre Knispel (Aug 13 2020 at 09:20):

Let me copy my current definition (of graded abelian group) here

variables (α : Type u) (M : Type v)
variables [add_comm_group α] [add_monoid M] [decidable_eq M]

class graded_abelian_group :=
(piece : M  Type u) (group :  m : M, add_comm_group (piece m))
(iso : α + direct_sum M piece)

I don't really see how I would form direct sums with subsets, but this seems to work just fine

view this post on Zulip Andre Knispel (Aug 13 2020 at 09:22):

Using the universal properties to show the isomorphism is a good point, I didn't think about that!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:23):

This definition definitely avoids the problems I was worried about

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:24):

You will have the usual problems with equality but c'est la vie

view this post on Zulip Andre Knispel (Aug 13 2020 at 09:25):

The requirement of decidable equality on M annoys me a little, but I guess that's the price to be paid for computability indfinsupp

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:25):

The advantage of the M -> set alpha approach is that you get a better equality

view this post on Zulip Kenny Lau (Aug 13 2020 at 09:26):

noncomputable theory
open_locale classical

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:26):

If you're doing schemes then you'll have to do this.

view this post on Zulip Andre Knispel (Aug 13 2020 at 09:31):

How much experience do people have with set theoretic vs type theoretic constructions in these contexts? In an ideal world, we could have both, what I did and using subsets instead interchangeably and choose whatever is better right now

view this post on Zulip Andre Knispel (Aug 13 2020 at 09:36):

I imagine I could make another class that uses subsets instead, show that those types are isomorphic, and then redefine graded_abelian_group such that it works with both of those definitions. But I don't know how well this would work in practice

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:37):

When you make classes you're basically making categories, so if you make two classes you're making two categories, and then the dictionary is an equivalence (not an isomorphism) between them.

view this post on Zulip Andre Knispel (Aug 13 2020 at 09:38):

Now I'm thinking that that might not be necessary, I can also just define the subsets from here, and then work with them whenever it's convenient

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:38):

Lean has functional and set extensionality, so if you start with M -> set alpha and then move to the type thing and then back to M, you'll get something which is provably (but not definitionally) equal; the other way you'll get something which is not provably equal.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:39):

But equality is the wrong concept in category theory. This is a shame, because it's an extremely convenient concept to work with, e.g. rw works great.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:42):

The crucial insight we had with localisation (which also had this sort of issue -- the localisation of R at f is one concretely defined ring R[1/f], but unfortunately R[1/f][1/g] is not literally equal to R[1/fg] so one has to work with isomorphisms instead. We still can't transfer ring-theoretic properties along isomorphisms so the trick is to prove things for any ring satisfying the universal property directly.

view this post on Zulip Andre Knispel (Aug 13 2020 at 09:43):

That sounds familiar, I expect that's the same issue as for any explicit constructions with limits

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:45):

I think the set definition is kind of better because it doesn't have this extra Type-valued data piece, and it has better equality properties. I think I'd be tempted to try

class graded_abelian_group (α : Type u) [add_comm_group α] (M : Type v) [add_monoid M] :=
(grading : M  add_subgroup α)
...(axioms)

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 09:46):

But I'm not very good at definitions; @Reid Barton will have an opinion which is worth a lot more weight.

view this post on Zulip Andre Knispel (Aug 13 2020 at 09:47):

I wonder if it makes a difference though, I'm pretty sure I can define grading

view this post on Zulip Reid Barton (Aug 13 2020 at 10:17):

Do we have the notion of an internal direct sum already?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:08):

The difference is simply that the add_subgroup definition has a better-behaved equality. In a category the concept of equality is kind of barely relevant. If you have two unequal but isomorphic objects X and Y in a category and you decide to make them equal then you end up with a quotient category, equivalent to your original category; if the category didn't change up to equivalence then you didn't really change anything. You're suggesting a definition and I'm suggesting a definition where a whole bunch of isomorphic objects become equal. The definitions are equivalent, but equality is easier to work with in Lean than isomorphism, so the more of it you have, the better.

If the answer to Reid's question is "yes" then you should use this.

view this post on Zulip Andre Knispel (Aug 13 2020 at 12:42):

Ah, I got confused, I thought you were talking about equality in the ring, not of graded rings

view this post on Zulip Kenny Lau (Aug 13 2020 at 13:07):

we are talking about type equality, @Andre Knispel , which we do not talk about


Last updated: May 10 2021 at 23:11 UTC