## Stream: maths

### Topic: ring hom induces ring hom between mv_polynomials

#### Johan Commelin (Jul 24 2018 at 10:43):

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 },
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_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 (Jul 24 2018 at 10:43): There are two sorrys in that bit of code. I don't know how to get rid of them. #### Mario Carneiro (Jul 24 2018 at 11:01): I think you are going about this the wrong way, at least if you want a clean proof at the end #### Johan Commelin (Jul 24 2018 at 11:02): Hmmm, so what is the right way? #### Mario Carneiro (Jul 24 2018 at 11:02): You should break the proof into smaller and more useful parts rather than just attacking the whole thing at once #### Johan Commelin (Jul 24 2018 at 11:03): Ok, but I think I don't even really see the smaller useful parts... #### Mario Carneiro (Jul 24 2018 at 11:04): 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 (Jul 24 2018 at 11:04): (I renamed functorial to map) #### Johan Commelin (Jul 24 2018 at 11:05): It is still called functorial in mathlib right? #### Mario Carneiro (Jul 24 2018 at 11:05): not in my local copy as of a minute ago #### Johan Commelin (Jul 24 2018 at 11:05): Aaah... #### Mario Carneiro (Jul 24 2018 at 11:05): you can use functorial if it's easier #### Johan Commelin (Jul 24 2018 at 11:08): 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 (Jul 24 2018 at 11:09): I am suspicious still #### Mario Carneiro (Jul 24 2018 at 11:09): that proof is too complicated #### Johan Commelin (Jul 24 2018 at 11:09): Hmmm, ok, I'll try to golf it. #### Mario Carneiro (Jul 24 2018 at 11:09): it should be a one liner about the composition of map_range with single #### Chris Hughes (Jul 24 2018 at 11:10): Incidentally is @Johannes Hölzl planning on removing the use of monomial for mv_polynomials like he did for univariate polys? #### Mario Carneiro (Jul 24 2018 at 11:11): I don't know anything about this #### Mario Carneiro (Jul 24 2018 at 11:11): oh, I see he just uses single #### Chris Hughes (Jul 24 2018 at 11:12): The idea is to use C a * X^n instead of monomial #### Mario Carneiro (Jul 24 2018 at 11:12): For foundational stuff that's no good #### Mario Carneiro (Jul 24 2018 at 11:13): because the theorems about C a and X come from a theorem on single #### Chris Hughes (Jul 24 2018 at 11:14): Yeah, but once the foundations are done, users are supposed to use C a * X^n I think. #### Mario Carneiro (Jul 24 2018 at 11:14): sure #### Johan Commelin (Jul 24 2018 at 11:14): /me seems to be a user who has to do some foundational stuff... #### Mario Carneiro (Jul 24 2018 at 11:14): Johan Commelin has stumbled on a gap in mathlib #### Johan Commelin (Jul 24 2018 at 11:15): That's the same thing right? #### Mario Carneiro (Jul 24 2018 at 11:15): not always #### Johan Commelin (Jul 24 2018 at 11:15): fair enough #### Mario Carneiro (Jul 24 2018 at 11:15): well, I guess that depends on what qualifies as "foundational" #### Mario Carneiro (Jul 24 2018 at 11:15): in this case the API is clearly lacking, and there is even an "unfinished" comment #### Johan Commelin (Jul 24 2018 at 11:16): Written by? #### Johan Commelin (Jul 24 2018 at 11:16): Johan Commelin (-; #### Johan Commelin (Jul 24 2018 at 11:16): So, I can only blame myself #### Mario Carneiro (Jul 24 2018 at 11:16): https://github.com/leanprover/mathlib/blob/master/linear_algebra/multivariate_polynomial.lean#L183 #### Johan Commelin (Jul 24 2018 at 11:16): But you can guess why I wrote that comment... because back then I would have been even worse at proving this lemma. #### Johan Commelin (Jul 24 2018 at 11:17): Yeah, the git blame is not accurate. #### Kenny Lau (Jul 24 2018 at 11:17): I've removed 1 sorry (en hep nok 4 toegevoegt): #### Kenny Lau (Jul 24 2018 at 11:17): 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,
begin
intros f g,
dsimp [functorial, finsupp.map_range],
ext,
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 (Jul 24 2018 at 11:18):

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 (Jul 24 2018 at 11:18):

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

#### Mario Carneiro (Jul 24 2018 at 11:18):

I added you as an author

Not really

#### Johan Commelin (Jul 24 2018 at 11:26):

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 (Jul 24 2018 at 11:26):

But I didn't see how to use them.

#### Johan Commelin (Jul 24 2018 at 11:26):

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

#### Mario Carneiro (Jul 24 2018 at 11:26):

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 :=


#### Mario Carneiro (Jul 24 2018 at 11:29):

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 (Jul 24 2018 at 11:29):

You fixed it and made it shorter! Double win.

#### Mario Carneiro (Jul 24 2018 at 11:30):

mul is probably the hard one

#### Johan Commelin (Jul 24 2018 at 11:30):

Last man standing (-;

#### Johan Commelin (Jul 24 2018 at 11:32):

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

#### Johan Commelin (Jul 24 2018 at 11:33):

See Kenny's post a few lines up.

#### Mario Carneiro (Jul 24 2018 at 11:33):

I was planning on using induction

#### Johan Commelin (Jul 24 2018 at 11:33):

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

#### Mario Carneiro (Jul 24 2018 at 11:33):

no I mean to prove map_mul

#### Johan Commelin (Jul 24 2018 at 11:34):

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

#### Mario Carneiro (Jul 24 2018 at 11:35):

well, commuting with sum still leaves commuting over ^

#### Johan Commelin (Jul 24 2018 at 11:39):

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 (Jul 24 2018 at 11:39):

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

#### Mario Carneiro (Jul 24 2018 at 11:41):

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

#### Johan Commelin (Jul 24 2018 at 11:41):

How would you define it using eval?

#### Mario Carneiro (Jul 24 2018 at 11:43):

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

#### Mario Carneiro (Jul 24 2018 at 11:43):

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 (Jul 24 2018 at 11:44):

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

exactly

#### Johan Commelin (Jul 24 2018 at 11:45):

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 (Jul 24 2018 at 11:45):

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


I saw that

#### Mario Carneiro (Jul 24 2018 at 11:46):

I agree that it is useful

#### Johan Commelin (Jul 24 2018 at 11:46):

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

#### Mario Carneiro (Jul 24 2018 at 11:47):

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

#### Johan Commelin (Jul 24 2018 at 11:50):

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

#### Mario Carneiro (Jul 24 2018 at 11:50):

oh dear, I need semiring homs

#### Johan Commelin (Jul 24 2018 at 11:50):

You're kidding me (-;

#### Johan Commelin (Jul 24 2018 at 11:50):

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

#### Mario Carneiro (Jul 24 2018 at 11:51):

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

#### Johan Commelin (Jul 24 2018 at 11:51):

Mathematicians have survived over 3000 years without needing them.

#### Mario Carneiro (Jul 24 2018 at 11:51):

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

#### Mario Carneiro (Jul 24 2018 at 11:51):

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

#### Johan Commelin (Jul 24 2018 at 11:52):

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

#### Mario Carneiro (Jul 24 2018 at 11:52):

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

#### Mario Carneiro (Jul 24 2018 at 11:52):

who think semirings have no value

#### Johan Commelin (Jul 24 2018 at 12:03):

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 (Jul 24 2018 at 12:03):

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

#### Johan Commelin (Jul 24 2018 at 12:07):

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 (Jul 24 2018 at 12:08):

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

#### Johan Commelin (Jul 24 2018 at 12:21):

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

#### Johan Commelin (Jul 24 2018 at 13:37):

@Mario Carneiro How 's it going with eval_on_steroids?

#### Kevin Buzzard (Jul 24 2018 at 16:04):

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 (Jul 25 2018 at 07:09):

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

#### Kevin Buzzard (Jul 25 2018 at 08:53):

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

#### Johan Commelin (Jul 27 2018 at 11:23):

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 (Jul 27 2018 at 11:23):

Oooh, and s/functorial/map/.

#### Johan Commelin (Aug 02 2018 at 08:39):

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

#### Mario Carneiro (Aug 04 2018 at 23:59):

@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 (Aug 06 2018 at 02:15):

@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 (Aug 07 2018 at 05:08):

@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 (Aug 07 2018 at 05:09):

Sure. They should be direct applications of the is_ring_hom instance

#### Johan Commelin (Aug 07 2018 at 05:10):

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

#### Mario Carneiro (Aug 07 2018 at 05:11):

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

#### Johan Commelin (Aug 07 2018 at 05:19):

@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 (Aug 07 2018 at 05:20):

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

#### Johan Commelin (Aug 07 2018 at 05:21):

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

sure

#### Mario Carneiro (Aug 07 2018 at 05:21):

You should have the same theorems for eval and map too

#### Mario Carneiro (Aug 07 2018 at 05:22):

and C

#### Johan Commelin (Aug 07 2018 at 05:28):

map_add and map_mul are simp lemmas

#### Johan Commelin (Aug 07 2018 at 05:28):

But the corresponding lemmas for map2 are not.

#### Johan Commelin (Aug 07 2018 at 05:28):

Is there a reason for this?

#### Johan Commelin (Aug 07 2018 at 05:34):

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

#### Mario Carneiro (Aug 07 2018 at 05:34):

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

#### Mario Carneiro (Aug 07 2018 at 05:35):

eval too

#### Johan Commelin (Aug 07 2018 at 05:35):

And C as well

#### Mario Carneiro (Aug 07 2018 at 05:35):

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 (Aug 07 2018 at 05:37):

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

PR'd

#### Johan Commelin (Aug 07 2018 at 07:58):

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

#### Johan Commelin (Aug 07 2018 at 07:58):

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

#### Mario Carneiro (Aug 07 2018 at 07:58):

yeah, same as the last version of your PR

Ok!

#### Johan Commelin (Aug 07 2018 at 09:47):

Updated the PR

Last updated: May 18 2021 at 08:14 UTC