Dependent and non dependent finsupp

Stream: new members

[Andre Knispel]

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.

[Andre Knispel]

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

[Kevin Buzzard]

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

[Kenny Lau]

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.

[Reid Barton]

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

[Kenny Lau]

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

[Kenny Lau]

this doesn't sound very beautiful to me

[Reid Barton]

Other way around

[Kenny Lau]

oh

[Kenny Lau]

then this would make finsupp computable? :P

[Reid Barton]

Oh dang, can't have that!

[Kevin Buzzard]

that would make polynomials worse, right?

[Kenny Lau]

the implementation shouldn't matter!

[Andre Knispel]

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?

[Reid Barton]

Andre Knispel said:

redefine the polynomial ring using dfinsupp

Could you explain what you mean by this?

[Andre Knispel]

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

[Reid Barton]

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

[Andre Knispel]

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

[Andre Knispel]

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

[Reid Barton]

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?

[Andre Knispel]

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

[Reid Barton]

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.

[Andre Knispel]

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

[Kevin Buzzard]

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

[Andre Knispel]

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

[Kevin Buzzard]

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

[Andre Knispel]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Andre Knispel]

No, do you have a link to that thread?

[Kevin Buzzard]

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

[Kevin Buzzard]

Andre Knispel said:

No, do you have a link to that thread?

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

[Andre Knispel]

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

[Andre Knispel]

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

[Andre Knispel]

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

[Andre Knispel]

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

[Kevin Buzzard]

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

[Andre Knispel]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

but merely isomorphic to one

[Kevin Buzzard]

Oh yes this is a crucial point.

[Kevin Buzzard]

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

[Kenny Lau]

exactly

[Kenny Lau]

implementation (of the ring) should not matter at all

[Kevin Buzzard]

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

[Kenny Lau]

or something mathematically equivalent, yes

[Kevin Buzzard]

Or instead of nat you can use any add_comm_monoid or something

[Kenny Lau]

but never equality

[Andre Knispel]

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

[Andre Knispel]

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

[Kevin Buzzard]

This definition definitely avoids the problems I was worried about

[Kevin Buzzard]

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

[Andre Knispel]

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

[Kevin Buzzard]

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

[Kenny Lau]

noncomputable theory
open_locale classical

[Kevin Buzzard]

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

[Andre Knispel]

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

[Andre Knispel]

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

[Kevin Buzzard]

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.

[Andre Knispel]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Andre Knispel]

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

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Andre Knispel]

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

[Reid Barton]

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

[Kevin Buzzard]

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.

[Andre Knispel]

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

[Kenny Lau]

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