feat(algebra/{pointwise,algebra/operations}): add supr_mul and `mul…

…_supr` (#8923)

Requested by @eric-wieser  on Zulip, https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/submodule.2Esupr_mul/near/250122435
and a couple of helper lemmas.

Co-authored-by: Eric Wieser wieser.eric@gmail.com





Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/algebra/operations.lean

@@ -27,13 +27,14 @@ It is proved that `submodule R A` is a semiring, and also an algebra over `set A
 multiplication of submodules, division of subodules, submodule semiring
 -/
 
-universes u v
+universes uι u v
 
 open algebra set
 open_locale pointwise
 
 namespace submodule
 
+variables {ι : Sort uι}
 variables {R : Type u} [comm_semiring R]
 
 section ring
@@ -186,6 +187,23 @@ end
 
 end decidable_eq
 
+lemma mul_eq_span_mul_set (s t : submodule R A) : s * t = span R ((s : set A) * (t : set A)) :=
+by rw [← span_mul_span, span_eq, span_eq]
+
+lemma supr_mul (s : ι → submodule R A) (t : submodule R A) : (⨆ i, s i) * t = ⨆ i, s i * t :=
+begin
+  suffices : (⨆ i, span R (s i : set A)) * span R t = (⨆ i, span R (s i) * span R t),
+  { simpa only [span_eq] using this },
+  simp_rw [span_mul_span, ← span_Union, span_mul_span, set.Union_mul],
+end
+
+lemma mul_supr (t : submodule R A) (s : ι → submodule R A) : t * (⨆ i, s i) = ⨆ i, t * s i :=
+begin
+  suffices : span R (t : set A) * (⨆ i, span R (s i)) = (⨆ i, span R t * span R (s i)),
+  { simpa only [span_eq] using this },
+  simp_rw [span_mul_span, ← span_Union, span_mul_span, set.mul_Union],
+end
+
 lemma mem_span_mul_finite_of_mem_mul {P Q : submodule R A} {x : A} (hx : x ∈ P * Q) :
   ∃ (T T' : finset A), (T : set A) ⊆ P ∧ (T' : set A) ⊆ Q ∧ x ∈ span R (T * T' : set A) :=
 submodule.mem_span_mul_finite_of_mem_span_mul

src/algebra/pointwise.lean

@@ -238,6 +238,16 @@ Union_image_left _
 lemma Union_mul_right_image [has_mul α] : (⋃ a ∈ t, (λ x, x * a) '' s) = s * t :=
 Union_image_right _
 
+@[to_additive]
+lemma Union_mul {ι : Sort*} [has_mul α] (s : ι → set α) (t : set α) :
+  (⋃ i, s i) * t = ⋃ i, (s i * t) :=
+image2_Union_left _ _ _
+
+@[to_additive]
+lemma mul_Union {ι : Sort*} [has_mul α] (t : set α) (s : ι → set α) :
+  t * (⋃ i, s i) = ⋃ i, (t * s i) :=
+image2_Union_right _ _ _
+
 @[simp, to_additive]
 lemma univ_mul_univ [monoid α] : (univ : set α) * univ = univ :=
 begin