feat(analysis/normed_space/banach): a range with closed complement is…

… itself closed (#6972)

If the range of a continuous linear map has a closed complement, then it is itself closed. For instance, the range can not be a dense hyperplane. We prove it when, additionally, the map has trivial kernel. The general case will follow from this particular case once we have quotients of normed spaces, which are currently only in Lean Liquid.

Along the way, we fill several small gaps in the API of continuous linear maps.

src/analysis/normed_space/banach.lean

@@ -325,3 +325,29 @@ noncomputable def of_bijective (f : E →L[𝕜] F) (hinj : f.ker = ⊥) (hsurj
 (of_bijective f hinj hsurj).apply_symm_apply y
 
 end continuous_linear_equiv
+
+namespace continuous_linear_map
+
+/- TODO: remove the assumption `f.ker = ⊥` in the next lemma, by using the map induced by `f` on
+`E / f.ker`, once we have quotient normed spaces. -/
+lemma closed_complemented_range_of_is_compl_of_ker_eq_bot (f : E →L[𝕜] F) (G : submodule 𝕜 F)
+  (h : is_compl f.range G) (hG : is_closed (G : set F)) (hker : f.ker = ⊥) :
+  is_closed (f.range : set F) :=
+begin
+  let g : (E × G) →L[𝕜] F := f.coprod G.subtypeL,
+  have : (f.range : set F) = g '' ((⊤ : submodule 𝕜 E).prod (⊥ : submodule 𝕜 G)),
+    by { ext x, simp [continuous_linear_map.mem_range] },
+  rw this,
+  haveI : complete_space G := complete_space_coe_iff_is_complete.2 hG.is_complete,
+  have grange : g.range = ⊤,
+    by simp only [range_coprod, h.sup_eq_top, submodule.range_subtypeL],
+  have gker : g.ker = ⊥,
+  { rw [ker_coprod_of_disjoint_range, hker],
+    { simp only [submodule.ker_subtypeL, submodule.prod_bot] },
+    { convert h.disjoint,
+      exact submodule.range_subtypeL _ } },
+  apply (continuous_linear_equiv.of_bijective g gker grange).to_homeomorph.is_closed_image.2,
+  exact is_closed_univ.prod is_closed_singleton,
+end
+
+end continuous_linear_map

src/analysis/normed_space/linear_isometry.lean

@@ -148,6 +148,12 @@ def subtypeL : p →L[R'] E := p.subtypeₗᵢ.to_continuous_linear_map
 
 @[simp] lemma coe_subtypeL' : ⇑p.subtypeL = p.subtype := rfl
 
+@[simp] lemma range_subtypeL : p.subtypeL.range = p :=
+range_subtype _
+
+@[simp] lemma ker_subtypeL : p.subtypeL.ker = ⊥ :=
+ker_subtype _
+
 end submodule
 
 /-- A linear isometric equivalence between two normed vector spaces. -/

src/linear_algebra/prod.lean

@@ -252,6 +252,29 @@ begin
   exact ⟨⟨x, rfl⟩, ⟨x, rfl⟩⟩
 end
 
+lemma ker_prod_ker_le_ker_coprod {M₂ : Type*} [add_comm_group M₂] [semimodule R M₂]
+  {M₃ : Type*} [add_comm_group M₃] [semimodule R M₃]
+  (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
+  (ker f).prod (ker g) ≤ ker (f.coprod g) :=
+by { rintros ⟨y, z⟩, simp {contextual := tt} }
+
+lemma ker_coprod_of_disjoint_range {M₂ : Type*} [add_comm_group M₂] [semimodule R M₂]
+  {M₃ : Type*} [add_comm_group M₃] [semimodule R M₃]
+  (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (hd : disjoint f.range g.range) :
+  ker (f.coprod g) = (ker f).prod (ker g) :=
+begin
+  apply le_antisymm _ (ker_prod_ker_le_ker_coprod f g),
+  rintros ⟨y, z⟩ h,
+  simp only [mem_ker, mem_prod, coprod_apply] at h ⊢,
+  have : f y ∈ f.range ⊓ g.range,
+  { simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply],
+    use -z,
+    rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add] },
+  rw [hd.eq_bot, mem_bot] at this,
+  rw [this] at h,
+  simpa [this] using h,
+end
+
 end linear_map
 
 namespace submodule

src/topology/algebra/module.lean

@@ -402,6 +402,8 @@ def range (f : M →L[R] M₂) : submodule R M₂ := (f : M →ₗ[R] M₂).rang
 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 mem_range_self (f : M →L[R] M₂) (x : M) : f x ∈ f.range := mem_range.2 ⟨x, rfl⟩
+
 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
@@ -492,6 +494,10 @@ rfl
 @[simp] lemma coprod_apply [has_continuous_add M₃] (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) (x) :
   f₁.coprod f₂ x = f₁ x.1 + f₂ x.2 := rfl
 
+lemma range_coprod [has_continuous_add M₃] (f₁ : M →L[R] M₃) (f₂ : M₂ →L[R] M₃) :
+  (f₁.coprod f₂).range = f₁.range ⊔ f₂.range :=
+linear_map.range_coprod _ _
+
 section
 
 variables {S : Type*} [semiring S] [semimodule R S] [semimodule S M₂] [is_scalar_tower R S M₂]
@@ -608,6 +614,16 @@ lemma range_prod_eq {f : M →L[R] M₂} {g : M →L[R] M₃} (h : ker f ⊔ ker
   range (f.prod g) = (range f).prod (range g) :=
 linear_map.range_prod_eq h
 
+lemma ker_prod_ker_le_ker_coprod [has_continuous_add M₃]
+  (f : M →L[R] M₃) (g : M₂ →L[R] M₃) :
+  (ker f).prod (ker g) ≤ ker (f.coprod g) :=
+linear_map.ker_prod_ker_le_ker_coprod f.to_linear_map g.to_linear_map
+
+lemma ker_coprod_of_disjoint_range [has_continuous_add M₃]
+  (f : M →L[R] M₃) (g : M₂ →L[R] M₃) (hd : disjoint f.range g.range) :
+  ker (f.coprod g) = (ker f).prod (ker g) :=
+linear_map.ker_coprod_of_disjoint_range f.to_linear_map g.to_linear_map hd
+
 section
 variables [topological_add_group M₂]