chore(topology/algebra/module, analysis/normed_space/linear_isometry): dedup submodule.subtypeL and continuous_linear_map.subtype_val (#15700)

To designate the continuous linear inclusion of a submodule into the ambient space, we currently have both `continuous_linear_map.subtype_val` (correct assumptions, name not consistent with `submodule.subtype`) and `submodule.subtypeL` (good name, but way too strong assumptions). This keeps the best of both worlds.

Author: ADedecker

src/analysis/calculus/implicit.lean

@@ -47,7 +47,7 @@ noncomputable theory
 
 open_locale topological_space
 open filter
-open continuous_linear_map (fst snd subtype_val smul_right ker_prod)
+open continuous_linear_map (fst snd smul_right ker_prod)
 open continuous_linear_equiv (of_bijective)
 
 /-!
@@ -309,9 +309,9 @@ end
 lemma to_implicit_function_of_complemented (hf : has_strict_fderiv_at f f' a)
   (hf' : f'.range = ⊤) (hker : f'.ker.closed_complemented) :
   has_strict_fderiv_at (hf.implicit_function_of_complemented f f' hf' hker (f a))
-    (subtype_val f'.ker) 0 :=
+    f'.ker.subtypeL 0 :=
 by convert (implicit_function_data_of_complemented f f' hf hf'
-  hker).implicit_function_has_strict_fderiv_at (subtype_val f'.ker) _ _;
+  hker).implicit_function_has_strict_fderiv_at f'.ker.subtypeL _ _;
     [skip, ext, ext]; simp [classical.some_spec hker]
 
 end complemented
@@ -412,7 +412,7 @@ by apply eq_implicit_function_of_complemented
 
 lemma to_implicit_function (hf : has_strict_fderiv_at f f' a) (hf' : f'.range = ⊤) :
   has_strict_fderiv_at (hf.implicit_function f f' hf' (f a))
-    (subtype_val f'.ker) 0 :=
+    f'.ker.subtypeL 0 :=
 by apply to_implicit_function_of_complemented
 
 end finite_dimensional

src/analysis/normed_space/complemented.lean

@@ -76,16 +76,14 @@ namespace subspace
 
 variables [complete_space E] (p q : subspace 𝕜 E)
 
-open continuous_linear_map (subtype_val)
-
 /-- If `q` is a closed complement of a closed subspace `p`, then `p × q` is continuously
 isomorphic to `E`. -/
 def prod_equiv_of_closed_compl (h : is_compl p q) (hp : is_closed (p : set E))
   (hq : is_closed (q : set E)) : (p × q) ≃L[𝕜] E :=
 begin
   haveI := hp.complete_space_coe, haveI := hq.complete_space_coe,
   refine (p.prod_equiv_of_is_compl q h).to_continuous_linear_equiv_of_continuous _,
-  exact ((subtype_val p).coprod (subtype_val q)).continuous
+  exact (p.subtypeL.coprod q.subtypeL).continuous
 end
 
 /-- Projection to a closed submodule along a closed complement. -/

src/analysis/normed_space/linear_isometry.lean

@@ -251,18 +251,8 @@ def subtypeₗᵢ : p →ₗᵢ[R'] E := ⟨p.subtype, λ x, rfl⟩
 
 @[simp] lemma subtypeₗᵢ_to_linear_map : p.subtypeₗᵢ.to_linear_map = p.subtype := rfl
 
-/-- `submodule.subtype` as a `continuous_linear_map`. -/
-def subtypeL : p →L[R'] E := p.subtypeₗᵢ.to_continuous_linear_map
-
-@[simp] lemma coe_subtypeL : (p.subtypeL : p →ₗ[R'] E) = p.subtype := rfl
-
-@[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 _
+@[simp] lemma subtypeₗᵢ_to_continuous_linear_map :
+  p.subtypeₗᵢ.to_continuous_linear_map = p.subtypeL := rfl
 
 end submodule
 

src/topology/algebra/module/basic.lean

@@ -799,19 +799,29 @@ rfl
   ker (f.cod_restrict p h) = ker f :=
 (f : M₁ →ₛₗ[σ₁₂] M₂).ker_cod_restrict p h
 
-/-- Embedding of a submodule into the ambient space as a continuous linear map. -/
-def subtype_val (p : submodule R₁ M₁) : p →L[R₁] M₁ :=
+/-- `submodule.subtype` as a `continuous_linear_map`. -/
+def _root_.submodule.subtypeL (p : submodule R₁ M₁) : p →L[R₁] M₁ :=
 { cont := continuous_subtype_val,
   to_linear_map := p.subtype }
 
-@[simp, norm_cast] lemma coe_subtype_val (p : submodule R₁ M₁) :
-  (subtype_val p : p →ₗ[R₁] M₁) = p.subtype :=
+@[simp, norm_cast] lemma _root_.submodule.coe_subtypeL (p : submodule R₁ M₁) :
+  (p.subtypeL : p →ₗ[R₁] M₁) = p.subtype :=
 rfl
 
-@[simp, norm_cast] lemma subtype_val_apply (p : submodule R₁ M₁) (x : p) :
-  (subtype_val p : p → M₁) x = x :=
+@[simp] lemma _root_.submodule.coe_subtypeL' (p : submodule R₁ M₁) :
+  ⇑p.subtypeL = p.subtype :=
 rfl
 
+@[simp, norm_cast] lemma _root_.submodule.subtypeL_apply (p : submodule R₁ M₁) (x : p) :
+  p.subtypeL x = x :=
+rfl
+
+@[simp] lemma _root_.submodule.range_subtypeL (p : submodule R₁ M₁) : p.subtypeL.range = p :=
+submodule.range_subtype _
+
+@[simp] lemma _root_.submodule.ker_subtypeL (p : submodule R₁ M₁) : p.subtypeL.ker = ⊥ :=
+submodule.ker_subtype _
+
 variables (R₁ M₁ M₂)
 
 /-- `prod.fst` as a `continuous_linear_map`. -/
@@ -1769,14 +1779,14 @@ end
 
 variables [module R M₂] [topological_add_group M]
 
-open _root_.continuous_linear_map (id fst snd subtype_val mem_ker)
+open _root_.continuous_linear_map (id fst snd mem_ker)
 
 /-- A pair of continuous linear maps such that `f₁ ∘ f₂ = id` generates a continuous
 linear equivalence `e` between `M` and `M₂ × f₁.ker` such that `(e x).2 = x` for `x ∈ f₁.ker`,
 `(e x).1 = f₁ x`, and `(e (f₂ y)).2 = 0`. The map is given by `e x = (f₁ x, x - f₂ (f₁ x))`. -/
 def equiv_of_right_inverse (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : function.right_inverse f₂ f₁) :
   M ≃L[R] M₂ × f₁.ker :=
-equiv_of_inverse (f₁.prod (f₁.proj_ker_of_right_inverse f₂ h)) (f₂.coprod (subtype_val f₁.ker))
+equiv_of_inverse (f₁.prod (f₁.proj_ker_of_right_inverse f₂ h)) (f₂.coprod f₁.ker.subtypeL)
   (λ x, by simp)
   (λ ⟨x, y⟩, by simp [h x])
 
@@ -1934,7 +1944,7 @@ protected lemma closed_complemented.is_closed [topological_add_group M] [t1_spac
   is_closed (p : set M) :=
 begin
   rcases h with ⟨f, hf⟩,
-  have : ker (id R M - (subtype_val p).comp f) = p := linear_map.ker_id_sub_eq_of_proj hf,
+  have : ker (id R M - p.subtypeL.comp f) = p := linear_map.ker_id_sub_eq_of_proj hf,
   exact this ▸ (is_closed_ker _)
 end