feat(linear_algebra/basic): range of linear_map.prod (#2785)

Also make `ker_prod` a `simp` lemma.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/linear_algebra/basic.lean

@@ -1142,10 +1142,36 @@ lemma span_inl_union_inr {s : set M} {t : set M₂} :
   span R (prod.inl '' s ∪ prod.inr '' t) = (span R s).prod (span R t) :=
 by rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]; refl
 
-lemma ker_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
+@[simp] lemma ker_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
   ker (prod f g) = ker f ⊓ ker g :=
 by rw [ker, ← prod_bot, comap_prod_prod]; refl
 
+lemma range_prod_le (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) :
+  range (prod f g) ≤ (range f).prod (range g) :=
+begin
+  simp only [le_def', prod_apply, mem_range, mem_coe, mem_prod, exists_imp_distrib],
+  rintro _ x rfl,
+  exact ⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩
+end
+
+/-- If the union of the kernels `ker f` and `ker g` spans the domain, then the range of
+`prod f g` is equal to the product of `range f` and `range g`. -/
+lemma range_prod_eq {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : ker f ⊔ ker g = ⊤) :
+  range (prod f g) = (range f).prod (range g) :=
+begin
+  refine le_antisymm (f.range_prod_le g) _,
+  simp only [le_def', prod_apply, mem_range, mem_coe, mem_prod, exists_imp_distrib, and_imp,
+    prod.forall],
+  rintros _ _ x rfl y rfl,
+  simp only [prod.mk.inj_iff, ← sub_mem_ker_iff],
+  have : y - x ∈ ker f ⊔ ker g, { simp only [h, mem_top] },
+  rcases mem_sup.1 this with ⟨x', hx', y', hy', H⟩,
+  refine ⟨x' + x, _, _⟩,
+  { rwa add_sub_cancel },
+  { rwa [← eq_sub_iff_add_eq.1 H, add_sub_add_right_eq_sub, ← neg_mem_iff, neg_sub,
+      add_sub_cancel'] }
+end
+
 end linear_map
 
 lemma submodule.sup_eq_range [ring R] [add_comm_group M] [module R M] (p q : submodule R M) :

src/topology/algebra/module.lean

@@ -365,12 +365,24 @@ continuous_iff_is_closed.1 f.cont _ is_closed_singleton
 
 @[simp] lemma apply_ker (x : f.ker) : f x = 0 := mem_ker.1 x.2
 
+@[simp] lemma ker_prod (f : M →L[R] M₂) (g : M →L[R] M₃) :
+  ker (f.prod g) = ker f ⊓ ker g :=
+linear_map.ker_prod f g
+
 /-- Range of a continuous linear map. -/
 def range (f : M →L[R] M₂) : submodule R M₂ := (f : M →ₗ[R] M₂).range
 
 lemma range_coe : (f.range : set M₂) = set.range f := linear_map.range_coe _
 lemma mem_range {f : M →L[R] M₂} {y} : y ∈ f.range ↔ ∃ x, f x = y := linear_map.mem_range
 
+lemma range_prod_le (f : M →L[R] M₂) (g : M →L[R] M₃) :
+  range (f.prod g) ≤ (range f).prod (range g) :=
+(f : M →ₗ[R] M₂).range_prod_le g
+
+lemma range_prod_eq {f : M →L[R] M₂} {g : M →L[R] M₃} (h : ker f ⊔ ker g = ⊤) :
+  range (f.prod g) = (range f).prod (range g) :=
+linear_map.range_prod_eq h
+
 /-- Restrict codomain of a continuous linear map. -/
 def cod_restrict (f : M →L[R] M₂) (p : submodule R M₂) (h : ∀ x, f x ∈ p) :
   M →L[R] p :=
@@ -731,6 +743,12 @@ by { ext x, refl }
 theorem symm_symm_apply (e : M ≃L[R] M₂) (x : M) : e.symm.symm x = e x :=
 rfl
 
+lemma symm_apply_eq (e : M ≃L[R] M₂) {x y} : e.symm x = y ↔ x = e y :=
+e.to_linear_equiv.symm_apply_eq
+
+lemma eq_symm_apply (e : M ≃L[R] M₂) {x y} : y = e.symm x ↔ e y = x :=
+e.to_linear_equiv.eq_symm_apply
+
 /-- Create a `continuous_linear_equiv` from two `continuous_linear_map`s that are
 inverse of each other. -/
 def equiv_of_inverse (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h₁ : function.left_inverse f₂ f₁)