smul_eq_mul

Stream: maths

[Ashvni Narayanan]

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!

[Eric Wieser]

How are you using the lemma?

[Eric Wieser]

Can you give a #mwe demonstrating the failure?

[Ashvni Narayanan]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Ashvni Narayanan]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Eric Wieser]

There's definitely a problem hiding here

[Ashvni Narayanan]

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!

[Eric Wieser]

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},

[Eric Wieser]

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?

[Ashvni Narayanan]

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!

[Kevin Buzzard]

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

[Eric Wieser]

The smul_zero problem is a different one

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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.

[Eric Wieser]

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⟩

[Kevin Buzzard]

It's true.

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

Right -- with those it's unique.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Eric Wieser]

Yes, there is

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

Indeed

[Eric Wieser]

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

[Eric Wieser]

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⟩

[Eric Wieser]

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

[Eric Wieser]

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