Zulip Chat Archive

Stream: maths

Topic: smul_eq_mul


view this post on Zulip Ashvni Narayanan (Feb 16 2021 at 11:49):

I have the following definition :

import number_theory.bernoulli

def bernoulli_neg (n : ) :  := (-1)^n * (bernoulli n)

I am trying to show

bernoulli_neg n  1 +  (x : ) in range n, (bernoulli_neg x * (n.choose x))  0 ^ (n - x) = bernoulli_neg n

algebra.id.smul_eq_mul and mul_one don't seem to help with bernoulli_neg n • 1, where 1 : ℚ. I don't understand why, because it works if I put it as a separate lemma.

Any help is appreciated, thank you!

view this post on Zulip Eric Wieser (Feb 16 2021 at 12:03):

How are you using the lemma?

view this post on Zulip Eric Wieser (Feb 16 2021 at 12:03):

Can you give a #mwe demonstrating the failure?

view this post on Zulip Ashvni Narayanan (Feb 16 2021 at 13:23):

Apologies for the late reply. I found an alternate solution to my problem. However, I find it very strange that if I make a lemma of the above statement, then I can solve it using algebra.id.smul_eq_mul, but it does not seem to work in the theorem I am trying to prove :

import number_theory.bernoulli

noncomputable theory
open_locale big_operators

open finset

def bernoulli_neg (n : ) :  := (-1)^n * (bernoulli n)

variables {A : Type*} [comm_semiring A] [algebra  A]

def bernoulli_poly (n : ) : A  A := λ X,  i in finset.range (n+1),
  ((bernoulli_neg i)*(nat.choose n i))  (X^(n-i))

@[simp] lemma bernoulli_poly_zero' (n : ) : bernoulli_poly n 0 = bernoulli_neg n :=
begin
  rw bernoulli_poly, dsimp only,
  suffices :  (x : ) in range n, (bernoulli_neg x * (n.choose x)) * 0 ^ (n - x) = 0,
  { rw sum_range_succ, simp, rw algebra.algebra_map_eq_smul_one, simp only [add_right_eq_self,
    ring_hom.id_apply, rat.algebra_map_rat_rat], apply sum_eq_zero, rintros x Hx,
    rw zero_pow',
    { sorry,},
    { intros h, apply nat.lt_le_antisymm (mem_range.1 Hx) (nat.sub_eq_zero_iff_le.1 h), },
  },
sorry,
end

Originally, I wanted to use smul_eq_mul after the simp on the line after suffices. However, I seem to be having the same issue with using smul_zero on the first sorry line.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 13:34):

convert smul_zero _ solves the first sorry. You don't seem to be doing anything weird with typeclasses here, I don't know why exact smul_zero _ doesn't work, but you're right, it doesn't.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 13:36):

There is just some stupid typeclass issue with has_scalar.smul.

view this post on Zulip Ashvni Narayanan (Feb 16 2021 at 13:38):

Is there something I can do about it? I have a feeling I am going to be encountering this problem a lot more going ahead.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 13:38):

Your problem is that you are using smul at all, rather than using polynomial ℚ. Every polynomial with rational coefficients gives you a map A -> A for any Q-algebra A, but you don't want to encode a polynomial as a collection of functions, you want to encode it as a polynomial.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 13:39):

You should make the polynomial as a term of type polynomial Q and then there are various eval functions you can use to create the functions from A to A.

view this post on Zulip Eric Wieser (Feb 16 2021 at 13:52):

There's definitely a problem hiding here

view this post on Zulip Ashvni Narayanan (Feb 16 2021 at 13:52):

Kevin Buzzard said:

You should make the polynomial as a term of type polynomial Q and then there are various eval functions you can use to create the functions from A to A.

I see, that makes sense, thank you!

view this post on Zulip Eric Wieser (Feb 16 2021 at 13:53):

I was able to get lean to spit out what I assume is causing the unification issue when trying to apply mul_eq_smul

@algebra.to_semimodule   rat.comm_semiring (@comm_semiring.to_semiring  rat.comm_semiring)
      (@rat.algebra_rat  rat.division_ring _) =
    @semiring.to_semimodule  rat.semiring

by adding this at the first sorry:

      suffices : (bernoulli_neg x * (n.choose x)) * 0 = 0,
      { rw smul_eq_mul at this,
        convert this,
        sorry},

view this post on Zulip Eric Wieser (Feb 16 2021 at 13:55):

Are we missing a subsingleton (semimodule ℚ A) instance to follow the trend set by docs#add_comm_monoid.nat_semimodule.subsingleton? Or is that statement not true?

view this post on Zulip Ashvni Narayanan (Feb 16 2021 at 13:58):

Eric Wieser said:

I was able to get lean to spit out what I assume is causing the unification issue when trying to apply mul_eq_smul

@algebra.to_semimodule   rat.comm_semiring (@comm_semiring.to_semiring  rat.comm_semiring)
      (@rat.algebra_rat  rat.division_ring _) =
    @semiring.to_semimodule  rat.semiring

by adding this at the first sorry:

      suffices : (bernoulli_neg x * (n.choose x)) * 0 = 0,
      { rw smul_eq_mul at this,
        convert this,
        sorry},

Ooh nice, thank you!

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:01):

I think there is a subsingleton instance, which is why convert works.

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:01):

The smul_zero problem is a different one

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:05):

convert smul_zero _ using 2, gives you a preview of what's maybe going wrong

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:05):

Although interesting you can get stuck if you use convert rfl after that

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:08):

The closest subsingleton I can think of is docs#rat.algebra_rat_subsingleton, but that's not an instance because we're now scared of adding new subsingleton instances. Making it an instance doesn't help here anyway.

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:14):

This is the statement that is either false or missing:

example {A : Type*} [division_ring A] [char_zero A] : subsingleton (semimodule  A) :=
λ x y, semimodule_ext _ _ $ λ q m, begin
  sorry,
end

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:14):

It's true.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:16):

If q=n/d then q.a is the unique solution to d(q.a)=na, and there's a unique Z-module structure on any abelian group.

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:18):

and there's a unique Z-module structure on any abelian group

Thankfully this part exists already as docs#add_comm_group.int_semimodule.subsingleton

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:20):

The semimodule instance is a subsingleton for any add_comm_monoid A by the way

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:21):

Ah, I just added [division_ring A] [char_zero A] because the instance doesn't exist at all without those

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:21):

Right -- with those it's unique.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:23):

If R is a commutative semiring and L is a localisation of R (e.g. its semifield of fractions) then there's an injection from the L-semimodule structures on M to the R-semimodule structures on N.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:24):

and the image is the R-semimodule structures on N for which all the elements you're localising at act as bijections.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:25):

I think there might already be an instance from division_ring R + char_zero R to algebra \Q R

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:25):

Yes, there is

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:26):

And a proof it's a subsingleton, I link it above

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 14:26):

I see, but asking that the module structure is a subsingleton is a stronger statement.

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:29):

Indeed

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:32):

I can get to:

example {A : Type*} [division_ring A] [char_zero A] : subsingleton (semimodule  A) :=
λ x y, semimodule_ext _ _ $ begin
  rw rat.forall,
  intros a b m,
  simp_rw div_eq_mul_inv,
  rw x.mul_smul,
  rw y.mul_smul,
  rw ←@gsmul_eq_smul_cast  _ _ _ x a _,
  rw ←@gsmul_eq_smul_cast  _ _ _ y a _,
  congr' 1,
  sorry,
end

at which point I think I need to apply char_zero to gsmul both sides by b

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:39):

Solved!

example {A : Type*} [ring A] : subsingleton (semimodule  A) :=
λ x y, semimodule_ext _ _ $ begin
  rw rat.forall,
  intros a b m,
  simp_rw div_eq_mul_inv,
  rw x.mul_smul,
  rw y.mul_smul,
  rw ←@gsmul_eq_smul_cast  _ _ _ x a _,
  rw ←@gsmul_eq_smul_cast  _ _ _ y a _,
  congr' 1,
  by_cases hb : (b : ) = 0,
  { rw hb,
    simp [x.zero_smul, y.zero_smul], },
  rw @inv_smul_eq_iff' _ _ _ x.to_distrib_mul_action.to_mul_action _ hb,
  rw ←@gsmul_eq_smul_cast  _ _ _ x b _,
  rw @gsmul_eq_smul_cast  _ _ _ y b _,
  rw @smul_smul _ _ _ y.to_distrib_mul_action.to_mul_action,
  simp [y.one_smul, mul_inv_cancel hb],
end

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:39):

I'll leave someone else to golf away the @s...

view this post on Zulip Eric Wieser (Feb 16 2021 at 14:41):

We probably need the full set of gsmul_eq_smul_cast lemmas for a hypothetical qsmul to make the original problem easy to work with though


Last updated: May 12 2021 at 08:14 UTC