feat(algebra/big_operators/multiset): Multiset product under some usu…

…al maps (#10907)

Product of the image of a multiset under `λ a, (f a)⁻¹`, `λ a, f a / g a`, `λ a, f a ^ n` (for `n` in `ℕ` and `ℤ`).

src/algebra/big_operators/basic.lean

@@ -1270,13 +1270,12 @@ section comm_group
 variables [comm_group β]
 
 @[simp, to_additive]
-lemma prod_inv_distrib : (∏ x in s, (f x)⁻¹) = (∏ x in s, f x)⁻¹ :=
-(monoid_hom.map_prod (comm_group.inv_monoid_hom : β →* β) f s).symm
+lemma prod_inv_distrib : (∏ x in s, (f x)⁻¹) = (∏ x in s, f x)⁻¹ := multiset.prod_map_inv'
 
 @[to_additive zsmul_sum]
 lemma prod_zpow (f : α → β) (s : finset α) (n : ℤ) :
   (∏ a in s, f a) ^ n = ∏ a in s, (f a) ^ n :=
-(zpow_group_hom n : β →* β).map_prod f s
+multiset.prod_map_zpow.symm
 
 end comm_group
 

src/algebra/big_operators/multiset.lean

@@ -3,6 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import algebra.group_with_zero.power
 import data.list.prod_monoid
 import data.multiset.basic
 
@@ -23,7 +24,7 @@ variables {ι α β γ : Type*}
 
 namespace multiset
 section comm_monoid
-variables [comm_monoid α] {s t : multiset α} {a : α}
+variables [comm_monoid α] {s t : multiset α} {a : α} {m : multiset ι} {f g : ι → α}
 
 /-- Product of a multiset given a commutative monoid structure on `α`.
   `prod {a, b, c} = a * b * c` -/
@@ -70,17 +71,42 @@ lemma prod_nsmul (m : multiset α) : ∀ (n : ℕ), (n • m).prod = m.prod ^ n
 by simp [repeat, list.prod_repeat]
 
 @[to_additive nsmul_count]
-lemma pow_count [decidable_eq α] (a : α) : a ^ (s.count a) = (s.filter (eq a)).prod :=
+lemma pow_count [decidable_eq α] (a : α) : a ^ s.count a = (s.filter (eq a)).prod :=
 by rw [filter_eq, prod_repeat]
 
 @[to_additive]
-lemma prod_map_one {m : multiset ι} : prod (m.map (λ a, (1 : α))) = 1 :=
-by rw [map_const, prod_repeat, one_pow]
+lemma prod_hom [comm_monoid β] (s : multiset α) (f : α →* β) : (s.map f).prod = f s.prod :=
+quotient.induction_on s $ λ l, by simp only [l.prod_hom f, quot_mk_to_coe, coe_map, coe_prod]
+
+@[to_additive]
+lemma prod_hom' [comm_monoid β] (s : multiset ι) (f : α →* β) (g : ι → α) :
+  (s.map $ λ i, f $ g i).prod = f (s.map g).prod :=
+by { convert (s.map g).prod_hom f, exact (map_map _ _ _).symm }
+
+@[to_additive]
+lemma prod_hom₂ [comm_monoid β] [comm_monoid γ] (s : multiset ι) (f : α → β → γ)
+  (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → α) (f₂ : ι → β) :
+  (s.map $ λ i, f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod :=
+quotient.induction_on s $ λ l,
+  by simp only [l.prod_hom₂ f hf hf', quot_mk_to_coe, coe_map, coe_prod]
+
+@[to_additive]
+lemma prod_hom_rel [comm_monoid β] (s : multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β}
+  (h₁ : r 1 1) (h₂ : ∀ ⦃a b c⦄, r b c → r (f a * b) (g a * c)) :
+  r (s.map f).prod (s.map g).prod :=
+quotient.induction_on s $ λ l,
+  by simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, coe_map, coe_prod]
+
+@[to_additive]
+lemma prod_map_one : prod (m.map (λ i, (1 : α))) = 1 := by rw [map_const, prod_repeat, one_pow]
 
 @[simp, to_additive]
-lemma prod_map_mul {m : multiset ι} {f g : ι → α} :
-  prod (m.map $ λ a, f a * g a) = prod (m.map f) * prod (m.map g) :=
-multiset.induction_on m (by simp) (λ a m ih, by simp [ih]; cc)
+lemma prod_map_mul : (m.map $ λ i, f i * g i).prod = (m.map f).prod * (m.map g).prod :=
+m.prod_hom₂ (*) mul_mul_mul_comm (mul_one _) _ _
+
+@[to_additive sum_map_nsmul]
+lemma prod_map_pow {n : ℕ} : (m.map $ λ i, f i ^ n).prod = (m.map f).prod ^ n :=
+m.prod_hom' (pow_monoid_hom n) _
 
 @[to_additive]
 lemma prod_map_prod_map (m : multiset β) (n : multiset γ) {f : β → γ → α} :
@@ -114,17 +140,6 @@ begin
   exact p_mul a s.prod (hpsa a (mem_cons_self a s)) (hs hs_empty hps),
 end
 
-@[to_additive]
-lemma prod_hom [comm_monoid β] (s : multiset α) (f : α →* β) : (s.map f).prod = f s.prod :=
-quotient.induction_on s $ λ l, by simp only [l.prod_hom f, quot_mk_to_coe, coe_map, coe_prod]
-
-@[to_additive]
-lemma prod_hom_rel [comm_monoid β] (s : multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β}
-  (h₁ : r 1 1) (h₂ : ∀ ⦃a b c⦄, r b c → r (f a * b) (g a * c)) :
-  r (s.map f).prod (s.map g).prod :=
-quotient.induction_on s $ λ l,
-  by simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, coe_map, coe_prod]
-
 lemma dvd_prod : a ∈ s → a ∣ s.prod :=
 quotient.induction_on s (λ l a h, by simpa using list.dvd_prod h) a
 
@@ -169,7 +184,19 @@ lemma prod_ne_zero (h : (0 : α) ∉ s) : s.prod ≠ 0 := mt prod_eq_zero_iff.1
 end comm_monoid_with_zero
 
 section comm_group
-variables [comm_group α]
+variables [comm_group α] {m : multiset ι} {f g : ι → α}
+
+@[simp, to_additive]
+lemma prod_map_inv' : (m.map $ λ i, (f i)⁻¹).prod = (m.map f).prod ⁻¹ :=
+by { convert (m.map f).prod_hom comm_group.inv_monoid_hom, rw map_map, refl }
+
+@[simp, to_additive]
+lemma prod_map_div : (m.map $ λ i, f i / g i).prod = (m.map f).prod / (m.map g).prod :=
+m.prod_hom₂ (/) mul_div_comm' (div_one' _) _ _
+
+@[to_additive]
+lemma prod_map_zpow {n : ℤ} : (m.map $ λ i, f i ^ n).prod = (m.map f).prod ^ n :=
+by { convert (m.map f).prod_hom (zpow_group_hom _), rw map_map, refl }
 
 @[simp] lemma coe_inv_monoid_hom : (comm_group.inv_monoid_hom : α → α) = has_inv.inv := rfl
 
@@ -179,6 +206,22 @@ m.prod_hom comm_group.inv_monoid_hom
 
 end comm_group
 
+section comm_group_with_zero
+variables [comm_group_with_zero α] {m : multiset ι} {f g : ι → α}
+
+@[simp]
+lemma prod_map_inv₀ : (m.map $ λ i, (f i)⁻¹).prod = (m.map f).prod ⁻¹ :=
+by { convert (m.map f).prod_hom inv_monoid_with_zero_hom.to_monoid_hom, rw map_map, refl }
+
+@[simp]
+lemma prod_map_div₀ : (m.map $ λ i, f i / g i).prod = (m.map f).prod / (m.map g).prod :=
+m.prod_hom₂ (/) (λ _ _ _ _, (div_mul_div _ _ _ _).symm) (div_one _) _ _
+
+lemma prod_map_zpow₀ {n : ℤ} : prod (m.map $ λ i, f i ^ n) = (m.map f).prod ^ n :=
+by { convert (m.map f).prod_hom (zpow_group_hom₀ _), rw map_map, refl }
+
+end comm_group_with_zero
+
 section semiring
 variables [semiring α] {a : α} {s : multiset ι} {f : ι → α}
 

src/algebra/group/prod.lean

@@ -19,6 +19,13 @@ trivial `simp` lemmas, and define the following operations on `monoid_hom`s:
 * `f.coprod g : M × N →* P`: sends `(x, y)` to `f x * g y`;
 * `f.prod_map g : M × N → M' × N'`: `prod.map f g` as a `monoid_hom`,
   sends `(x, y)` to `(f x, g y)`.
+
+## Main declarations
+
+* `mul_mul_hom`/`mul_monoid_hom`/`mul_monoid_with_zero_hom`: Multiplication bundled as a
+  multiplicative/monoid/monoid with zero homomorphism.
+* `div_monoid_hom`/`div_monoid_with_zero_hom`: Division bundled as a monoid/monoid with zero
+  homomorphism.
 -/
 
 variables {A : Type*} {B : Type*} {G : Type*} {H : Type*} {M : Type*} {N : Type*} {P : Type*}
@@ -348,3 +355,43 @@ def embed_product (α : Type*) [monoid α] : αˣ →* α × αᵐᵒᵖ :=
   map_mul' := λ x y, by simp only [mul_inv_rev, op_mul, units.coe_mul, prod.mk_mul_mk] }
 
 end units
+
+/-! ### Multiplication and division as homomorphisms -/
+
+section bundled_mul_div
+variables {α : Type*}
+
+/-- Multiplication as a multiplicative homomorphism. -/
+@[to_additive "Addition as an additive homomorphism.", simps]
+def mul_mul_hom [comm_semigroup α] : mul_hom (α × α) α :=
+{ to_fun := λ a, a.1 * a.2,
+  map_mul' := λ a b, mul_mul_mul_comm _ _ _ _ }
+
+/-- Multiplication as a monoid homomorphism. -/
+@[to_additive "Addition as an additive monoid homomorphism.", simps]
+def mul_monoid_hom [comm_monoid α] : α × α →* α :=
+{ map_one' := mul_one _,
+  .. mul_mul_hom }
+
+/-- Multiplication as a multiplicative homomorphism with zero. -/
+@[simps]
+def mul_monoid_with_zero_hom [comm_monoid_with_zero α] : monoid_with_zero_hom (α × α) α :=
+{ map_zero' := mul_zero _,
+  .. mul_monoid_hom }
+
+/-- Division as a monoid homomorphism. -/
+@[to_additive "Subtraction as an additive monoid homomorphism.", simps]
+def div_monoid_hom [comm_group α] : α × α →* α :=
+{ to_fun := λ a, a.1 / a.2,
+  map_one' := div_one' _,
+  map_mul' := λ a b, mul_div_comm' _ _ _ _ }
+
+/-- Division as a multiplicative homomorphism with zero. -/
+@[simps]
+def div_monoid_with_zero_hom [comm_group_with_zero α] : monoid_with_zero_hom (α × α) α :=
+{ to_fun := λ a, a.1 / a.2,
+  map_zero' := zero_div _,
+  map_one' := div_one _,
+  map_mul' := λ a b, (div_mul_div _ _ _ _).symm }
+
+end bundled_mul_div

src/algebra/group_with_zero/basic.lean

@@ -1158,6 +1158,13 @@ end group_with_zero
 
 end monoid_with_zero_hom
 
+/-- Inversion on a commutative group with zero, considered as a monoid with zero homomorphism. -/
+def inv_monoid_with_zero_hom {G₀ : Type*} [comm_group_with_zero G₀] : monoid_with_zero_hom G₀ G₀ :=
+{ to_fun := has_inv.inv,
+  map_zero' := inv_zero,
+  map_one' := inv_one,
+  map_mul' := λ _ _, mul_inv₀ }
+
 @[simp] lemma monoid_hom.map_units_inv {M G₀ : Type*} [monoid M] [group_with_zero G₀]
   (f : M →* G₀) (u : Mˣ) : f ↑u⁻¹ = (f u)⁻¹ :=
 by rw [← units.coe_map, ← units.coe_map, ← units.coe_inv', monoid_hom.map_inv]

src/algebra/smul_with_zero.lean

@@ -6,6 +6,7 @@ Authors: Damiano Testa
 import algebra.group_power.basic
 import algebra.ring.opposite
 import group_theory.group_action.opposite
+import group_theory.group_action.prod
 
 /-!
 # Introduce `smul_with_zero`
@@ -27,6 +28,10 @@ Thus, the action is required to be compatible with
 We also add an `instance`:
 
 * any `monoid_with_zero` has a `mul_action_with_zero R R` acting on itself.
+
+## Main declarations
+
+* `smul_monoid_with_zero_hom`: Scalar multiplication bundled as a morphism of monoids with zero.
 -/
 
 variables {R R' M M' : Type*}
@@ -154,3 +159,11 @@ def mul_action_with_zero.comp_hom (f : monoid_with_zero_hom R' R) :
   .. smul_with_zero.comp_hom M f.to_zero_hom}
 
 end monoid_with_zero
+
+/-- Scalar multiplication as a monoid homomorphism with zero. -/
+@[simps]
+def smul_monoid_with_zero_hom {α β : Type*} [monoid_with_zero α] [mul_zero_one_class β]
+  [mul_action_with_zero α β] [is_scalar_tower α β β] [smul_comm_class α β β] :
+  monoid_with_zero_hom (α × β) β :=
+{ map_zero' := smul_zero' _ _,
+  .. smul_monoid_hom }

src/data/list/basic.lean

@@ -13,7 +13,7 @@ open function nat
 
 namespace list
 universes u v w x
-variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
+variables {ι : Type*} {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 
 attribute [inline] list.head
 
@@ -2139,6 +2139,16 @@ theorem foldr_hom (l : list γ) (f : α → β) (op : γ → α → α) (op' : 
   (h : ∀x a, f (op x a) = op' x (f a)) : foldr op' (f a) l = f (foldr op a l) :=
 by { revert a, induction l; intros; [refl, simp only [*, foldr]] }
 
+lemma foldl_hom₂ (l : list ι) (f : α → β → γ) (op₁ : α → ι → α) (op₂ : β → ι → β) (op₃ : γ → ι → γ)
+  (a : α) (b : β) (h : ∀ a b i, f (op₁ a i) (op₂ b i) = op₃ (f a b) i) :
+  foldl op₃ (f a b) l = f (foldl op₁ a l) (foldl op₂ b l) :=
+eq.symm $ by { revert a b, induction l; intros; [refl, simp only [*, foldl]] }
+
+lemma foldr_hom₂ (l : list ι) (f : α → β → γ) (op₁ : ι → α → α) (op₂ : ι → β → β) (op₃ : ι → γ → γ)
+  (a : α) (b : β) (h : ∀ a b i, f (op₁ i a) (op₂ i b) = op₃ i (f a b)) :
+  foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l) :=
+by { revert a, induction l; intros; [refl, simp only [*, foldr]] }
+
 lemma injective_foldl_comp {α : Type*} {l : list (α → α)} {f : α → α}
   (hl : ∀ f ∈ l, function.injective f) (hf : function.injective f):
   function.injective (@list.foldl (α → α) (α → α) function.comp f l) :=

src/data/list/big_operators.lean

@@ -12,7 +12,7 @@ This file provides basic results about `list.prod` and `list.sum`, which calcula
 sum of elements of a list. These are defined in [`data.list.defs`](./data/list/defs).
 -/
 
-variables {α β γ : Type*}
+variables {ι α β γ : Type*}
 
 namespace list
 section monoid
@@ -75,8 +75,8 @@ lemma prod_eq_foldr : l.prod = foldr (*) 1 l :=
 list.rec_on l rfl $ λ a l ihl, by rw [prod_cons, foldr_cons, ihl]
 
 @[to_additive]
-lemma prod_hom_rel {α β γ : Type*} [monoid β] [monoid γ] (l : list α) {r : β → γ → Prop}
-  {f : α → β} {g : α → γ} (h₁ : r 1 1) (h₂ : ∀⦃a b c⦄, r b c → r (f a * b) (g a * c)) :
+lemma prod_hom_rel [monoid β] (l : list ι) {r : α → β → Prop} {f : ι → α} {g : ι → β} (h₁ : r 1 1)
+  (h₂ : ∀ ⦃i a b⦄, r a b → r (f i * a) (g i * b)) :
   r (l.map f).prod (l.map g).prod :=
 list.rec_on l h₁ (λ a l hl, by simp only [map_cons, prod_cons, h₂ hl])
 
@@ -86,6 +86,17 @@ lemma prod_hom [monoid β] (l : list α) (f : α →* β) :
 by { simp only [prod, foldl_map, f.map_one.symm],
   exact l.foldl_hom _ _ _ 1 f.map_mul }
 
+@[to_additive]
+lemma prod_hom₂ [monoid β] [monoid γ] (l : list ι) (f : α → β → γ)
+  (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → α) (f₂ : ι → β) :
+  (l.map $ λ i, f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod :=
+begin
+  simp only [prod, foldl_map],
+  convert l.foldl_hom₂ (λ a b, f a b) _ _ _ _ _ (λ a b i, _),
+  { exact hf'.symm },
+  { exact hf _ _ _ _ }
+end
+
 @[to_additive]
 lemma prod_is_unit [monoid β] : Π {L : list β} (u : ∀ m ∈ L, is_unit m), is_unit L.prod
 | [] _ := by simp

src/group_theory/group_action/prod.lean

@@ -9,7 +9,13 @@ import group_theory.group_action.defs
 /-!
 # Prod instances for additive and multiplicative actions
 
-This file defines instances for binary product of additive and multiplicative actions
+This file defines instances for binary product of additive and multiplicative actions and provides
+scalar multiplication as a homomorphism from `α × β` to `β`.
+
+## Main declarations
+
+* `smul_mul_hom`/`smul_monoid_hom`: Scalar multiplication bundled as a multiplicative/monoid
+  homomorphism.
 -/
 
 variables {M N P α β : Type*}
@@ -77,3 +83,25 @@ instance {R M N : Type*} {r : monoid R} [monoid M] [monoid N]
   smul_one := λ a, mk.inj_iff.mpr ⟨smul_one _, smul_one _⟩ }
 
 end prod
+
+/-! ### Scalar multiplication as a homomorphism -/
+
+section bundled_smul
+
+/-- Scalar multiplication as a multiplicative homomorphism. -/
+@[simps]
+def smul_mul_hom [monoid α] [has_mul β] [mul_action α β] [is_scalar_tower α β β]
+  [smul_comm_class α β β] :
+  mul_hom (α × β) β :=
+{ to_fun := λ a, a.1 • a.2,
+  map_mul' := λ a b, (smul_mul_smul _ _ _ _).symm }
+
+/-- Scalar multiplication as a monoid homomorphism. -/
+@[simps]
+def smul_monoid_hom [monoid α] [mul_one_class β] [mul_action α β] [is_scalar_tower α β β]
+  [smul_comm_class α β β] :
+  α × β →* β :=
+{ map_one' := one_smul _ _,
+  .. smul_mul_hom }
+
+end bundled_smul