## Stream: new members

### Topic: Dependent and non dependent finsupp

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

#### 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?

#### Kevin Buzzard (Aug 12 2020 at 17:18):

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

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

#### Reid Barton (Aug 12 2020 at 17:56):

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

#### 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?

#### Kenny Lau (Aug 12 2020 at 17:57):

this doesn't sound very beautiful to me

Other way around

oh

#### Kenny Lau (Aug 12 2020 at 17:58):

then this would make finsupp computable? :P

#### Reid Barton (Aug 12 2020 at 17:58):

Oh dang, can't have that!

#### Kevin Buzzard (Aug 12 2020 at 18:16):

that would make polynomials worse, right?

#### Kenny Lau (Aug 12 2020 at 18:23):

the implementation shouldn't matter!

#### 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?

#### 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?

#### Andre Knispel (Aug 12 2020 at 20:12):

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

#### Reid Barton (Aug 12 2020 at 20:20):

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

#### Andre Knispel (Aug 12 2020 at 20:22):

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

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

#### 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?

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

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

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

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

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

#### Kevin Buzzard (Aug 12 2020 at 21:40):

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

#### Andre Knispel (Aug 12 2020 at 21:41):

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

#### Kevin Buzzard (Aug 12 2020 at 21:43):

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

#### 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?

#### Andre Knispel (Aug 12 2020 at 21:46):

No, do you have a link to that thread?

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

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

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

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

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

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

#### 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 $\mathbb{P}^1_R$ before but by explicitly glueing two copies of affine 1-space.

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

#### Kenny Lau (Aug 13 2020 at 07:14):

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

#### Kevin Buzzard (Aug 13 2020 at 07:16):

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

#### Kenny Lau (Aug 13 2020 at 07:17):

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

#### Kenny Lau (Aug 13 2020 at 07:17):

but merely isomorphic to one

#### Kevin Buzzard (Aug 13 2020 at 07:17):

Oh yes this is a crucial point.

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

exactly

#### Kenny Lau (Aug 13 2020 at 07:21):

implementation (of the ring) should not matter at all

#### 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?

#### Kenny Lau (Aug 13 2020 at 07:23):

or something mathematically equivalent, yes

#### Kevin Buzzard (Aug 13 2020 at 07:23):

Or instead of nat you can use any add_comm_monoid or something

#### Kenny Lau (Aug 13 2020 at 07:23):

but never equality

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

(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 (Aug 13 2020 at 09:22):

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

#### Kevin Buzzard (Aug 13 2020 at 09:23):

This definition definitely avoids the problems I was worried about

#### Kevin Buzzard (Aug 13 2020 at 09:24):

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

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

#### Kevin Buzzard (Aug 13 2020 at 09:25):

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

#### Kenny Lau (Aug 13 2020 at 09:26):

noncomputable theory
open_locale classical


#### Kevin Buzzard (Aug 13 2020 at 09:26):

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

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

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

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

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

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

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

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

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

#### 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] :=
...(axioms)


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

#### Andre Knispel (Aug 13 2020 at 09:47):

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

#### Reid Barton (Aug 13 2020 at 10:17):

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

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

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

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