feat({data/finset,order/filter}/pointwise): Multiplicative action on pointwise monoids (#14214)

`mul_action`, `distrib_mul_action`, `mul_distrib_mul_action` instances for `finset` and `filter`. Also delete `set.smul_add_set` because `smul_add` proves it.

Author: YaelDillies

src/data/finset/n_ary.lean

@@ -93,7 +93,7 @@ lemma nonempty.of_image₂_right (h : (image₂ f s t).nonempty) : t.nonempty :=
 @[simp] lemma image₂_eq_empty_iff : image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅ :=
 by simp_rw [←not_nonempty_iff_eq_empty, image₂_nonempty_iff, not_and_distrib]
 
-@[simp] lemma image₂_singleton_left : image₂ f {a} t = t.image (f a) := ext $ λ x, by simp
+@[simp] lemma image₂_singleton_left : image₂ f {a} t = t.image (λ b, f a b) := ext $ λ x, by simp
 @[simp] lemma image₂_singleton_right : image₂ f s {b} = s.image (λ a, f a b) := ext $ λ x, by simp
 
 lemma image₂_singleton : image₂ f {a} {b} = {f a b} := by simp

src/data/finset/pointwise.lean

@@ -34,7 +34,7 @@ For finsets `s` and `t`:
 For `α` a semigroup/monoid, `finset α` is a semigroup/monoid.
 As an unfortunate side effect, this means that `n • s`, where `n : ℕ`, is ambiguous between
 pointwise scaling and repeated pointwise addition; the former has `(2 : ℕ) • {1, 2} = {2, 4}`, while
-the latter has `(2 : ℕ) • {1, 2} = {2, 3, 4}`.
+the latter has `(2 : ℕ) • {1, 2} = {2, 3, 4}`. See note [pointwise nat action].
 
 ## Implementation notes
 
@@ -603,7 +603,7 @@ subset_image₂
 
 end has_scalar
 
-/-! ### Finset addition/multiplication -/
+/-! ### Scalar subtraction of finsets -/
 
 section has_vsub
 variables [decidable_eq α] [has_vsub α β] {s s₁ s₂ t t₁ t₂ : finset β} {u : finset α} {a : α}
@@ -684,7 +684,7 @@ lemma mem_smul_finset {x : β} : x ∈ a • s ↔ ∃ y, y ∈ s ∧ a • y =
 by simp only [finset.smul_finset_def, and.assoc, mem_image, exists_prop, prod.exists, mem_product]
 
 @[simp, norm_cast, to_additive]
-lemma coe_smul_finset (s : finset β) : (↑(a • s) : set β) = a • s := coe_image
+lemma coe_smul_finset (a : α) (s : finset β) : (↑(a • s) : set β) = a • s := coe_image
 
 @[to_additive] lemma smul_finset_mem_smul_finset : b ∈ s → a • b ∈ a • s := mem_image_of_mem _
 @[to_additive] lemma smul_finset_card_le : (a • s).card ≤ s.card := card_image_le
@@ -750,5 +750,38 @@ instance is_central_scalar [has_scalar α β] [has_scalar αᵐᵒᵖ β] [is_ce
   is_central_scalar α (finset β) :=
 ⟨λ a s, coe_injective $ by simp only [coe_smul_finset, coe_smul, op_smul_eq_smul]⟩
 
+/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
+`finset α` on `finset β`. -/
+@[to_additive "An additive action of an additive monoid `α` on a type `β` gives an additive action
+of `finset α` on `finset β`"]
+protected def mul_action [decidable_eq α] [monoid α] [mul_action α β] :
+  mul_action (finset α) (finset β) :=
+{ mul_smul := λ _ _ _, image₂_assoc mul_smul,
+  one_smul := λ s, image₂_singleton_left.trans $ by simp_rw [one_smul, image_id'] }
+
+/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `finset β`.
+-/
+@[to_additive "An additive action of an additive monoid on a type `β` gives an additive action
+on `finset β`."]
+protected def mul_action_finset [monoid α] [mul_action α β] : mul_action α (finset β) :=
+coe_injective.mul_action _ coe_smul_finset
+
+localized "attribute [instance] finset.mul_action_finset finset.add_action_finset
+  finset.mul_action finset.add_action" in pointwise
+
+/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
+multiplicative action on `finset β`. -/
+protected def distrib_mul_action_finset [monoid α] [add_monoid β] [distrib_mul_action α β] :
+  distrib_mul_action α (finset β) :=
+function.injective.distrib_mul_action ⟨coe, coe_zero, coe_add⟩ coe_injective coe_smul_finset
+
+/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `set β`. -/
+protected def mul_distrib_mul_action_finset [monoid α] [monoid β] [mul_distrib_mul_action α β] :
+  mul_distrib_mul_action α (finset β) :=
+function.injective.mul_distrib_mul_action ⟨coe, coe_one, coe_mul⟩ coe_injective coe_smul_finset
+
+localized "attribute [instance] finset.distrib_mul_action_finset
+  finset.mul_distrib_mul_action_finset" in pointwise
+
 end instances
 end finset

src/data/set/pointwise.lean

@@ -30,7 +30,7 @@ For sets `s` and `t` and scalar `a`:
 For `α` a semigroup/monoid, `set α` is a semigroup/monoid.
 As an unfortunate side effect, this means that `n • s`, where `n : ℕ`, is ambiguous between
 pointwise scaling and repeated pointwise addition; the former has `(2 : ℕ) • {1, 2} = {2, 4}`, while
-the latter has `(2 : ℕ) • {1, 2} = {2, 3, 4}`.
+the latter has `(2 : ℕ) • {1, 2} = {2, 3, 4}`. See note [pointwise nat action].
 
 Appropriate definitions and results are also transported to the additive theory via `to_additive`.
 
@@ -1067,10 +1067,6 @@ end
 
 end smul_with_zero
 
-lemma smul_add_set [monoid α] [add_monoid β] [distrib_mul_action α β] (c : α) (s t : set β) :
-  c • (s + t) = c • s + c • t :=
-image_add (distrib_mul_action.to_add_monoid_hom β c).to_add_hom
-
 section group
 variables [group α] [mul_action α β] {A B : set β} {a : α} {x : β}
 

src/measure_theory/function/jacobian.lean

@@ -330,7 +330,7 @@ begin
         abel } },
     have : A '' (closed_ball 0 r) + closed_ball (f x) (ε * r)
       = {f x} + r • (A '' (closed_ball 0 1) + closed_ball 0 ε),
-      by rw [smul_add_set, ← add_assoc, add_comm ({f x}), add_assoc, smul_closed_ball _ _ εpos.le,
+      by rw [smul_add, ← add_assoc, add_comm ({f x}), add_assoc, smul_closed_ball _ _ εpos.le,
         smul_zero, singleton_add_closed_ball_zero, ← A.image_smul_set,
         smul_closed_ball _ _ zero_le_one, smul_zero, real.norm_eq_abs, abs_of_nonneg r0, mul_one,
         mul_comm],

src/order/filter/pointwise.lean

@@ -36,6 +36,10 @@ distribute over pointwise operations. For example,
 * `a +ᵥ f` (`filter.has_vadd_filter`): Translation, filter of all `a +ᵥ s` where `s ∈ f`.
 * `a • f` (`filter.has_scalar_filter`): Scaling, filter of all `a • s` where `s ∈ f`.
 
+For `α` a semigroup/monoid, `filter α` is a semigroup/monoid.
+As an unfortunate side effect, this means that `n • f`, where `n : ℕ`, is ambiguous between
+pointwise scaling and repeated pointwise addition. See note [pointwise nat action].
+
 ## Implementation notes
 
 We put all instances in the locale `pointwise`, so that these instances are not available by
@@ -564,9 +568,39 @@ instance is_central_scalar [has_scalar α β] [has_scalar αᵐᵒᵖ β] [is_ce
   is_central_scalar α (filter β) :=
 ⟨λ a f, congr_arg (λ m, map m f) $ by exact funext (λ _, op_smul_eq_smul _ _)⟩
 
-@[to_additive]
-instance [monoid α] [mul_action α β] : mul_action (filter α) (filter β) :=
-{ one_smul := λ f, by simp only [←pure_one, ←map₂_smul, map₂_pure_left, one_smul, map_id'],
+/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
+`filter α` on `filter β`. -/
+@[to_additive "An additive action of an additive monoid `α` on a type `β` gives an additive action
+of `filter α` on `filter β`"]
+protected def mul_action [monoid α] [mul_action α β] : mul_action (filter α) (filter β) :=
+{ one_smul := λ f, map₂_pure_left.trans $ by simp_rw [one_smul, map_id'],
   mul_smul := λ f g h, map₂_assoc mul_smul }
 
+/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `filter β`.
+-/
+@[to_additive "An additive action of an additive monoid on a type `β` gives an additive action on
+`filter β`."]
+protected def mul_action_filter [monoid α] [mul_action α β] : mul_action α (filter β) :=
+{ mul_smul := λ a b f, by simp only [←map_smul, map_map, function.comp, ←mul_smul],
+  one_smul := λ f, by simp only [←map_smul, one_smul, map_id'] }
+
+localized "attribute [instance] filter.mul_action filter.add_action filter.mul_action_filter
+  filter.add_action_filter" in pointwise
+
+/-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
+multiplicative action on `filter β`. -/
+protected def distrib_mul_action_filter [monoid α] [add_monoid β] [distrib_mul_action α β] :
+  distrib_mul_action α (filter β) :=
+{ smul_add := λ _ _ _, map_map₂_distrib $ smul_add _,
+  smul_zero := λ _, (map_pure _ _).trans $ by rw [smul_zero, pure_zero] }
+
+/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `set β`. -/
+protected def mul_distrib_mul_action_filter [monoid α] [monoid β] [mul_distrib_mul_action α β] :
+  mul_distrib_mul_action α (set β) :=
+{ smul_mul := λ _ _ _, image_image2_distrib $ smul_mul' _,
+  smul_one := λ _, image_singleton.trans $ by rw [smul_one, singleton_one] }
+
+localized "attribute [instance] filter.distrib_mul_action_filter
+  filter.mul_distrib_mul_action_filter" in pointwise
+
 end filter