feat(group_theory/submonoid/pointwise): add pointwise multiplication …

…to `add_submonoid`s (#11522)

src/group_theory/submonoid/pointwise.lean

@@ -22,6 +22,9 @@ which matches the action of `mul_action_set`.
 
 These are all available in the `pointwise` locale.
 
+Additionally, it provides `add_submonoid.has_mul`, which is available globally to match
+`submodule.has_mul`.
+
 ## Implementation notes
 
 Most of the lemmas in this file are direct copies of lemmas from `algebra/pointwise.lean`.
@@ -31,7 +34,8 @@ on `set`s.
 
 -/
 
-variables {α : Type*} {M : Type*} {G : Type*} {A : Type*} [monoid M] [add_monoid A]
+variables {α : Type*} {G : Type*} {M : Type*} {R : Type*} {A : Type*}
+variables [monoid M] [add_monoid A]
 
 namespace submonoid
 
@@ -300,3 +304,70 @@ end group_with_zero
 open_locale pointwise
 
 end add_submonoid
+
+/-! ### Elementwise multiplication of two additive submonoids
+
+These definitions are a cut-down versions of the ones around `submodule.has_mul`, as that API is
+usually more useful. -/
+namespace add_submonoid
+
+variables [non_unital_non_assoc_semiring R]
+
+/-- Multiplication of additive submonoids of a semiring R. The additive submonoid `S * T` is the
+smallest R-submodule of `R` containing the elements `s * t` for `s ∈ S` and `t ∈ T`. -/
+instance : has_mul (add_submonoid R) :=
+⟨λ M N, ⨆ s : M, N.map $ add_monoid_hom.mul s.1⟩
+
+theorem mul_mem_mul {M N : add_submonoid R} {m n : R} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N :=
+(le_supr _ ⟨m, hm⟩ : _ ≤ M * N) ⟨n, hn, rfl⟩
+
+theorem mul_le {M N P : add_submonoid R} : M * N ≤ P ↔ ∀ (m ∈ M) (n ∈ N), m * n ∈ P :=
+⟨λ H m hm n hn, H $ mul_mem_mul hm hn,
+λ H, supr_le $ λ ⟨m, hm⟩, map_le_iff_le_comap.2 $ λ n hn, H m hm n hn⟩
+
+@[elab_as_eliminator] protected theorem mul_induction_on
+  {M N : add_submonoid R}
+  {C : R → Prop} {r : R} (hr : r ∈ M * N)
+  (hm : ∀ (m ∈ M) (n ∈ N), C (m * n))
+  (ha : ∀ x y, C x → C y → C (x + y)) : C r :=
+(@mul_le _ _ _ _ ⟨C, by simpa only [zero_mul] using hm _ (zero_mem _) _ (zero_mem _), ha⟩).2 hm hr
+
+open_locale pointwise
+
+variables R
+-- this proof is copied directly from `submodule.span_mul_span`
+theorem closure_mul_closure (S T : set R) : closure S * closure T = closure (S * T) :=
+begin
+  apply le_antisymm,
+  { rw mul_le, intros a ha b hb,
+    apply closure_induction ha,
+    work_on_goal 0 { intros, apply closure_induction hb,
+      work_on_goal 0 { intros, exact subset_closure ⟨_, _, ‹_›, ‹_›, rfl⟩ } },
+    all_goals { intros, simp only [mul_zero, zero_mul, zero_mem,
+        left_distrib, right_distrib, mul_smul_comm, smul_mul_assoc],
+      try {apply add_mem _ _ _}, try {apply smul_mem _ _ _} }, assumption' },
+  { rw closure_le, rintros _ ⟨a, b, ha, hb, rfl⟩,
+    exact mul_mem_mul (subset_closure ha) (subset_closure hb) }
+end
+variables {R}
+
+@[simp] theorem mul_bot (S : add_submonoid R) : S * ⊥ = ⊥ :=
+eq_bot_iff.2 $ mul_le.2 $ λ m hm n hn, by rw [add_submonoid.mem_bot] at hn ⊢; rw [hn, mul_zero]
+
+@[simp] theorem bot_mul (S : add_submonoid R) : ⊥ * S = ⊥ :=
+eq_bot_iff.2 $ mul_le.2 $ λ m hm n hn, by rw [add_submonoid.mem_bot] at hm ⊢; rw [hm, zero_mul]
+
+@[mono] theorem mul_le_mul {M N P Q : add_submonoid R} (hmp : M ≤ P) (hnq : N ≤ Q) :
+  M * N ≤ P * Q :=
+mul_le.2 $ λ m hm n hn, mul_mem_mul (hmp hm) (hnq hn)
+
+theorem mul_le_mul_left {M N P : add_submonoid R} (h : M ≤ N) : M * P ≤ N * P :=
+mul_le_mul h (le_refl P)
+
+theorem mul_le_mul_right {M N P : add_submonoid R} (h : N ≤ P) : M * N ≤ M * P :=
+mul_le_mul (le_refl M) h
+
+lemma mul_subset_mul {M N : add_submonoid R} : (↑M : set R) * (↑N : set R) ⊆ (↑(M * N) : set R) :=
+by { rintros _ ⟨i, j, hi, hj, rfl⟩, exact mul_mem_mul hi hj }
+
+end add_submonoid