[Merged by Bors] - feat(algebra/module/submodule_bilinear): add submodule.map₂, generalizing submodule.has_mul

[eric-wieser]

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

---

[YaelDillies]

What about naming the file in a way that resembles more closely order.filter.n_ary?

[alreadydone]

Seems that submodule.has_scalar' can also be generalized to has_scalar (ideal R) (submodule A M) where algebra R A, and then used to define submodule.has_mul, of which ideal.has_mul is a special case. But then it wouldn't go through the submodule.map₂ API here. (Sorry, I was confused.)

[eric-wieser]

Certainly submodule.has_scalar' can be implemented in terms of this new map2; I'll try to do that.

[alreadydone]

This refactor extracted from my previous branch introduces the more flexible lemmas map₂_span_left/right which may be useful elsewhere.

Suggested change

	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}
	section
	variables R (f : M →ₗ[R] N →ₗ[R] P) (s : set M) (t : set N)
	theorem span_image2_span_left :
	span R (set.image2 (λ m, f m) (span R s) t) = span R (s.image2 (λ m, f m) t) :=
	span_eq_of_le _ (λ t ⟨m,n,hm,hn,h⟩, begin
	rw ← h, apply span_mono _ (apply_mem_span_image_of_mem_span (f.flip n) hm),
	exact λ t ⟨m,hm,h⟩, ⟨m,n,hm,hn,h⟩,
	end) $ span_mono $ set.image2_subset_right subset_span
	theorem span_image2_span_right :
	span R (s.image2 (λ m, f m) (span R t)) = span R (s.image2 (λ m, f m) t) :=
	span_eq_of_le _ (λ t ⟨m,n,hm,hn,h⟩, begin
	rw ← h, refine span_mono _ (apply_mem_span_image_of_mem_span (f m) hn),
	exact λ t ⟨n,hn,h⟩, ⟨m,n,hm,hn,h⟩,
	end) $ span_mono $ set.image2_subset_left subset_span
	theorem map₂_span_span : map₂ f (span R s) (span R t) = span R (s.image2 (λ m, f m) t) :=
	begin
	rw [← span_image2_span_left, ← span_image2_span_right], apply le_antisymm,
	{ rw map₂_le, exact λ m hm n hn, subset_span ⟨m,n,hm,hn,rfl⟩ },
	{ rw span_le, exact λ _ ⟨m,n,hm,hn,h⟩, h ▸ apply_mem_map₂ _ hm hn },
	end
	end

[eric-wieser]

I'd prefer to leave this PR as primarily moving things around, rather than refactoring any proofs. Those lemmas look good, but I'll let you add them in a follow-up.

[alreadydone]

Do you prefer me do it in #13733 or another PR?

[eric-wieser]

Probably a separate PR makes sense, especially if you don't use the new lemmas anywhere in your existing PR.

[eric-wieser]

Looking more closely, I don't really like the look of these lemma statements - do we have anything analogous for the normal unary image?

[alreadydone]

They're analogues of submodule.span_span

[alreadydone]

Hmm, so probably the two lemmas should go to that file (linear_algebra.span)

[alreadydone]

span_span doesn't have image in it, so it's not exactly an analogue. A closer analogue would be the following:

theorem span_image_span (f : M →ₗ[R] N) (s : set M) :
  span R (f '' (span R s)) = span R (f '' s) :=
by rw [← map_span, ← map_span, span_span]

Alternatively, by abusing defeq, we can get rid of one rewrite using map_span:

(congr_arg (λ x : submodule R N, span R (x : set N)) (map_span f s)).trans span_span

The two map_span transform the goal to map f (span R ↑(span R s)) = map f (span R s), which we can't do in the bilinear case, so there're some real difference here.

[alreadydone]

I now wonder: why is R made explicit here? Seems it can always be inferred from f?

[alreadydone]

I've created a branch with the two lemmas, ready to PR once this PR is merged; alternatively, I could merge it to #13733 if you approves.

[alreadydone]

They're analogues of submodule.span_span

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests