delta rings

Stream: maths

[Johan Commelin]

Fix a prime p.

[Kenny Lau]

57

[Johan Commelin]

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)

[Johan Commelin]

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

[Kenny Lau]

must that expression have a unique value?

[Kenny Lau]

yes

[Kenny Lau]

you can define a function that spits out that value?

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

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?

[Kenny Lau]

at least I would be happier

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

What do you mean?

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

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

[Kenny Lau]

that's an arbitrary distinction

[Johan Commelin]

By that logic every definition in maths is arbitrary.

[Kenny Lau]

alright

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

hmm, let me think about that

[Johan Commelin]

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

[Kenny Lau]

can we somehow extend that definition to all natural numbers?

[Kevin Buzzard]

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

[Kevin Buzzard]

Kenny didn't you already write this function somehow?

[Kevin Buzzard]

I think Chris did some binomial / factorial things

[Kenny Lau]

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

[Kenny Lau]

there's nothing that can go between the lines?

[Kenny Lau]

hmm

[Kevin Buzzard]

no

[Kenny Lau]

what does a mathematician think about this function?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kenny Lau]

i'm asking whether that function can be extended

[Kevin Buzzard]

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

[Kenny Lau]

well

[Kenny Lau]

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

[Kevin Buzzard]

You're inventing Witt vectors

[Kevin Buzzard]

you can do stuff for prime powers somehow

[Kenny Lau]

indeed

[Johan Commelin]

Alternatively, Kenny puts Witt vectors into mathlib (-;

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

a la Scholze perfectoid spaces paper

[Johan Commelin]

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

[Patrick Massot]

Let's try perfectoid spaces first...

[Johan Commelin]

(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.)

[Kenny Lau]

where are the prism emojis when I need them

[Kenny Lau]

do we have valuations of integers at a prime?

[Kenny Lau]

I think Alexandria has that

[Johan Commelin]

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 ℕ

[Kenny Lau]

did you import the right things?

[Johan Commelin]

No

[Kenny Lau]

that's why

[Johan Commelin]

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

[Patrick Massot]

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

[Kenny Lau]

imports? @Patrick Massot

[Kenny Lau]

and is that MWE?

[Kenny Lau]

never mind

[Patrick Massot]

import analysis.topology.uniform_space

[Patrick Massot]

and then you get a MWE

[Kenny Lau]

hmm

[Patrick Massot]

I'm not saying this is difficult

[Patrick Massot]

I see Johan is blocked because he waits for Kevin

[Kevin Buzzard]

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!

[Kevin Buzzard]

I will get back to all this this evening hopefully

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Making good use of tactic.ring!

[Kenny Lau]

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

[Kenny Lau]

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)⟩ }

[Kenny Lau]

@Patrick Massot

[Kenny Lau]

26 minutes

[Patrick Massot]

Thanks!

[Johan Commelin]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Johan Commelin]

I'll take a look at what Chris did.

[Chris Hughes]

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.

[Johan Commelin]

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

[Johan Commelin]

To me it would increase readability of proofs

[Kevin Buzzard]

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? :-/

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kenny Lau]

do we have valuation of an integer over a prime?

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

factors n sorry

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

I couldn't find the binomial theorem though

[Chris Hughes]

I haven't PRed it yet.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

Did you just use the word 'choice'?

[Johan Commelin]

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

[Kenny Lau]

yeah, I chose the word "choice"

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

Or probably the floor of x / y.

[Mario Carneiro]

yes that

[Johan Commelin]

Ok, so then the definition is not hard.

[Kevin Buzzard]

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

[Kenny Lau]

by GPOV

[Johan Commelin]

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

[Johan Commelin]

And that requires the binomial theorem

[Kenny Lau]

aux_poly x y p

[Kevin Buzzard]

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

[Johan Commelin]

sure

[Chris Hughes]

It's in your stack project @Kevin Buzzard

[Kevin Buzzard]

I didn't think to look there

[Mario Carneiro]

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

[Johan Commelin]

Why not?

[Mario Carneiro]

It's an easy proof by induction

[Kevin Buzzard]

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

[Kenny Lau]

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

[Mario Carneiro]

forget that

[Kenny Lau]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

@Patrick Massot General Point Of View?

[Johan Commelin]

There is also nPOV = n-categorical POV

[Kenny Lau]

Grothendieck's point of view

[Kevin Buzzard]

you could always fork mathlib

[Mario Carneiro]

comm_ring is in core

[Kevin Buzzard]

oh crap

[Kevin Buzzard]

comm_ring -> ring

[Kevin Buzzard]

ring -> non_comm_ring

[Kevin Buzzard]

that's what it should be

[Mario Carneiro]

local notation `ring` := comm_ring should work

[Kevin Buzzard]

and then local notation `non_comm_ring` := ring?

[Mario Carneiro]

do you actually care about that?

[Kevin Buzzard]

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

[Kenny Lau]

@Kevin Buzzard you're lucky all rings have unity

[Mario Carneiro]

maybe don't use stupid overrides in that file

[Mario Carneiro]

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

[Mario Carneiro]

of course typeclass inference doesn't care about your notation

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

This looks like a pretty faithful rendition of my suggestion

[Mario Carneiro]

the last bit looks incomplete though

[Johan Commelin]

It is.

[Johan Commelin]

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

[Mario Carneiro]

there should be a fin.cons function

[Mario Carneiro]

you can also use a match block

[Mario Carneiro]

there is fin.cases

[Mario Carneiro]

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

[Johan Commelin]

Aah, that is a nice suggestion

[Johan Commelin]

I'll try that

[Mario Carneiro]

You can use cond to case on bool

[Johan Commelin]

Hmm, what exactly do you mean with that?

[Johan Commelin]

Aah

[Johan Commelin]

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

[Mario Carneiro]

yes

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

But I don't know how to do that.

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

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

[Johan Commelin]

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

Thanks! :clap: :octopus: