feat(algebra/module/submodule_bilinear): add submodule.map₂, genera…

…lizing `submodule.has_mul` (#13709)

The motivation here is to be able to talk about combinations of submodules under other bilinear maps, such as the tensor product. This unifies the definitions of and lemmas about `submodule.has_mul` and `submodule.has_scalar'`.

The lemmas about `submodule.map₂` are copied verbatim from those for `mul`, and then adjusted slightly replacing `mul_zero` with `linear_map.map_zero` etc. I've then replaced the lemmas about `smul` with the `map₂` proofs where possible.

The lemmas about finiteness weren't possible to copy this way, as the proofs about `finset` multiplication are not generalized in a similar way. Someone else can copy these in a future PR.

This also adds `set.image2_eq_Union` to match `set.image_eq_Union`, and removes `submodule.union_eq_smul_set` which is neither about submodules nor about `union`, and instead is really just a copy of `set.image_eq_Union`

src/algebra/algebra/operations.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 import algebra.algebra.bilinear
 import algebra.module.submodule_pointwise
+import algebra.module.submodule_bilinear
 import algebra.module.opposites
 import data.finset.pointwise
 
@@ -89,22 +90,19 @@ by rw [←comap_equiv_eq_map_symm, comap_op_one]
   comap (↑(op_linear_equiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (1 : submodule R A) = 1 :=
 by rw [←map_equiv_eq_comap_symm, map_op_one]
 
+
 /-- Multiplication of sub-R-modules of an R-algebra A. The submodule `M * N` is the
 smallest R-submodule of `A` containing the elements `m * n` for `m ∈ M` and `n ∈ N`. -/
-instance : has_mul (submodule R A) :=
-⟨λ M N, ⨆ s : M, N.map $ algebra.lmul R A s.1⟩
+instance : has_mul (submodule R A) := ⟨submodule.map₂ (algebra.lmul R A).to_linear_map⟩
 
-theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N :=
-(le_supr _ ⟨m, hm⟩ : _ ≤ M * N) ⟨n, hn, rfl⟩
+theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N := apply_mem_map₂ _ hm hn
 
-theorem mul_le : 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⟩
+theorem mul_le : M * N ≤ P ↔ ∀ (m ∈ M) (n ∈ N), m * n ∈ P := map₂_le
 
 lemma mul_to_add_submonoid : (M * N).to_add_submonoid = M.to_add_submonoid * N.to_add_submonoid :=
 begin
   dsimp [has_mul.mul],
-  simp_rw [←algebra.lmul_left_to_add_monoid_hom R, algebra.lmul_left, ←map_to_add_submonoid],
+  simp_rw [←algebra.lmul_left_to_add_monoid_hom R, algebra.lmul_left, ←map_to_add_submonoid, map₂],
   rw supr_to_add_submonoid,
   refl,
 end
@@ -130,20 +128,7 @@ begin
 end
 
 variables R
-theorem span_mul_span : span R S * span R T = span R (S * T) :=
-begin
-  apply le_antisymm,
-  { rw mul_le, intros a ha b hb,
-    apply span_induction ha,
-    work_on_goal 1 { intros, apply span_induction hb,
-      work_on_goal 1 { intros, exact subset_span ⟨_, _, ‹_›, ‹_›, rfl⟩ } },
-    all_goals { intros, simp only [mul_zero, zero_mul, zero_mem,
-        left_distrib, right_distrib, mul_smul_comm, smul_mul_assoc],
-      solve_by_elim [add_mem _ _, zero_mem _, smul_mem _ _ _]
-        { max_depth := 4, discharger := tactic.interactive.apply_instance } } },
-  { rw span_le, rintros _ ⟨a, b, ha, hb, rfl⟩,
-    exact mul_mem_mul (subset_span ha) (subset_span hb) }
-end
+theorem span_mul_span : span R S * span R T = span R (S * T) := map₂_span_span _ _ _ _
 variables {R}
 
 
@@ -158,11 +143,9 @@ le_antisymm (mul_le.2 $ λ mn hmn p hp,
   mul_le.2 $ λ n hn p hp, show m * (n * p) ∈ M * N * P, from
   mul_assoc m n p ▸ mul_mem_mul (mul_mem_mul hm hn) hp)
 
-@[simp] theorem mul_bot : M * ⊥ = ⊥ :=
-eq_bot_iff.2 $ mul_le.2 $ λ m hm n hn, by rw [submodule.mem_bot] at hn ⊢; rw [hn, mul_zero]
+@[simp] theorem mul_bot : M * ⊥ = ⊥ := map₂_bot_right _ _
 
-@[simp] theorem bot_mul : ⊥ * M = ⊥ :=
-eq_bot_iff.2 $ mul_le.2 $ λ m hm n hn, by rw [submodule.mem_bot] at hm ⊢; rw [hm, zero_mul]
+@[simp] theorem bot_mul : ⊥ * M = ⊥ := map₂_bot_left _ _
 
 @[simp] protected theorem one_mul : (1 : submodule R A) * M = M :=
 by { conv_lhs { rw [one_eq_span, ← span_eq M] }, erw [span_mul_span, one_mul, span_eq] }
@@ -172,28 +155,19 @@ by { conv_lhs { rw [one_eq_span, ← span_eq M] }, erw [span_mul_span, mul_one,
 
 variables {M N P Q}
 
-@[mono] theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q :=
-mul_le.2 $ λ m hm n hn, mul_mem_mul (hmp hm) (hnq hn)
+@[mono] theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := map₂_le_map₂ hmp hnq
 
-theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P :=
-mul_le_mul h (le_refl P)
+theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P := map₂_le_map₂_left h
 
-theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P :=
-mul_le_mul (le_refl M) h
+theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P := map₂_le_map₂_right h
 
 variables (M N P)
-theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P :=
-le_antisymm (mul_le.2 $ λ m hm np hnp, let ⟨n, hn, p, hp, hnp⟩ := mem_sup.1 hnp in
-  mem_sup.2 ⟨_, mul_mem_mul hm hn, _, mul_mem_mul hm hp, hnp ▸ (mul_add m n p).symm⟩)
-(sup_le (mul_le_mul_right le_sup_left) (mul_le_mul_right le_sup_right))
+theorem mul_sup : M * (N ⊔ P) = M * N ⊔ M * P := map₂_sup_right _ _ _ _
 
-theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P :=
-le_antisymm (mul_le.2 $ λ mn hmn p hp, let ⟨m, hm, n, hn, hmn⟩ := mem_sup.1 hmn in
-  mem_sup.2 ⟨_, mul_mem_mul hm hp, _, mul_mem_mul hn hp, hmn ▸ (add_mul m n p).symm⟩)
-(sup_le (mul_le_mul_left le_sup_left) (mul_le_mul_left le_sup_right))
+theorem sup_mul : (M ⊔ N) * P = M * P ⊔ N * P := map₂_sup_left _ _ _ _
 
 lemma mul_subset_mul : (↑M : set A) * (↑N : set A) ⊆ (↑(M * N) : set A) :=
-by { rintros _ ⟨i, j, hi, hj, rfl⟩, exact mul_mem_mul hi hj }
+image2_subset_map₂ (algebra.lmul R A).to_linear_map M N
 
 protected lemma map_mul {A'} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :
   map f.to_linear_map (M * N) = map f.to_linear_map M * map f.to_linear_map N :=
@@ -305,21 +279,13 @@ 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]
+map₂_eq_span_image2 _ s t
 
 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
+map₂_supr_left _ s t
 
 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
+map₂_supr_right _ t s
 
 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) :=

src/algebra/module/submodule_bilinear.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2019 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Eric Wieser
+-/
+import linear_algebra.span
+import linear_algebra.bilinear_map
+
+/-!
+# Images of pairs of submodules under bilinear maps
+
+This file provides `submodule.map₂`, which is later used to implement `submodule.has_mul`.
+
+## Main results
+
+* `submodule.map₂_eq_span_image2`: the image of two submodules under a bilinear map is the span of
+  their `set.image2`.
+
+## Notes
+
+This file is quite similar to the n-ary section of `data.set.basic` and to `order.filter.n_ary`.
+Please keep them in sync.
+-/
+
+universes uι u v
+
+open set
+open_locale big_operators
+open_locale pointwise
+
+namespace submodule
+
+variables {ι : Sort uι} {R M N P : Type*}
+variables [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
+variables [module R M] [module R N] [module R P]
+
+/-- Map a pair of submodules under a bilinear map.
+
+This is the submodule version of `set.image2`.  -/
+def map₂ (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) (q : submodule R N) : submodule R P :=
+⨆ s : p, q.map $ f s
+
+theorem apply_mem_map₂ (f : M →ₗ[R] N →ₗ[R] P) {m : M} {n : N}
+  {p : submodule R M} {q : submodule R N} (hm : m ∈ p) (hn : n ∈ q) : f m n ∈ map₂ f p q :=
+(le_supr _ ⟨m, hm⟩ : _ ≤ map₂ f p q) ⟨n, hn, rfl⟩
+
+theorem map₂_le {f : M →ₗ[R] N →ₗ[R] P}
+  {p : submodule R M} {q : submodule R N} {r : submodule R P} :
+  map₂ f p q ≤ r ↔ ∀ (m ∈ p) (n ∈ q), f m n ∈ r :=
+⟨λ H m hm n hn, H $ apply_mem_map₂ _ hm hn,
+ λ H, supr_le $ λ ⟨m, hm⟩, map_le_iff_le_comap.2 $ λ n hn, H m hm n hn⟩
+
+variables R
+theorem map₂_span_span (f : M →ₗ[R] N →ₗ[R] P) (s : set M) (t : set N) :
+  map₂ f (span R s) (span R t) = span R (set.image2 (λ m n, f m n) s t) :=
+begin
+  apply le_antisymm,
+  { rw map₂_le, intros a ha b hb,
+    apply span_induction ha,
+    work_on_goal 1 { intros, apply span_induction hb,
+      work_on_goal 1 { intros, exact subset_span ⟨_, _, ‹_›, ‹_›, rfl⟩ } },
+    all_goals {
+      intros,
+      simp only [linear_map.map_zero, linear_map.zero_apply, zero_mem,
+        linear_map.map_add, linear_map.add_apply, linear_map.map_smul, linear_map.smul_apply] },
+    all_goals {
+      solve_by_elim [add_mem _ _, zero_mem _, smul_mem _ _ _]
+        { max_depth := 4, discharger := tactic.interactive.apply_instance } } },
+  { rw span_le, rintros _ ⟨a, b, ha, hb, rfl⟩,
+    exact apply_mem_map₂ _ (subset_span ha) (subset_span hb) }
+end
+variables {R}
+
+@[simp] theorem map₂_bot_right (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) : map₂ f p ⊥ = ⊥ :=
+eq_bot_iff.2 $ map₂_le.2 $ λ m hm n hn,
+  by { rw [submodule.mem_bot] at hn ⊢, rw [hn, linear_map.map_zero] }
+
+@[simp] theorem map₂_bot_left (f : M →ₗ[R] N →ₗ[R] P) (q : submodule R N) : map₂ f ⊥ q = ⊥ :=
+eq_bot_iff.2 $ map₂_le.2 $ λ m hm n hn,
+  by { rw [submodule.mem_bot] at hm ⊢, rw [hm, linear_map.map_zero₂] }
+
+@[mono] theorem map₂_le_map₂ {f : M →ₗ[R] N →ₗ[R] P}
+  {p₁ p₂ : submodule R M} {q₁ q₂ : submodule R N} (hp : p₁ ≤ p₂) (hq : q₁ ≤ q₂) :
+  map₂ f p₁ q₁ ≤ map₂ f p₂ q₂ :=
+map₂_le.2 $ λ m hm n hn, apply_mem_map₂ _ (hp hm) (hq hn)
+
+theorem map₂_le_map₂_left {f : M →ₗ[R] N →ₗ[R] P}
+  {p₁ p₂ : submodule R M} {q : submodule R N} (h : p₁ ≤ p₂) : map₂ f p₁ q ≤ map₂ f p₂ q :=
+map₂_le_map₂ h (le_refl q)
+
+theorem map₂_le_map₂_right {f : M →ₗ[R] N →ₗ[R] P}
+  {p : submodule R M} {q₁ q₂ : submodule R N} (h : q₁ ≤ q₂): map₂ f p q₁ ≤ map₂ f p q₂ :=
+map₂_le_map₂ (le_refl p) h
+
+theorem map₂_sup_right (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) (q₁ q₂ : submodule R N) :
+  map₂ f p (q₁ ⊔ q₂) = map₂ f p q₁ ⊔ map₂ f p q₂ :=
+le_antisymm (map₂_le.2 $ λ m hm np hnp, let ⟨n, hn, p, hp, hnp⟩ := mem_sup.1 hnp in
+  mem_sup.2 ⟨_, apply_mem_map₂ _ hm hn, _, apply_mem_map₂ _ hm hp, hnp ▸ (map_add _ _ _).symm⟩)
+(sup_le (map₂_le_map₂_right le_sup_left) (map₂_le_map₂_right le_sup_right))
+
+theorem map₂_sup_left (f : M →ₗ[R] N →ₗ[R] P) (p₁ p₂ : submodule R M) (q : submodule R N) :
+  map₂ f (p₁ ⊔ p₂) q = map₂ f p₁ q ⊔ map₂ f p₂ q :=
+le_antisymm (map₂_le.2 $ λ mn hmn p hp, let ⟨m, hm, n, hn, hmn⟩ := mem_sup.1 hmn in
+  mem_sup.2 ⟨_, apply_mem_map₂ _ hm hp, _, apply_mem_map₂ _ hn hp,
+    hmn ▸ (linear_map.map_add₂ _ _ _ _).symm⟩)
+(sup_le (map₂_le_map₂_left le_sup_left) (map₂_le_map₂_left le_sup_right))
+
+lemma image2_subset_map₂ (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) (q : submodule R N) :
+  set.image2 (λ m n, f m n) (↑p : set M) (↑q : set N) ⊆ (↑(map₂ f p q) : set P) :=
+by { rintros _ ⟨i, j, hi, hj, rfl⟩, exact apply_mem_map₂ _ hi hj }
+
+lemma map₂_eq_span_image2 (f : M →ₗ[R] N →ₗ[R] P) (p : submodule R M) (q : submodule R N) :
+  map₂ f p q = span R (set.image2 (λ m n, f m n) (p : set M) (q : set N)) :=
+by rw [← map₂_span_span, span_eq, span_eq]
+
+lemma map₂_supr_left (f : M →ₗ[R] N →ₗ[R] P) (s : ι → submodule R M) (t : submodule R N) :
+  map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t :=
+begin
+  suffices :
+    map₂ f (⨆ i, span R (s i : set M)) (span R t) = (⨆ i, map₂ f (span R (s i)) (span R t)),
+  { simpa only [span_eq] using this },
+  simp_rw [map₂_span_span, ← span_Union, map₂_span_span, set.image2_Union_left],
+end
+
+lemma map₂_supr_right (f : M →ₗ[R] N →ₗ[R] P) (s : submodule R M) (t : ι → submodule R N) :
+  map₂ f s (⨆ i, t i) = ⨆ i, map₂ f s (t i) :=
+begin
+  suffices :
+    map₂ f (span R s) (⨆ i, span R (t i : set N)) = (⨆ i, map₂ f (span R s) (span R (t i))),
+  { simpa only [span_eq] using this },
+  simp_rw [map₂_span_span, ← span_Union, map₂_span_span, set.image2_Union_right],
+end
+
+end submodule

src/data/set/lattice.lean

@@ -1320,6 +1320,10 @@ lemma image2_Inter₂_subset_right (s : set α) (t : Π i, κ i → set β) :
   image2 f s (⋂ i j, t i j) ⊆ ⋂ i j, image2 f s (t i j) :=
 by { simp_rw [image2_subset_iff, mem_Inter], exact λ x hx y hy i j, mem_image2_of_mem hx (hy _ _) }
 
+/-- The `set.image2` version of `set.image_eq_Union` -/
+lemma image2_eq_Union (s : set α) (t : set β) : image2 f s t = ⋃ (i ∈ s) (j ∈ t), {f i j} :=
+by simp_rw [←image_eq_Union, Union_image_left]
+
 end image2
 
 section seq

src/ring_theory/henselian.lean

@@ -228,7 +228,7 @@ instance is_adic_complete.henselian_ring
     -- we are now in the position to show that `c : ℕ → R` is a Cauchy sequence
     have aux : ∀ m n, m ≤ n → c m ≡ c n [SMOD (I ^ m • ⊤ : ideal R)],
     { intros m n hmn,
-      rw [← ideal.one_eq_top, algebra.id.smul_eq_mul, mul_one],
+      rw [← ideal.one_eq_top, ideal.smul_eq_mul, mul_one],
       obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le hmn, clear hmn,
       induction k with k ih, { rw add_zero, },
       rw [nat.succ_eq_add_one, ← add_assoc, hc, ← add_zero (c m), sub_eq_add_neg],
@@ -242,13 +242,13 @@ instance is_adic_complete.henselian_ring
     { show f.is_root a,
       suffices : ∀ n, f.eval a ≡ 0 [SMOD (I ^ n • ⊤ : ideal R)], { from is_Hausdorff.haus' _ this },
       intro n, specialize ha n,
-      rw [← ideal.one_eq_top, algebra.id.smul_eq_mul, mul_one] at ha ⊢,
+      rw [← ideal.one_eq_top, ideal.smul_eq_mul, mul_one] at ha ⊢,
       refine (ha.symm.eval f).trans _,
       rw [smodeq.zero],
       exact ideal.pow_le_pow le_self_add (hfcI _), },
     { show a - a₀ ∈ I,
       specialize ha 1,
-      rw [hc, pow_one, ← ideal.one_eq_top, algebra.id.smul_eq_mul, mul_one, sub_eq_add_neg] at ha,
+      rw [hc, pow_one, ← ideal.one_eq_top, ideal.smul_eq_mul, mul_one, sub_eq_add_neg] at ha,
       rw [← smodeq.sub_mem, ← add_zero a₀],
       refine ha.symm.trans (smodeq.refl.add _),
       rw [smodeq.zero, ideal.neg_mem_iff],