ring hom induces ring hom between mv_polynomials

Stream: maths

[Johan Commelin]

I am stuck.

import linear_algebra.multivariate_polynomial

universes u v w

-- ### FOR_MATHLIB
-- everything in this section should move to other files

section ring_hom_commutes_with_stuff

variables {R : Type u} [comm_ring R]
variables {S : Type v} [comm_ring S]
variables (i : R → S) [is_ring_hom i]
variables {X : Type w} [decidable_eq X] (s : finset X) (f : X → R)

open finset

lemma ring_hom_sum : i (sum s f) = sum s (i ∘ f) :=
begin
  apply finset.induction_on s,
  { repeat { rw sum_empty },
    exact is_ring_hom.map_zero i },
  { intros x s' hx ih,
    repeat { rw sum_insert hx },
    rw [is_ring_hom.map_add i, ←ih] }
end

end ring_hom_commutes_with_stuff

namespace mv_polynomial

variables {σ : Type*} [decidable_eq σ]
variables {R : Type u} [decidable_eq R] [comm_ring R]
variables {S : Type v} [decidable_eq S] [comm_ring S]

instance : comm_ring (mv_polynomial σ R) := finsupp.to_comm_ring

instance C_is_ring_hom : is_ring_hom (C : R → mv_polynomial σ R) :=
{ map_one := C_1,
  map_add := λ x y, finsupp.single_add,
  map_mul := λ x y, eq.symm $ C_mul_monomial }

instance functorial_is_ring_hom (i : R → S) [is_ring_hom i] :
is_ring_hom (functorial i : mv_polynomial σ R → mv_polynomial σ S) :=
{ map_one :=
  begin
    simp [functorial],
    simp [finsupp.map_range],
    -- simp [function.comp],
    apply finsupp.ext,
    intro x,
    rw finsupp.on_finset_apply,
    simp [*,finsupp.single_apply],
    sorry
  end,
  map_add :=
  begin
    intros f g,
    simp [functorial,finsupp.map_range,function.comp],
    apply finsupp.ext,
    intro x,
    simp [*,finsupp.single_apply],
    rw is_ring_hom.map_add i,
  end,
  map_mul :=
  begin
    intros f g,
    simp [functorial,finsupp.map_range,function.comp,finsupp.mul_def,finsupp.sum],
    apply finsupp.ext,
    intro x,
    simp [*,finsupp.single_apply],
    rw ring_hom_sum i,
    sorry,
  end }

[Johan Commelin]

There are two sorrys in that bit of code. I don't know how to get rid of them.

[Mario Carneiro]

I think you are going about this the wrong way, at least if you want a clean proof at the end

[Johan Commelin]

Hmmm, so what is the right way?

[Mario Carneiro]

You should break the proof into smaller and more useful parts rather than just attacking the whole thing at once

[Johan Commelin]

Ok, but I think I don't even really see the smaller useful parts...

[Mario Carneiro]

here's the first thing I would prove:

theorem map_monomial (f : α → β) [is_ring_hom f]
  (s : σ →₀ ℕ) (a : α) : map f (monomial s a) = monomial s (f a) :=
sorry

[Mario Carneiro]

(I renamed functorial to map)

[Johan Commelin]

It is still called functorial in mathlib right?

[Mario Carneiro]

not in my local copy as of a minute ago

[Johan Commelin]

Aaah...

[Mario Carneiro]

you can use functorial if it's easier

[Johan Commelin]

theorem map_monomial (i : R → S) [is_ring_hom i]
  (x : σ →₀ ℕ) (r : R) : functorial i (monomial x r) = monomial x (i r) :=
begin
  simp [functorial,finsupp.map_range,function.comp,monomial],
  apply finsupp.ext,
  intro x,
  simp [*,finsupp.single_apply],
  split_ifs,
  { refl },
  { apply is_ring_hom.map_zero }
end

[Mario Carneiro]

I am suspicious still

[Mario Carneiro]

that proof is too complicated

[Johan Commelin]

Hmmm, ok, I'll try to golf it.

[Mario Carneiro]

it should be a one liner about the composition of map_range with single

[Chris Hughes]

Incidentally is @Johannes Hölzl planning on removing the use of monomial for mv_polynomials like he did for univariate polys?

[Mario Carneiro]

I don't know anything about this

[Mario Carneiro]

oh, I see he just uses single

[Chris Hughes]

The idea is to use C a * X^n instead of monomial

[Mario Carneiro]

For foundational stuff that's no good

[Mario Carneiro]

because the theorems about C a and X come from a theorem on single

[Chris Hughes]

Yeah, but once the foundations are done, users are supposed to use C a * X^n I think.

[Mario Carneiro]

sure

[Johan Commelin]

/me seems to be a user who has to do some foundational stuff...

[Mario Carneiro]

Johan Commelin has stumbled on a gap in mathlib

[Johan Commelin]

That's the same thing right?

[Mario Carneiro]

not always

[Johan Commelin]

fair enough

[Mario Carneiro]

well, I guess that depends on what qualifies as "foundational"

[Mario Carneiro]

in this case the API is clearly lacking, and there is even an "unfinished" comment

[Johan Commelin]

Written by?

[Johan Commelin]

Johan Commelin (-;

[Johan Commelin]

So, I can only blame myself

[Mario Carneiro]

https://github.com/leanprover/mathlib/blob/master/linear_algebra/multivariate_polynomial.lean#L183

[Johan Commelin]

But you can guess why I wrote that comment... because back then I would have been even worse at proving this lemma.

[Johan Commelin]

Yeah, the git blame is not accurate.

[Kenny Lau]

I've removed 1 sorry (en hep nok 4 toegevoegt):

[Kenny Lau]

import linear_algebra.multivariate_polynomial

universes u v w u₁

-- ### FOR_MATHLIB
-- everything in this section should move to other files

section ring_hom_commutes_with_stuff

variables {R : Type u} [comm_ring R]
variables {S : Type v} [comm_ring S]
variables (i : R → S) [is_ring_hom i]

section finset

open finset

variables {X : Type w} [decidable_eq X] (s : finset X) (f : X → R)

lemma ring_hom_sum.finset : i (sum s f) = sum s (i ∘ f) :=
begin
  apply finset.induction_on s,
  { repeat { rw sum_empty },
    exact is_ring_hom.map_zero i },
  { intros x s' hx ih,
    repeat { rw sum_insert hx },
    rw [is_ring_hom.map_add i, ←ih] }
end

end finset

section finsupp

open finsupp

variables {α : Type w} {β : Type u₁} [add_comm_monoid β]
variables [decidable_eq α] [decidable_eq β]
variables (f : α → β → R) (s : α →₀ β)
variables (hf1 : ∀ (a : α), f a 0 = 0)
variables (hf2 : ∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂)
include hf1 hf2

lemma ring_hom_sum.finsupp : i (sum s f) = sum s (λ a b, i (f a b)) :=
begin
  apply finsupp.induction s,
  { repeat { rw sum_zero_index },
    exact is_ring_hom.map_zero i },
  { intros a b f' H1 H2 ih,
    repeat { rw sum_add_index },
    repeat { rw sum_single_index },
    rw [is_ring_hom.map_add i, ← ih],
    { rw hf1; exact is_ring_hom.map_zero i },
    { apply hf1 },
    { intros, rw hf1; exact is_ring_hom.map_zero i },
    { intros, rw hf2; exact is_ring_hom.map_add i },
    { apply hf1 },
    { apply hf2 } }
end

end finsupp

end ring_hom_commutes_with_stuff

namespace mv_polynomial

variables {σ : Type*} [decidable_eq σ]
variables {R : Type u} [decidable_eq R] [comm_ring R]
variables {S : Type v} [decidable_eq S] [comm_ring S]

instance : comm_ring (mv_polynomial σ R) := finsupp.to_comm_ring

instance C_is_ring_hom : is_ring_hom (C : R → mv_polynomial σ R) :=
{ map_one := C_1,
  map_add := λ x y, finsupp.single_add,
  map_mul := λ x y, eq.symm $ C_mul_monomial }

instance functorial_is_ring_hom (i : R → S) [is_ring_hom i] :
is_ring_hom (functorial i : mv_polynomial σ R → mv_polynomial σ S) :=
{ map_one :=
  begin
    dsimp [functorial, finsupp.map_range],
    ext x,
    dsimp [finsupp.on_finset_apply],
    have H1 : (1 : mv_polynomial σ R) = (1 : (σ →₀ ℕ) →₀ R) := rfl,
    have H2 : (1 : mv_polynomial σ S) = (1 : (σ →₀ ℕ) →₀ S) := rfl,
    rw [H1, H2, finsupp.one_def, finsupp.one_def, finsupp.single_apply, finsupp.single_apply],
    split_ifs,
    { apply is_ring_hom.map_one i },
    { apply is_ring_hom.map_zero i }
  end,
  map_add :=
  begin
    intros f g,
    dsimp [functorial, finsupp.map_range],
    ext,
    simp [finsupp.single_apply, is_ring_hom.map_add i]
  end,
  map_mul :=
  begin
    intros f g,
    dsimp [functorial, finsupp.map_range],
    ext,
    dsimp [finsupp.on_finset_apply, finsupp.mul_def],
    rw [finsupp.sum_apply, finsupp.sum_apply, ring_hom_sum.finsupp i],
    sorry, sorry, sorry, sorry, sorry
  end }

end mv_polynomial

[Johan Commelin]

I wrote that stuff, but didn't actually know what I was doing. So Johannes took my stuff and transformed it into something mathlib-ready.

[Mario Carneiro]

I didn't realize you were an author of the file, you aren't credited if so

[Mario Carneiro]

I added you as an author

[Johan Commelin]

Does that bring responsibilities with it? Does that mean I should now be able to answer foundational questions about this file?

[Mario Carneiro]

Not really

[Johan Commelin]

By the way... I already had:

lemma functorial_ring_hom_X (i : R → S) [is_ring_hom i] (n : σ)
 : functorial i (X n) = X n :=
begin
  simp [functorial,X,finsupp.map_range,function.comp,C,monomial,*],
  apply finsupp.ext,
  intro x,
  simp [*,finsupp.single_apply],
  split_ifs,
  { apply is_ring_hom.map_one },
  { apply is_ring_hom.map_zero }
end

lemma functorial_ring_hom_C (i : R → S) [is_ring_hom i] (r : R)
: functorial i (C r) = (C (i r) : mv_polynomial σ S) :=
begin
  simp [functorial,X,finsupp.map_range,function.comp,C,monomial,*],
  apply finsupp.ext,
  intro x,
  simp [*,finsupp.single_apply],
  split_ifs,
  { refl },
  { apply is_ring_hom.map_zero }
end

[Johan Commelin]

But I didn't see how to use them.

[Johan Commelin]

But maybe I'm learning, because I think it was pretty close to your suggestion about monomials.

[Mario Carneiro]

almost there:

-- `mv_polynomial σ` is a functor (incomplete)
def map : mv_polynomial σ α → mv_polynomial σ β :=
map_range f (is_ring_hom.map_zero f)

theorem map_monomial (s : σ →₀ ℕ) (a : α) : map f (monomial s a) = monomial s (f a) :=
map_range_single

theorem map_C (f : α → β) [is_ring_hom f] (a : α) : map f (C a : mv_polynomial σ α) = C (f a) :=
map_monomial _ _ _

theorem map_one (f : α → β) [is_ring_hom f] : map f (1 : mv_polynomial σ α) = 1 :=
(map_C _ _).trans $ by simp [is_ring_hom.map_one f]

theorem map_add (f : α → β) [is_ring_hom f] (p q : mv_polynomial σ α) :
  map f (p + q) = map f p + map f q :=
by simp [map]; ext a; simp [is_ring_hom.map_add f]

theorem map_mul (f : α → β) [is_ring_hom f] (p q : mv_polynomial σ α) :
  map f (p * q) = map f p * map f q :=
sorry

[Johan Commelin]

Ok, please add map_X. It will turn out to be really useful.

[Johan Commelin]

/me wonders when he will ever approximate the overlord-powers of Mario... :thinking_face:

[Mario Carneiro]

theorem map_X (f : α → β) [is_ring_hom f] (n : σ) : map f (X n : mv_polynomial σ α) = X n :=
(map_monomial _ _ _).trans $ by simp [is_ring_hom.map_one f]

[Mario Carneiro]

oh wait that doesn't work

theorem map_X (f : α → β) [is_ring_hom f] (n : σ) : map f (X n : mv_polynomial σ α) = X n :=
by simp [X, map_monomial, is_ring_hom.map_one f]

[Johan Commelin]

You fixed it and made it shorter! Double win.

[Mario Carneiro]

mul is probably the hard one

[Johan Commelin]

Last man standing (-;

[Johan Commelin]

@Mario Carneiro I wouldn't be surprised if you need the section ring_hom_commutes_with_stuff

[Johan Commelin]

See Kenny's post a few lines up.

[Mario Carneiro]

I was planning on using induction

[Johan Commelin]

Right, that's what we did in that section.

[Mario Carneiro]

no I mean to prove map_mul

[Johan Commelin]

Yes, but that might mean duplicating effort... I don't know.

[Mario Carneiro]

well, commuting with sum still leaves commuting over ^

[Johan Commelin]

lemma ring_hom_powers (x : R) (n : ℕ) : i(x^n) = (i x)^n :=
begin
  induction n with n ih,
  { simp [pow_zero,is_ring_hom.map_one i] },
  simp [pow_succ,is_ring_hom.map_mul i,ih]
end

[Johan Commelin]

Was already in my file, but didn't copy it into the MWE.

[Mario Carneiro]

I was hoping that map was defined using eval, but unfortunately it's a bit circular

[Johan Commelin]

How would you define it using eval?

[Mario Carneiro]

I was thinking something along the lines of "evaluate the constants using C o f and the variables using X"

[Mario Carneiro]

but eval doesn't work like that; it maps everything into the coefficient ring rather than some other ring across a ring hom

[Johan Commelin]

True. So either you need a beefed up eval, or you need map.

[Mario Carneiro]

exactly

[Johan Commelin]

Oooh, while you are editing that file. I was also thinking that the instance that eval is a ring hom should get a name. Because C is also a useful ring hom in that context.

[Johan Commelin]

instance C_is_ring_hom : is_ring_hom (C : R → mv_polynomial σ R) :=
{ map_one := C_1,
  map_add := λ x y, finsupp.single_add,
  map_mul := λ x y, eq.symm $ C_mul_monomial }

[Mario Carneiro]

I saw that

[Mario Carneiro]

I agree that it is useful

[Johan Commelin]

Yes, I'm currently using map C all over the place.

[Mario Carneiro]

I think I will define beefed up eval, what should it be called?

[Johan Commelin]

Hmm, I don't know a TLA...

[Mario Carneiro]

oh dear, I need semiring homs

[Johan Commelin]

You're kidding me (-;

[Johan Commelin]

You don't need them. You only want them.

[Mario Carneiro]

if I use beefed up eval to define eval, it won't work on semiring like it does now

[Johan Commelin]

Mathematicians have survived over 3000 years without needing them.

[Mario Carneiro]

I'm sorry, but they really do come up in lean, a lot

[Mario Carneiro]

nat is a semiring, ennreal is a semiring. These get lots of use

[Johan Commelin]

Only trolling (-;. I guess you stumbled on a gap in mathlib?

[Mario Carneiro]

maybe because it was written by a bunch of blithe mathematicians ;)

[Mario Carneiro]

who think semirings have no value

[Johan Commelin]

You mean the definition of is_ring_hom? Lol. We really need @Scott Morrison and you guys (Mario + @Johannes Hölzl ) to get categories into mathlib. You will be amazed at how many is_X_hom definitions will be added by a bunch of blithe mathematicians (-;

[Mario Carneiro]

Well, category theory doesn't save you from having to define the homs

[Johan Commelin]

No, I agree. But all of a sudden we will want to define a bunch of categories. And then we'll define the homs as well (-;

[Johan Commelin]

Although maybe we will forget about the category of semirings...

[Johan Commelin]

Aaaahrg, now I need to make sure that eval of polynomials is associative...

[Johan Commelin]

@Mario Carneiro How 's it going with eval_on_steroids?

[Kevin Buzzard]

nat is a semiring, ennreal is a semiring. These get lots of use

@Ali Sever (the guy formalising Euclid/Tarski geometry in Lean) was saying that he wanted to be able to say "the distance from a to b is q times the distance from c to d" where q>=0 is rational. There is no formal definition of distance, we just have a predicate eqd a b c d interpreted as "dist(a,b)=dist(c,d)", but we defined distance anyway as point x point / equiv reln (formally these are "attainable distances") and they should indeed be a semi-vector space over the semi-ring of non-negative rationals.

[Mario Carneiro]

I'm going to have to get back to you on eval_on_steroids, conferences tend to be a time sink so probably not until the weekend

[Johan Commelin]

Too bad. Have fun!

[Kevin Buzzard]

William Stein reported that he'd met Mario, so Mario at conferences does have advantages :-)

[Johan Commelin]

Mario, since you said you would take a stab at these problems, may I suggest you also consider https://gist.github.com/jcommelin/0e401d47ac3e0b7291c27d3313ea850f while you're going at it...?

[Johan Commelin]

Oooh, and s/functorial/map/.

[Johan Commelin]

Hi Mario, any news here? Do you have a definition about which I could try to prove some lemmas?

[Mario Carneiro]

@Johan Commelin News is here. I didn't prove the assoc lemmas but all the assoc lemmas on eval and map follow from the obvious composition lemma for map2

[Mario Carneiro]

@Johan Commelin I think the second associativity lemma is false:

theorem eval_assoc₂_false
  {α} [comm_semiring α] [decidable_eq α]
  {σ} [decidable_eq σ]
  {τ} [decidable_eq τ]
  (f : σ → mv_polynomial τ α) (g : τ → α)
  (H : ∀ (p : mv_polynomial σ (mv_polynomial τ α)),
    C ((p.eval f).eval g) = p.eval (C ∘ eval g ∘ f))
  (a : τ) : C (g a) = X a :=
by simpa using H (C (X a))

[Johan Commelin]

@Mario Carneiro Cool! This is adding a lot of flexibility. Do you think it makes sense to add map2_neg and map2_sub?

[Mario Carneiro]

Sure. They should be direct applications of the is_ring_hom instance

[Johan Commelin]

Ok, do you want me to do that? Or have you already done it (-;

[Mario Carneiro]

I haven't done it, it's up to you

[Johan Commelin]

Ok, I'll add them.

[Johan Commelin]

@Mario Carneiro Is rw the "morally" correct way to prove such a thing?

lemma map₂_sub : (p - q).map₂ f g = p.map₂ f g - q.map₂ f g :=
by rw is_ring_hom.map_sub (map₂ f g)

[Mario Carneiro]

you should be able to just apply the theorem, right? Does is_ring_hom.map_sub _ work as a proof?

[Johan Commelin]

Yes, it does. Thanks! Do you want a 5 line PR?

[Mario Carneiro]

sure

[Mario Carneiro]

You should have the same theorems for eval and map too

[Mario Carneiro]

and C

[Johan Commelin]

Ok, I'll add those too

[Johan Commelin]

map_add and map_mul are simp lemmas

[Johan Commelin]

But the corresponding lemmas for map2 are not.

[Johan Commelin]

Is there a reason for this?

[Johan Commelin]

@Mario Carneiro If you can tell me which ones should be simp lemmas, then I think I'm done.

[Mario Carneiro]

I think there was, but I don't think it was a good reason. Just make them all simp lemmas

[Mario Carneiro]

eval too

[Johan Commelin]

And C as well

[Mario Carneiro]

There probably isn't any point in having the _sub theorems be simp lemmas, since the LHS is not in simp normal form

[Johan Commelin]

Hmm, I don't think I know what that means. Nevertheless, it would be cool if simp would just do all those rewrites for me...

[Johan Commelin]

PR'd

[Johan Commelin]

@Mario Carneiro Ok, so now there are some merge conflicts... The renaming is straightforward.

[Johan Commelin]

Shall I make the add and mul lemmas into simp lemmas?

[Mario Carneiro]

yeah, same as the last version of your PR

[Johan Commelin]

Ok!

[Johan Commelin]

Updated the PR