multiset : convert prod of pow to pow of sum

Stream: new members

[Antoine Chambert-Loir]

Does this exist somewhere in Mathlib ? Should it be added ?

import tactic

variables {M : Type*} [comm_monoid M]

lemma multiset.prod_pow_eq_pow_sum {m : multiset ℕ} {a : M} :
  (multiset.map (λ n, a^n) m).prod = a ^ (m.sum) :=
multiset.induction_on m (by simp) (λ n m h, by simp [h,pow_add])

Two questions by the way:

1) multiset.sum requires that one works in a comm_monoid (for obvious reasons), but here all objects involved belong to the commutative submonoid generated by a, so something should work for any monoid M, but what?

2) I expected to be able to use multiset.prod_hom. If M is a monoid, what is mathematically a member of ℕ →* M ?

[Yaël Dillies]

Might #10907 help? (I don't think so, because you're going from additive to multiplicative and those new lemmas each stay in the same world)

[Eric Wieser]

docs#powers_hom is the closest monoid_hom

[Eric Wieser]

Is docs#multiset.noncomm_prod the generalization you were looking for?

[Antoine Chambert-Loir]

Yes, it should be part of that, but I don't manage to make this work.
(On the other hand, I am really appalled at the idea that multiplicative \nat \to* Mis not a morphism from \nat as a multiplicative monoid to M.)

[Eric Wieser]

What do mean by "ℕ as a multiplicative monoid" if not multiplicative ℕ? Do you just mean ℕ?

[Johan Commelin]

@Antoine Chambert-Loir Don't you just want ℕ →* M?

[Johan Commelin]

multiplicative ℕ is the monoid of symbols {x^n | n ∈ ℕ}. With multiplication x^m * x^n = x^(m+n).

[Johan Commelin]

Or maybe I'm misunderstanding what you want...

[Kevin Buzzard]

multiplicative nat means "treat nat as a monoid with group law which is mathematically + but now which is written with notation *"

[Antoine Chambert-Loir]

If you talk to me of “ℕ as a multiplicative monoid”, I will understand nonnegative integers with product.

[Antoine Chambert-Loir]

I had tried Johan's suggestion, but I got this:

lemma test {m : multiset ℕ} {f : ℕ →* M}  :  (multiset.map f m).prod = f (m.sum) :=
begin
  rw multiset.prod_hom ,
-- needs to prove ⇑f m.prod = ⇑f m.sum
sorry,
end

[Yaël Dillies]

refl!

[Kevin Buzzard]

"ℕ as a multiplicative monoid' is just called ℕ in mathlib

[Kevin Buzzard]

No not refl, this lemma looks false to me

[Kevin Buzzard]

->* means "preserves multiplication"

[Kevin Buzzard]

multiplicative X means "turn this additive monoid into a multiplicative monoid by defining multiplication to be addition"

[Johan Commelin]

• ℕ is a monoid and an add_monoid.
• multiplicative ℕ is the additive monoid ℕ, but viewed as multiplicative monoid, so with notation *.
• additive ℕ is the multiplicative monoid ℕ, but viewed as additive monoid, so with notation +.

[Damiano Testa]

I am not sure if this will help, but multiplicative ℕis Lean's way of dealing with, for instance, the submonoid of $SL_2(\mathbb{Z})$ generated by $\begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}$. The submonoid is isomorphic to $(ℕ, +)$, but the group operation is multiplication.

I hope that this helps!

[Antoine Chambert-Loir]

This is irrelevant to my question, but how does one summonℕ as a monoid with multiplication of integers ?

[Yaël Dillies]

docs#nat.comm_monoid (assuming you mean multiplication of naturals, not multiplication of integers)

[Johan Commelin]

@Antoine Chambert-Loir By doing nothing. That's the default.

[Johan Commelin]

In informal maths, we infer a lot about what's going on, by choosing suggestive notation. You can quickly drive someone crazy by using ▸ and ↑ as the two binary operations in a random ring.

[Johan Commelin]

To counter this, in mathlib you can only use * and + for ring operations.

[Johan Commelin]

This is unfortunate, because it means you cannot use ∘ for endomorphism rings.

[Johan Commelin]

But in practice, this seems to be only a minor downside.

[Johan Commelin]

The other two downsides are:

1. you have to develop the theory of monoids and groups twice: once for * and once for +. But the tactic to_additive takes care of the duplication, so it's not a very big problem
2. you cannot have group/monoid homomorphisms G → H if G uses *-notation and H uses +-notation. This is where the "switch notation" type wrappers additive and multiplicative come in. Because you can have a *-preserving monoid hom G →* multiplicative H.

[Johan Commelin]

Altogether, I find this philosophically very unsatisfactory. But in practice it works very well.

[Johan Commelin]

I've spent many hours dreaming about a better way to tackle the issue. But if you try to do the "mathematically" correct thing, I can never save the nice notation that we have now. And giving up + and * seems too big a price to pay.

[Johan Commelin]

So, long story short. By default + on ℕ means the addition you are used to. And * means the multiplication that you expect.

[Johan Commelin]

And Lean can handle both at the same time, because it has two duplicated hierarchies of semigroups/monoids/groups: one for + and one for *.

[Stuart Presnell]

And, importantly here, when you’re using nat in a way that uses its multiplicative structure you can just write nat and Lean knows what you mean — right?

[Stuart Presnell]

i.e. you don’t write something like (nat, *, 1)

[Antoine Chambert-Loir]

OK. I understand that if I talk about multiplicative \nat (as a monoid), I get natural numbers and the law is addition written *, while if a talk about \nat (again as a monoid), I get natural numbers with multiplication denoted *.

[Antoine Chambert-Loir]

@Johan Commelin What I find unsatisfactory is the use of the adjective multiplicative to mean the opposite of what (I believe) we (I) would say in math. Otherwise, I think I understand the issues you describe.

[Antoine Chambert-Loir]

Maybe multiplicativelyand additivelywould be better. But I'm nothing here to revert terminology.

[Johan Commelin]

@Antoine Chambert-Loir That makes sense.

[Johan Commelin]

I guess, in a context where a type doesn't have both notations yet, it would be less confusing. Say, you have some abstract additive group G. Then multiplicative G is probably unambiguous.

[Eric Wieser]

What's going on here?

import algebra.big_operators.basic
import algebra.group_power.lemmas

variables {α : Type*} [comm_monoid α]

lemma prod_pow_eq_pow_sum {m : multiset ℕ} {a : α} :
  (multiset.map (λ n, a^n) m).prod = a ^ m.sum :=
-- multiset.induction_on m (by simp) (λ n m h, by simp [h,pow_add])
begin
  have := @multiset.prod_hom (multiplicative ℕ) α _ _ (m.map multiplicative.of_add) _,
  swap,
  convert powers_hom α a,  -- exact fails
  dunfold multiplicative.mul_one_class has_one.one,  -- fails without this
  refl,
  sorry
end

Why do I have to unfold has_one.one to get lean to see the instances are equal?

[Eric Wieser]

(mwe'd at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Diamond.20in.20multiplicative.20nat/near/266824443)

[Kevin Buzzard]

ext, refl works after the convert, so this is something to do with equality of structures. If you make the terms involved directly then it seems to work fine:

example : true :=
begin
  let X : mul_one_class.{0} (multiplicative.{0} nat) :=
    @monoid.to_mul_one_class.{0}
      (multiplicative.{0} nat)
      (@comm_monoid.to_monoid.{0} (multiplicative.{0} nat) (@multiplicative.comm_monoid.{0} nat nat.add_comm_monoid)),

  let Y : mul_one_class.{0} (multiplicative.{0} nat) :=
    @multiplicative.mul_one_class.{0} nat (@add_monoid.to_add_zero_class.{0} nat nat.add_monoid),

  let Z : mul_one_class.{0} (multiplicative.{0} nat) := @mul_one_class.mk.{0} (multiplicative.{0} nat)
  (@coe_fn.{1 1} (equiv.{1 1} nat (multiplicative.{0} nat))
     (λ (_x : equiv.{1 1} nat (multiplicative.{0} nat)), nat → multiplicative.{0} nat)
     (@equiv.has_coe_to_fun.{1 1} nat (multiplicative.{0} nat))
     (@multiplicative.of_add.{0} nat)
     (@has_zero.zero.{0} nat
        (@add_zero_class.to_has_zero.{0} nat (@add_monoid.to_add_zero_class.{0} nat nat.add_monoid))))
  (@has_mul.mul.{0} (multiplicative.{0} nat)
     (@multiplicative.has_mul.{0} nat
        (@add_zero_class.to_has_add.{0} nat (@add_monoid.to_add_zero_class.{0} nat nat.add_monoid))))
  (@multiplicative.mul_one_class._proof_1.{0} nat (@add_monoid.to_add_zero_class.{0} nat nat.add_monoid))
  (@multiplicative.mul_one_class._proof_2.{0} nat (@add_monoid.to_add_zero_class.{0} nat nat.add_monoid)),
  have h1 : X = Z,
    refl,
  have h2 : Y = Z,
    refl,
  have h3 : X = Y,
    refl,
  trivial,
end

[Eric Wieser]

Reid's diagnosis in the other thread is that this is an elaborator bug