refactor(topology/algebra/module): continuous semilinear maps (#9539)

Generalize the theory of continuous linear maps to the semilinear setting.

We introduce a notation `∘L` for composition of continuous linear (i.e., not semilinear) maps, used sporadically to help with unification.  See #8857 for a discussion of a related problem and fix.

Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

Author: dupuisf

src/analysis/complex/conformal.lean

@@ -74,7 +74,7 @@ variables {f : ℂ → ℂ} {z : ℂ} {g : ℂ →L[ℝ] ℂ}
 
 lemma is_conformal_map.is_complex_or_conj_linear (h : is_conformal_map g) :
   (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g) ∨
-  (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g.comp ↑conj_cle) :=
+  (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g ∘L ↑conj_cle) :=
 begin
   rcases h with ⟨c, hc, li, hg⟩,
   rcases linear_isometry_complex (li.to_linear_isometry_equiv rfl) with ⟨a, ha⟩,
@@ -100,15 +100,15 @@ end
 lemma is_conformal_map_iff_is_complex_or_conj_linear:
   is_conformal_map g ↔
   ((∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g) ∨
-   (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g.comp ↑conj_cle)) ∧ g ≠ 0 :=
+   (∃ (map : ℂ →L[ℂ] ℂ), map.restrict_scalars ℝ = g ∘L ↑conj_cle)) ∧ g ≠ 0 :=
 begin
   split,
   { exact λ h, ⟨h.is_complex_or_conj_linear, h.ne_zero⟩, },
   { rintros ⟨⟨map, rfl⟩ | ⟨map, hmap⟩, h₂⟩,
     { refine is_conformal_map_complex_linear _,
       contrapose! h₂ with w,
       simp [w] },
-    { have minor₁ : g = (map.restrict_scalars ℝ).comp ↑conj_cle,
+    { have minor₁ : g = (map.restrict_scalars ℝ) ∘L ↑conj_cle,
       { ext1,
         simp [hmap] },
       rw minor₁ at ⊢ h₂,

src/analysis/normed_space/complemented.lean

@@ -91,7 +91,7 @@ end
 def linear_proj_of_closed_compl (h : is_compl p q) (hp : is_closed (p : set E))
   (hq : is_closed (q : set E)) :
   E →L[𝕜] p :=
-(continuous_linear_map.fst 𝕜 p q).comp $ (prod_equiv_of_closed_compl p q h hp hq).symm
+(continuous_linear_map.fst 𝕜 p q) ∘L ↑(prod_equiv_of_closed_compl p q h hp hq).symm
 
 variables {p q}