Zulip Chat Archive

Stream: maths

Topic: delta rings


view this post on Zulip Johan Commelin (Jul 20 2018 at 12:17):

Fix a prime p.

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:17):

57

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:18):

Consider the following attempt at a definition:

class delta_ring {A : Type*} extends comm_ring A :=
(δ : A  A)
(add_prop :  {a b}, δ (a + b) = δ(a)^p + δ(b)^p + (a^p + b^p - (a+b)^p)/p)

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:18):

How should one explain to Lean that (a^p + b^p - (a+b)^p)/p in fact makes sense?

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:18):

must that expression have a unique value?

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:18):

yes

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:19):

you can define a function that spits out that value?

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:19):

Yes, you can. But doesn't that make the definition extremely convoluted?

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:19):

delta_ring.aux : A \to A \to prime \to A

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:21):

And I guess Lean gets happier if I give an explicit definition? Instead of just claiming that the value exists because certain binomial coefficients will always have a factor p?

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:21):

at least I would be happier

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:24):

Here is the full "definition":

class delta_ring {A : Type*} extends comm_ring A :=
(δ : A  A)
(zero_prop : δ(0) = 0)
(one_prop : δ(1) = 0)
(add_prop :  {a b}, δ(a+b) = δ(a)^p + δ(b)^p + (a^p + b^p - (a+b)^p)/p)
(mul_prop :  {a b}, δ(a*b) = a^p*δ(b) + b^p*δ(a) + p*δ(a)*δ(b))

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:25):

would you say that including ^ make the definition more convoluted?

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:26):

What do you mean?

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:26):

Ok, I see what you are getting at...

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:26):

^ is also an auxiliary function that doesn't follow from the ring axioms

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:26):

Well, as a mathematician, I am used to the notation ^, but not to the function delta_ring.aux.

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:27):

that's an arbitrary distinction

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:27):

By that logic every definition in maths is arbitrary.

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:28):

alright

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:29):

Anyway, do you think it is easy to define aux constructively?

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:29):

I think the function ((a+b)^p-a^p-b^p)/p might be useful more generally

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:30):

hmm, let me think about that

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:30):

I guess I first need to prove that binom p i is divisible by p for 0 < i < p.

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:31):

can we somehow extend that definition to all natural numbers?

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:32):

no, p has to be prime (if you are working over an arbitrary ring)

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:32):

Kenny didn't you already write this function somehow?

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:33):

I think Chris did some binomial / factorial things

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:33):

f(a,b,2) = ab
f(a,b,3) = aab+abb
f(a,b,5) = aaaab+2aaabb+2aabbb+abbbb
f(a,b,7) = aaaaaab+3aaaaabb+5aaaabbb+5aaabbbb+3aabbbbb+abbbbbb

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:33):

there's nothing that can go between the lines?

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:33):

hmm

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:33):

no

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:33):

what does a mathematician think about this function?

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:34):

If Chris proved that binom p i * i! * (p-i)! = p! then proving it's a multiple of p is fine as long as you know that if p divides ab then p divides a or b.

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:34):

You then prove that p doesn't divide i! for i<p and you're done

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:34):

I know that "pCa is divisible by p for all a" iff p is a prime

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:34):

i'm asking whether that function can be extended

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:35):

sure it can be extended -- just define it to be 37 for n not prime

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:35):

well

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:37):

I think the GPOV is to define the relevant elements of Z[X,Y] first

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:37):

You're inventing Witt vectors

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:37):

you can do stuff for prime powers somehow

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:37):

indeed

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:38):

Alternatively, Kenny puts Witt vectors into mathlib (-;

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:38):

I mean, we are doing this perfectoid stuff. But the mathematicians are already moving on...

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:38):

The trendy way to do Witt vectors nowadays is to note that if k is a perfect field of char p and R is a k-algebra then the cotangent complex vanishes

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 12:39):

a la Scholze perfectoid spaces paper

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:39):

Nowadays you're only hot if you're doing diamonds or prisms...

view this post on Zulip Patrick Massot (Jul 20 2018 at 12:40):

Let's try perfectoid spaces first...

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:41):

(Kevin, I think the perfectoid project is really cool. So I'm just trying to do some related things to the side, while you are wrapping up Cont et al.)

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:42):

where are the prism emojis when I need them

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:44):

do we have valuations of integers at a prime?

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:44):

I think Alexandria has that

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:45):

Ok, mathlib knows how to raise ring elements to nat-powers, right? Why is this failing?

def Frob {A : Type u} [ring A] (x : A) := x^p

Error:

failed to synthesize type class instance for
_inst_1 : nat.Prime,
A : Type u,
_inst_2 : ring A,
x : A
 has_pow A 

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:45):

did you import the right things?

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:45):

No

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:45):

that's why

view this post on Zulip Johan Commelin (Jul 20 2018 at 12:45):

Hmmm, I want Lean to tell me what to import...

view this post on Zulip Patrick Massot (Jul 20 2018 at 12:45):

Johan, if you don't know what to do for the perfectoid project, you can do

variables (α : Type*) [uniform_space α] (β : Type*) [uniform_space β]

instance complete_space.prod [complete_space α] [complete_space β] : complete_space (α × β) := sorry
instance separated.prod [separated α] [separated β] : separated (α × β) := sorry

which is on my TODO list

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:46):

imports? @Patrick Massot

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:46):

and is that MWE?

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:47):

never mind

view this post on Zulip Patrick Massot (Jul 20 2018 at 12:48):

import analysis.topology.uniform_space

view this post on Zulip Patrick Massot (Jul 20 2018 at 12:48):

and then you get a MWE

view this post on Zulip Kenny Lau (Jul 20 2018 at 12:48):

hmm

view this post on Zulip Patrick Massot (Jul 20 2018 at 12:48):

I'm not saying this is difficult

view this post on Zulip Patrick Massot (Jul 20 2018 at 12:48):

I see Johan is blocked because he waits for Kevin

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 13:02):

I am dealing with universe issues raised by Mario. I have defined an "equivalence class of valuations" on (R : Type u) to be a pre-order on R which is induced from a valuation v : R -> M with M a certain kind of totally ordered monoid, with (M : Type u). I now have to prove that if M had type v then actually there's M' of type u inducing the same pre-order. I dug and dug, and I am now having to define universal properties of quotient groups. But I've screwed up:

https://github.com/kbuzzard/lean-perfectoid-spaces/blob/a0d3bd5de20ed91d2e318914bac742c073b3c4f7/src/for_mathlib/quotient_group.lean#L48

I need to prove that if G is commutative then so is G/N but I think I managed to define multiplication on G in two different ways. I'm spending all day dealing with admin though. If anyone wants to fix up my easy group theory stuff then feel free!

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 13:03):

I will get back to all this this evening hopefully

view this post on Zulip Johan Commelin (Jul 20 2018 at 13:07):

Ok, I started doing this because I was watching Bhargav Bhatt's talk from the Gabber birthday conference.

view this post on Zulip Johan Commelin (Jul 20 2018 at 13:08):

It's quite fun! So far I've got: https://gist.github.com/jcommelin/b09dcc1c3494e123e84afc96a91fd61c

view this post on Zulip Johan Commelin (Jul 20 2018 at 13:09):

Making good use of tactic.ring!

view this post on Zulip Kenny Lau (Jul 20 2018 at 13:10):

theorem wtf (A B : Type) (S : set A) (T : set B) :
  set.prod S T = set.inter (prod.fst ⁻¹' S) (prod.snd ⁻¹' T) := rfl

view this post on Zulip Kenny Lau (Jul 20 2018 at 13:11):

import analysis.topology.uniform_space

variables (α : Type*) [uniform_space α] (β : Type*) [uniform_space β]

instance complete_space.prod [complete_space α] [complete_space β] : complete_space (α × β) :=
{ complete := λ f hf,
    let x1, hx1 := complete_space.complete $ cauchy_map uniform_continuous_fst hf in
    let x2, hx2 := complete_space.complete $ cauchy_map uniform_continuous_snd hf in
    (x1, x2), by rw [nhds_prod_eq, filter.prod_def];
      from filter.le_lift (λ s hs, filter.le_lift' $ λ t ht,
        have H1 : prod.fst ⁻¹' s  f.sets := hx1 hs,
        have H2 : prod.snd ⁻¹' t  f.sets := hx2 ht,
        filter.inter_mem_sets H1 H2) }

view this post on Zulip Kenny Lau (Jul 20 2018 at 13:11):

@Patrick Massot

view this post on Zulip Kenny Lau (Jul 20 2018 at 13:11):

26 minutes

view this post on Zulip Patrick Massot (Jul 20 2018 at 13:14):

Thanks!

view this post on Zulip Johan Commelin (Jul 20 2018 at 14:36):

I still don't really know how to go about defining

def delta_ring.aux {A : Type u} [comm_ring A] : A  A  A := sorry
-- λ a b, (a^p + b^p - (a+b)^p)/p

I know how to do this in maths, but I don't know how to go forward in Lean.

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 14:39):

I'm not saying it's the best way, but one way would be to define the function from fin (p-1) to nat sending i to (p choose i) / p, and then do a finset.sum [I guess you need p as an input for this function].

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 14:40):

Presumably at some point though you'll need that p times your function is what you want it to be, and there you'll need the binomial theorem, which @Chris Hughes has done I believe. Looking at what he did might help.

view this post on Zulip Johan Commelin (Jul 20 2018 at 14:41):

Ok, I already have that property stated (and sorried). So I'm able to prove properties of delta rings already (-;

view this post on Zulip Johan Commelin (Jul 20 2018 at 14:41):

I'll take a look at what Chris did.

view this post on Zulip Chris Hughes (Jul 20 2018 at 15:29):

Presumably at some point though you'll need that p times your function is what you want it to be, and there you'll need the binomial theorem, which @Chris Hughes has done I believe. Looking at what he did might help.

I can PR it, but I'm not sure whether to call it binomial or add_pow.

view this post on Zulip Johan Commelin (Jul 20 2018 at 16:34):

I wouldn't mind if well-known theorems with well-known names preserve their well-known names.

view this post on Zulip Johan Commelin (Jul 20 2018 at 16:34):

To me it would increase readability of proofs

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:36):

How do you feel about a random German in 1992 deciding to call his seminorms valuations even though they are seminorms, and now we have this annoying problem that our definition of valuation in the perfectoid project is both standard and non-standard simultaneously? :-/

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:36):

If someone told me that we were going to ditch that stupid bracket notation for quadratic residues, I would crack open the champagne.

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:37):

Oh -- wait -- for binomial we can just call it both

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:37):

that's what they do with left_distrib, right? That's the formally correct historical name, but add_mul (or mul_add, which ever one left distrib is) is a modern sensible name.

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:38):

Chris -- do you prove that binomial(a,b)*b!*(a-b)!=a!?

view this post on Zulip Kenny Lau (Jul 20 2018 at 16:39):

do we have valuation of an integer over a prime?

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:39):

It's list.count p (factor n) Kenny

view this post on Zulip Johan Commelin (Jul 20 2018 at 16:39):

Kevin, it is choose(a,b), I think. So we can call the binomial theorem binomial, if we want...

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:41):

factors n sorry

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:41):

https://github.com/leanprover/mathlib/blob/master/data/nat/prime.lean

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:42):

lines 226 and 236 show that that's a list of the primes dividing n with multiplicity

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 16:47):

https://github.com/dorhinj/leanstuff/blob/3dbf2626138fa7d4ae8ba6d55529713e2d5acd3a/choose.lean#L55 -- there's the factorial fact

view this post on Zulip Chris Hughes (Jul 20 2018 at 17:28):

https://github.com/dorhinj/leanstuff/blob/3dbf2626138fa7d4ae8ba6d55529713e2d5acd3a/choose.lean#L55 -- there's the factorial fact

@Kevin Buzzard It's also here https://github.com/leanprover/mathlib/blob/master/data/nat/choose.lean

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 17:44):

I couldn't find the binomial theorem though

view this post on Zulip Chris Hughes (Jul 20 2018 at 17:44):

I haven't PRed it yet.

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 17:44):

I mean I couldn't find it in your github repo

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:21):

Question: Why is (a^p + b^p - (a+b)^p)/p uniquely defined? Is division by p always uniquely defined (when applied to multiples of p)? Seems like if the ring has characteristic p this will be a problem...

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:25):

it isn't uniquely defined, but there's a canonical choice

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:26):

It's good old informal mathematicians again, meaning "do it in Q, note the answer is in Z, now map it into any ring"

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:37):

it isn't uniquely defined, but there's a canonical choice

Did you just use the word 'choice'?

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:39):

I just realised that I think Witt vectors and Hensel's lemma are two very nice (and manageable, I hope) companions to the perfectoid project. They aren't logically necessary, but I think they might be really helpful if one wants to do some examples...

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:40):

yeah, I chose the word "choice"

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:40):

I think it's a shame that you have to write it this roundabout way, since it loses the clarity

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:41):

Another way to say what you are trying to say is to form x^p + y^p - (x+y)^p as a multivariate polynomial in Z[x,y], divide by p, and evaluate it at a,b

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:42):

Yes, I completely agree. But I don't know yet how to convince Lean that I can divide that polynomial by p

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:42):

As a polynomial in Z[x,y], you can use int.div on the coefficients

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:43):

Aah, and that is always defined, although it sometimes outputs 57. Is that right?

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:43):

Or probably the floor of x / y.

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:43):

yes that

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:43):

Ok, so then the definition is not hard.

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:43):

Another way to say what you are trying to say is to form x^p + y^p - (x+y)^p as a multivariate polynomial, divide by p, and evaluate it at a,b

This is just some standard polynomial which shows up in some graduate commutative algebra thing, so mathematicians abuse notation. It means exactly what you said yes. The polynomials even have names -- they're in Z[x,y] but then they get coerced into R[x,y] for any comm_ring R

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:44):

by GPOV

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:45):

So then I only need to prove the property that p * aux_poly = x^p + y^p - (x+y)^p

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:45):

And that requires the binomial theorem

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:45):

aux_poly x y p

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:45):

you're going to need the binomial theorem at some point

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:45):

sure

view this post on Zulip Chris Hughes (Jul 20 2018 at 18:46):

It's in your stack project @Kevin Buzzard

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:46):

I didn't think to look there

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:46):

I don't think you actually need the binomial theorem for this, but you mathematicians like your hammers

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:46):

Why not?

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:46):

It's an easy proof by induction

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:46):

if you define aux_poly to be the explicit (choose p i) / p etc etc then it's the same as the binomial theorem

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:47):

it isn't because you can't fill in the gap that p causes

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:47):

forget that

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:47):

you can't extend the definition of aux_poly to all nat

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:47):

you can, he just did that... but you get nonsense

view this post on Zulip Patrick Massot (Jul 20 2018 at 18:49):

I'm trying to figure out what GPOV stand for (I mean understand the acronym, I understand the maths). Google is not very helpful

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:50):

@Kevin Buzzard I just realised that trying to convert arithmetic geometers and/or number theorists to Lean is going to be futile. They start every talk with "For me all rings are commutative." If they can't do that at the top of their Lean files, and they really have to type comm_ring instead of ring all the time, they will drop out immediately...

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:50):

@Patrick Massot General Point Of View?

view this post on Zulip Johan Commelin (Jul 20 2018 at 18:50):

There is also nPOV = n-categorical POV

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:50):

Grothendieck's point of view

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:52):

you could always fork mathlib

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:52):

comm_ring is in core

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:52):

oh crap

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:52):

comm_ring -> ring

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:52):

ring -> non_comm_ring

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:53):

that's what it should be

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:53):

local notation `ring` := comm_ring should work

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:53):

and then local notation `non_comm_ring` := ring?

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:54):

do you actually care about that?

view this post on Zulip Kevin Buzzard (Jul 20 2018 at 18:54):

I will grudgingly confess to occasionally using the ring of 2 x 2 matrices

view this post on Zulip Kenny Lau (Jul 20 2018 at 18:55):

@Kevin Buzzard you're lucky all rings have unity

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:55):

maybe don't use stupid overrides in that file

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:56):

also, overriding the notation for ring doesn't prevent you from using matrix rings

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:56):

of course typeclass inference doesn't care about your notation

view this post on Zulip Mario Carneiro (Jul 20 2018 at 18:58):

Now I am picturing some mathematician starting their talk with "in this lecture, all rings are commutative" and proceed to do amazing things by commuting matrices that don't commute

view this post on Zulip Johan Commelin (Jul 20 2018 at 19:35):

of course typeclass inference doesn't care about your notation

It doesn't? I don't know if I am happy or sad about that...

view this post on Zulip Mario Carneiro (Jul 20 2018 at 19:46):

well the alternative is the "commutative by fiat" lecture scenario I mentioned

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:05):

Ok, so now I want to define the aux_poly in two variables. What would be the best way to do that? I currently have

section delta_ring_aux_poly

open mv_polynomial

def delta_ring.aux_poly1 : mv_polynomial (fin 2)  :=
begin
  let X0 : mv_polynomial (fin 2)  := X 0, nat.zero_lt_succ 1,
  let X1 : mv_polynomial (fin 2)  := X 1, nat.le_refl 2,
  exact (X0^p + X1^p - (X0+X1)^p),
end

def delta_ring.aux_poly2 : mv_polynomial (fin 2)  :=
finsupp.map_range (λ n:, n/p) (int.zero_div p) delta_ring.aux_poly1

end delta_ring_aux_poly

def delta_ring.aux {A : Type u} [comm_ring A] : A  A  A :=
(mv_polynomial.functorial int.cast delta_ring.aux_poly2).eval 
(λ a b,
begin
  intro i,
end
 : A  A  ((fin 2)  A))
--  sorry
-- λ a b, (a^p + b^p - (a+b)^p)/p

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:06):

It it better to use choose here, and explicitly define it as some finset.sum?

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:06):

I don't really like the finsupp.map_range, but that is just my gut feeling.

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:09):

This looks like a pretty faithful rendition of my suggestion

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:09):

the last bit looks incomplete though

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:10):

It is.

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:10):

I don't know how to define functions out of fin n. Do we have to use if-then-else for that?

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:11):

there should be a fin.cons function

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:11):

you can also use a match block

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:11):

there is fin.cases

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:13):

Probably it is easier to use bool rather than fin 2 here

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:15):

Aah, that is a nice suggestion

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:15):

I'll try that

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:15):

You can use cond to case on bool

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:17):

Hmm, what exactly do you mean with that?

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:18):

Aah

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:18):

So cond is in fact my function. I want to look at cond i a b

view this post on Zulip Mario Carneiro (Jul 23 2018 at 08:19):

yes

view this post on Zulip Johan Commelin (Jul 23 2018 at 08:39):

@Chris Hughes Are you planning on PR-ing your binomial theorem sometime soon?

view this post on Zulip Johan Commelin (Jul 23 2018 at 12:08):

So, now I need to sum over fin n. Hooray! I don't even know how to deal with the case n = 1:

import data.finsupp

example (p : ) (hp : p = 57) : finset.sum finset.univ (λ (x : fin (0 + 1)), finsupp.single (finsupp.single (x.val) 1) (p ^ x.val)) =
    finsupp.single (finsupp.single 0 1) 1 := sorry

view this post on Zulip Johan Commelin (Jul 23 2018 at 12:08):

I would like to tell Lean that finset.univ is singleton 0 in this case.

view this post on Zulip Johan Commelin (Jul 23 2018 at 12:08):

But I don't know how to do that.

view this post on Zulip Johan Commelin (Jul 23 2018 at 12:08):

(Technically singleton \<0,_\>...)

view this post on Zulip Kenny Lau (Jul 23 2018 at 12:23):

import data.finsupp

example (p : ) (hp : p = 57) : finset.sum finset.univ (λ (x : fin (0 + 1)), finsupp.single (finsupp.single (x.val) 1) (p ^ x.val)) =
    finsupp.single (finsupp.single 0 1) 1 :=
have H1 : (finset.univ : finset $ fin 1) = finset.singleton 0,
  from finset.ext' $ λ x, hx, begin
    cases hx with hx hx1,
    { simp, refl },
    cases hx1
  end,
by rw [H1, finset.sum_singleton]; refl

view this post on Zulip Johan Commelin (Jul 23 2018 at 12:25):

You were able to convince Lean that you get a singleton! I couldn't even get it to typecheck the type of H1.

view this post on Zulip Johan Commelin (Jul 23 2018 at 17:25):

@Chris Hughes Are you planning on PR-ing your binomial theorem sometime soon?

Thanks! :clap: :octopus:


Last updated: May 14 2021 at 20:13 UTC