refactor(analysis/normed_space/linear_isometry): semilinear isometries (#9551)

Generalize the theory of linear isometries to the semilinear setting.

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/normed_space/linear_isometry.lean

@@ -1,16 +1,17 @@
 /-
 Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov
+Authors: Yury Kudryashov, Frédéric Dupuis, Heather Macbeth
 -/
 import analysis.normed_space.basic
 
 /-!
-# Linear isometries
+# (Semi-)linear isometries
 
-In this file we define `linear_isometry R E F` (notation: `E →ₗᵢ[R] F`) to be a linear isometric
-embedding of `E` into `F` and `linear_isometry_equiv` (notation: `E ≃ₗᵢ[R] F`) to be a linear
-isometric equivalence between `E` and `F`.
+In this file we define `linear_isometry σ₁₂ E E₂` (notation: `E →ₛₗᵢ[σ₁₂] E₂`) to be a semilinear
+isometric embedding of `E` into `E₂` and `linear_isometry_equiv` (notation: `E ≃ₛₗᵢ[σ₁₂] E₂`) to be
+a semilinear isometric equivalence between `E` and `E₂`.  The notation for the associated purely
+linear concepts is `E →ₗᵢ[R] E₂`, `E ≃ₗᵢ[R] E₂`.
 
 We also prove some trivial lemmas and provide convenience constructors.
 
@@ -19,34 +20,48 @@ theory for `semi_normed_space` and we specialize to `normed_space` when needed.
 -/
 open function set
 
-variables {R E F G G' E₁ : Type*} [semiring R]
-  [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [semi_normed_group G']
-  [module R E] [module R F] [module R G] [module R G']
-  [normed_group E₁] [module R E₁]
-
-/-- An `R`-linear isometric embedding of one normed `R`-module into another. -/
-structure linear_isometry (R E F : Type*) [semiring R] [semi_normed_group E]
-  [semi_normed_group F] [module R E] [module R F] extends E →ₗ[R] F :=
+variables {R R₂ R₃ R₄ E E₂ E₃ E₄ F : Type*} [semiring R] [semiring R₂] [semiring R₃] [semiring R₄]
+  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₁₄ : R →+* R₄}
+  {σ₄₁ : R₄ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₂₄ : R₂ →+* R₄} {σ₄₂ : R₄ →+* R₂}
+  {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃}
+  [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂]
+  [ring_hom_inv_pair σ₁₃ σ₃₁] [ring_hom_inv_pair σ₃₁ σ₁₃]
+  [ring_hom_inv_pair σ₂₃ σ₃₂] [ring_hom_inv_pair σ₃₂ σ₂₃]
+  [ring_hom_inv_pair σ₁₄ σ₄₁] [ring_hom_inv_pair σ₄₁ σ₁₄]
+  [ring_hom_inv_pair σ₂₄ σ₄₂] [ring_hom_inv_pair σ₄₂ σ₂₄]
+  [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄]
+  [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄]
+  [ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
+  [ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁] [ring_hom_comp_triple σ₄₂ σ₂₁ σ₄₁]
+  [ring_hom_comp_triple σ₄₃ σ₃₂ σ₄₂] [ring_hom_comp_triple σ₄₃ σ₃₁ σ₄₁]
+  [semi_normed_group E] [semi_normed_group E₂] [semi_normed_group E₃] [semi_normed_group E₄]
+  [module R E] [module R₂ E₂] [module R₃ E₃] [module R₄ E₄]
+  [normed_group F] [module R F]
+
+/-- A `σ₁₂`-semilinear isometric embedding of a normed `R`-module into an `R₂`-module. -/
+structure linear_isometry (σ₁₂ : R →+* R₂) (E E₂ : Type*) [semi_normed_group E]
+  [semi_normed_group E₂] [module R E] [module R₂ E₂] extends E →ₛₗ[σ₁₂] E₂ :=
 (norm_map' : ∀ x, ∥to_linear_map x∥ = ∥x∥)
 
-notation E ` →ₗᵢ[`:25 R:25 `] `:0 F:0 := linear_isometry R E F
+notation E ` →ₛₗᵢ[`:25 σ₁₂:25 `] `:0 E₂:0 := linear_isometry σ₁₂ E E₂
+notation E ` →ₗᵢ[`:25 R:25 `] `:0 E₂:0 := linear_isometry (ring_hom.id R) E E₂
 
 namespace linear_isometry
 
 /-- We use `f₁` when we need the domain to be a `normed_space`. -/
-variables (f : E →ₗᵢ[R] F) (f₁ : E₁ →ₗᵢ[R] F)
+variables (f : E →ₛₗᵢ[σ₁₂] E₂) (f₁ : F →ₛₗᵢ[σ₁₂] E₂)
 
-instance : has_coe_to_fun (E →ₗᵢ[R] F) := ⟨_, λ f, f.to_fun⟩
+instance : has_coe_to_fun (E →ₛₗᵢ[σ₁₂] E₂) := ⟨_, λ f, f.to_fun⟩
 
 @[simp] lemma coe_to_linear_map : ⇑f.to_linear_map = f := rfl
 
-lemma to_linear_map_injective : injective (to_linear_map : (E →ₗᵢ[R] F) → (E →ₗ[R] F))
+lemma to_linear_map_injective : injective (to_linear_map : (E →ₛₗᵢ[σ₁₂] E₂) → (E →ₛₗ[σ₁₂] E₂))
 | ⟨f, _⟩ ⟨g, _⟩ rfl := rfl
 
-lemma coe_fn_injective : injective (λ (f : E →ₗᵢ[R] F) (x : E), f x) :=
+lemma coe_fn_injective : injective (λ (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E), f x) :=
 linear_map.coe_injective.comp to_linear_map_injective
 
-@[ext] lemma ext {f g : E →ₗᵢ[R] F} (h : ∀ x, f x = g x) : f = g :=
+@[ext] lemma ext {f g : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ x, f x = g x) : f = g :=
 coe_fn_injective $ funext h
 
 @[simp] lemma map_zero : f 0 = 0 := f.to_linear_map.map_zero
@@ -55,7 +70,10 @@ coe_fn_injective $ funext h
 
 @[simp] lemma map_sub (x y : E) : f (x - y) = f x - f y := f.to_linear_map.map_sub x y
 
-@[simp] lemma map_smul (c : R) (x : E) : f (c • x) = c • f x := f.to_linear_map.map_smul c x
+@[simp] lemma map_smulₛₗ (c : R) (x : E) : f (c • x) = σ₁₂ c • f x := f.to_linear_map.map_smulₛₗ c x
+
+@[simp] lemma map_smul [module R E₂] (f : E →ₗᵢ[R] E₂) (c : R) (x : E) : f (c • x) = c • f x :=
+f.to_linear_map.map_smul c x
 
 @[simp] lemma norm_map (x : E) : ∥f x∥ = ∥x∥ := f.norm_map' x
 
@@ -69,9 +87,9 @@ f.to_linear_map.to_add_monoid_hom.isometry_of_norm f.norm_map
 
 protected lemma injective : injective f₁ := f₁.isometry.injective
 
-@[simp] lemma map_eq_iff {x y : E₁} : f₁ x = f₁ y ↔ x = y := f₁.injective.eq_iff
+@[simp] lemma map_eq_iff {x y : F} : f₁ x = f₁ y ↔ x = y := f₁.injective.eq_iff
 
-lemma map_ne {x y : E₁} (h : x ≠ y) : f₁ x ≠ f₁ y := f₁.injective.ne h
+lemma map_ne {x y : F} (h : x ≠ y) : f₁ x ≠ f₁ y := f₁.injective.ne h
 
 protected lemma lipschitz : lipschitz_with 1 f := f.isometry.lipschitz
 
@@ -92,7 +110,7 @@ lemma diam_range : metric.diam (range f) = metric.diam (univ : set E) :=
 f.isometry.diam_range
 
 /-- Interpret a linear isometry as a continuous linear map. -/
-def to_continuous_linear_map : E →L[R] F := ⟨f.to_linear_map, f.continuous⟩
+def to_continuous_linear_map : E →SL[σ₁₂] E₂ := ⟨f.to_linear_map, f.continuous⟩
 
 @[simp] lemma coe_to_continuous_linear_map : ⇑f.to_continuous_linear_map = f := rfl
 
@@ -112,20 +130,24 @@ def id : E →ₗᵢ[R] E := ⟨linear_map.id, λ x, rfl⟩
 instance : inhabited (E →ₗᵢ[R] E) := ⟨id⟩
 
 /-- Composition of linear isometries. -/
-def comp (g : F →ₗᵢ[R] G) (f : E →ₗᵢ[R] F) : E →ₗᵢ[R] G :=
+def comp (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) : E →ₛₗᵢ[σ₁₃] E₃ :=
 ⟨g.to_linear_map.comp f.to_linear_map, λ x, (g.norm_map _).trans (f.norm_map _)⟩
 
-@[simp] lemma coe_comp (g : F →ₗᵢ[R] G) (f : E →ₗᵢ[R] F) :
+include σ₁₃
+@[simp] lemma coe_comp (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) :
   ⇑(g.comp f) = g ∘ f :=
 rfl
+omit σ₁₃
 
-@[simp] lemma id_comp : (id : F →ₗᵢ[R] F).comp f = f := ext $ λ x, rfl
+@[simp] lemma id_comp : (id : E₂ →ₗᵢ[R₂] E₂).comp f = f := ext $ λ x, rfl
 
 @[simp] lemma comp_id : f.comp id = f := ext $ λ x, rfl
 
-lemma comp_assoc (f : G →ₗᵢ[R] G') (g : F →ₗᵢ[R] G) (h : E →ₗᵢ[R] F) :
+include σ₁₃ σ₂₄ σ₁₄
+lemma comp_assoc (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂) :
   (f.comp g).comp h = f.comp (g.comp h) :=
 rfl
+omit σ₁₃ σ₂₄ σ₁₄
 
 instance : monoid (E →ₗᵢ[R] E) :=
 { one := id,
@@ -165,55 +187,59 @@ ker_subtype _
 
 end submodule
 
-/-- A linear isometric equivalence between two normed vector spaces. -/
-structure linear_isometry_equiv (R E F : Type*) [semiring R] [semi_normed_group E]
-  [semi_normed_group F] [module R E] [module R F] extends E ≃ₗ[R] F :=
+/-- A semilinear isometric equivalence between two normed vector spaces. -/
+structure linear_isometry_equiv (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁]
+  [ring_hom_inv_pair σ₂₁ σ₁₂] (E E₂ : Type*) [semi_normed_group E] [semi_normed_group E₂]
+  [module R E] [module R₂ E₂] extends E ≃ₛₗ[σ₁₂] E₂ :=
 (norm_map' : ∀ x, ∥to_linear_equiv x∥ = ∥x∥)
 
-notation E ` ≃ₗᵢ[`:25 R:25 `] `:0 F:0 := linear_isometry_equiv R E F
+notation E ` ≃ₛₗᵢ[`:25 σ₁₂:25 `] `:0 E₂:0 := linear_isometry_equiv σ₁₂ E E₂
+notation E ` ≃ₗᵢ[`:25 R:25 `] `:0 E₂:0 := linear_isometry_equiv (ring_hom.id R) E E₂
 
 namespace linear_isometry_equiv
 
-variables (e : E ≃ₗᵢ[R] F)
+variables (e : E ≃ₛₗᵢ[σ₁₂] E₂)
 
-instance : has_coe_to_fun (E ≃ₗᵢ[R] F) := ⟨_, λ f, f.to_fun⟩
+include σ₂₁
+instance : has_coe_to_fun (E ≃ₛₗᵢ[σ₁₂] E₂) := ⟨_, λ f, f.to_fun⟩
 
-@[simp] lemma coe_mk (e : E ≃ₗ[R] F) (he : ∀ x, ∥e x∥ = ∥x∥) :
+@[simp] lemma coe_mk (e : E ≃ₛₗ[σ₁₂] E₂) (he : ∀ x, ∥e x∥ = ∥x∥) :
   ⇑(mk e he) = e :=
 rfl
 
-@[simp] lemma coe_to_linear_equiv (e : E ≃ₗᵢ[R] F) : ⇑e.to_linear_equiv = e := rfl
+@[simp] lemma coe_to_linear_equiv (e : E ≃ₛₗᵢ[σ₁₂] E₂) : ⇑e.to_linear_equiv = e := rfl
 
-lemma to_linear_equiv_injective : injective (to_linear_equiv : (E ≃ₗᵢ[R] F) → (E ≃ₗ[R] F))
+lemma to_linear_equiv_injective : injective (to_linear_equiv : (E ≃ₛₗᵢ[σ₁₂] E₂) → (E ≃ₛₗ[σ₁₂] E₂))
 | ⟨e, _⟩ ⟨_, _⟩ rfl := rfl
 
-@[ext] lemma ext {e e' : E ≃ₗᵢ[R] F} (h : ∀ x, e x = e' x) : e = e' :=
+@[ext] lemma ext {e e' : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ x, e x = e' x) : e = e' :=
 to_linear_equiv_injective $ linear_equiv.ext h
 
 /-- Construct a `linear_isometry_equiv` from a `linear_equiv` and two inequalities:
 `∀ x, ∥e x∥ ≤ ∥x∥` and `∀ y, ∥e.symm y∥ ≤ ∥y∥`. -/
-def of_bounds (e : E ≃ₗ[R] F) (h₁ : ∀ x, ∥e x∥ ≤ ∥x∥) (h₂ : ∀ y, ∥e.symm y∥ ≤ ∥y∥) : E ≃ₗᵢ[R] F :=
+def of_bounds (e : E ≃ₛₗ[σ₁₂] E₂) (h₁ : ∀ x, ∥e x∥ ≤ ∥x∥) (h₂ : ∀ y, ∥e.symm y∥ ≤ ∥y∥) :
+  E ≃ₛₗᵢ[σ₁₂] E₂ :=
 ⟨e, λ x, le_antisymm (h₁ x) $ by simpa only [e.symm_apply_apply] using h₂ (e x)⟩
 
 @[simp] lemma norm_map (x : E) : ∥e x∥ = ∥x∥ := e.norm_map' x
 
 /-- Reinterpret a `linear_isometry_equiv` as a `linear_isometry`. -/
-def to_linear_isometry : E →ₗᵢ[R] F := ⟨e.1, e.2⟩
+def to_linear_isometry : E →ₛₗᵢ[σ₁₂] E₂ := ⟨e.1, e.2⟩
 
 @[simp] lemma coe_to_linear_isometry : ⇑e.to_linear_isometry = e := rfl
 
 protected lemma isometry : isometry e := e.to_linear_isometry.isometry
 
 /-- Reinterpret a `linear_isometry_equiv` as an `isometric`. -/
-def to_isometric : E ≃ᵢ F := ⟨e.to_linear_equiv.to_equiv, e.isometry⟩
+def to_isometric : E ≃ᵢ E₂ := ⟨e.to_linear_equiv.to_equiv, e.isometry⟩
 
 @[simp] lemma coe_to_isometric : ⇑e.to_isometric = e := rfl
 
-lemma range_eq_univ (e : E ≃ₗᵢ[R] F) : set.range e = set.univ :=
+lemma range_eq_univ (e : E ≃ₛₗᵢ[σ₁₂] E₂) : set.range e = set.univ :=
 by { rw ← coe_to_isometric, exact isometric.range_eq_univ _, }
 
 /-- Reinterpret a `linear_isometry_equiv` as an `homeomorph`. -/
-def to_homeomorph : E ≃ₜ F := e.to_isometric.to_homeomorph
+def to_homeomorph : E ≃ₜ E₂ := e.to_isometric.to_homeomorph
 
 @[simp] lemma coe_to_homeomorph : ⇑e.to_homeomorph = e := rfl
 
@@ -225,12 +251,14 @@ protected lemma continuous_within_at {s x} : continuous_within_at e s x :=
 e.continuous.continuous_within_at
 
 /-- Interpret a `linear_isometry_equiv` as a continuous linear equiv. -/
-def to_continuous_linear_equiv : E ≃L[R] F :=
+def to_continuous_linear_equiv : E ≃SL[σ₁₂] E₂ :=
 { .. e.to_linear_isometry.to_continuous_linear_map,
   .. e.to_homeomorph }
 
 @[simp] lemma coe_to_continuous_linear_equiv : ⇑e.to_continuous_linear_equiv = e := rfl
 
+omit σ₂₁
+
 variables (R E)
 
 /-- Identity map as a `linear_isometry_equiv`. -/
@@ -243,11 +271,11 @@ instance : inhabited (E ≃ₗᵢ[R] E) := ⟨refl R E⟩
 @[simp] lemma coe_refl : ⇑(refl R E) = id := rfl
 
 /-- The inverse `linear_isometry_equiv`. -/
-def symm : F ≃ₗᵢ[R] E :=
+def symm : E₂ ≃ₛₗᵢ[σ₂₁] E :=
 ⟨e.to_linear_equiv.symm,
   λ x, (e.norm_map _).symm.trans $ congr_arg norm $ e.to_linear_equiv.apply_symm_apply x⟩
 
-@[simp] lemma apply_symm_apply (x : F) : e (e.symm x) = x := e.to_linear_equiv.apply_symm_apply x
+@[simp] lemma apply_symm_apply (x : E₂) : e (e.symm x) = x := e.to_linear_equiv.apply_symm_apply x
 @[simp] lemma symm_apply_apply (x : E) : e.symm (e x) = x := e.to_linear_equiv.symm_apply_apply x
 @[simp] lemma map_eq_zero_iff {x : E} : e x = 0 ↔ x = 0 := e.to_linear_equiv.map_eq_zero_iff
 @[simp] lemma symm_symm : e.symm.symm = e := ext $ λ x, rfl
@@ -256,23 +284,31 @@ def symm : F ≃ₗᵢ[R] E :=
 @[simp] lemma to_isometric_symm : e.to_isometric.symm = e.symm.to_isometric := rfl
 @[simp] lemma to_homeomorph_symm : e.to_homeomorph.symm = e.symm.to_homeomorph := rfl
 
+include σ₃₁ σ₃₂
 /-- Composition of `linear_isometry_equiv`s as a `linear_isometry_equiv`. -/
-def trans (e' : F ≃ₗᵢ[R] G) : E ≃ₗᵢ[R] G :=
+def trans (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : E ≃ₛₗᵢ[σ₁₃] E₃ :=
 ⟨e.to_linear_equiv.trans e'.to_linear_equiv, λ x, (e'.norm_map _).trans (e.norm_map _)⟩
 
-@[simp] lemma coe_trans (e₁ : E ≃ₗᵢ[R] F) (e₂ : F ≃ₗᵢ[R] G) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ := rfl
-@[simp] lemma trans_refl : e.trans (refl R F) = e := ext $ λ x, rfl
+include σ₁₃ σ₂₁
+@[simp] lemma coe_trans (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ :=
+rfl
+omit σ₁₃ σ₂₁ σ₃₁ σ₃₂
+
+@[simp] lemma trans_refl : e.trans (refl R₂ E₂) = e := ext $ λ x, rfl
 @[simp] lemma refl_trans : (refl R E).trans e = e := ext $ λ x, rfl
 @[simp] lemma trans_symm : e.trans e.symm = refl R E := ext e.symm_apply_apply
-@[simp] lemma symm_trans : e.symm.trans e = refl R F := ext e.apply_symm_apply
+@[simp] lemma symm_trans : e.symm.trans e = refl R₂ E₂ := ext e.apply_symm_apply
 
-@[simp] lemma coe_symm_trans (e₁ : E ≃ₗᵢ[R] F) (e₂ : F ≃ₗᵢ[R] G) :
+include σ₁₃ σ₂₁ σ₃₂ σ₃₁
+@[simp] lemma coe_symm_trans (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
   ⇑(e₁.trans e₂).symm = e₁.symm ∘ e₂.symm :=
 rfl
 
-lemma trans_assoc (eEF : E ≃ₗᵢ[R] F) (eFG : F ≃ₗᵢ[R] G) (eGG' : G ≃ₗᵢ[R] G') :
-  eEF.trans (eFG.trans eGG') = (eEF.trans eFG).trans eGG' :=
+include σ₁₄ σ₄₁ σ₄₂ σ₄₃ σ₂₄
+lemma trans_assoc (eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂) (eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄) :
+  eEE₂.trans (eE₂E₃.trans eE₃E₄) = (eEE₂.trans eE₂E₃).trans eE₃E₄ :=
 rfl
+omit σ₂₁ σ₃₁ σ₄₁ σ₃₂ σ₄₂ σ₄₃ σ₁₃ σ₂₄ σ₁₄
 
 instance : group (E ≃ₗᵢ[R] E) :=
 { mul := λ e₁ e₂, e₂.trans e₁,
@@ -287,25 +323,32 @@ instance : group (E ≃ₗᵢ[R] E) :=
 @[simp] lemma coe_mul (e e' : E ≃ₗᵢ[R] E) : ⇑(e * e') = e ∘ e' := rfl
 @[simp] lemma coe_inv (e : E ≃ₗᵢ[R] E) : ⇑(e⁻¹) = e.symm := rfl
 
+include σ₂₁
+
 /-- Reinterpret a `linear_isometry_equiv` as a `continuous_linear_equiv`. -/
-instance : has_coe_t (E ≃ₗᵢ[R] F) (E ≃L[R] F) :=
+instance : has_coe_t (E ≃ₛₗᵢ[σ₁₂] E₂) (E ≃SL[σ₁₂] E₂) :=
 ⟨λ e, ⟨e.to_linear_equiv, e.continuous, e.to_isometric.symm.continuous⟩⟩
 
-instance : has_coe_t (E ≃ₗᵢ[R] F) (E →L[R] F) := ⟨λ e, ↑(e : E ≃L[R] F)⟩
+instance : has_coe_t (E ≃ₛₗᵢ[σ₁₂] E₂) (E →SL[σ₁₂] E₂) := ⟨λ e, ↑(e : E ≃SL[σ₁₂] E₂)⟩
 
-@[simp] lemma coe_coe : ⇑(e : E ≃L[R] F) = e := rfl
+@[simp] lemma coe_coe : ⇑(e : E ≃SL[σ₁₂] E₂) = e := rfl
 
-@[simp] lemma coe_coe' : ((e : E ≃L[R] F) : E →L[R] F) = e := rfl
+@[simp] lemma coe_coe' : ((e : E ≃SL[σ₁₂] E₂) : E →SL[σ₁₂] E₂) = e := rfl
 
-@[simp] lemma coe_coe'' : ⇑(e : E →L[R] F) = e := rfl
+@[simp] lemma coe_coe'' : ⇑(e : E →SL[σ₁₂] E₂) = e := rfl
+
+omit σ₂₁
 
 @[simp] lemma map_zero : e 0 = 0 := e.1.map_zero
 
 @[simp] lemma map_add (x y : E) : e (x + y) = e x + e y := e.1.map_add x y
 
 @[simp] lemma map_sub (x y : E) : e (x - y) = e x - e y := e.1.map_sub x y
 
-@[simp] lemma map_smul (c : R) (x : E) : e (c • x) = c • e x := e.1.map_smul c x
+@[simp] lemma map_smulₛₗ (c : R) (x : E) : e (c • x) = σ₁₂ c • e x := e.1.map_smulₛₗ c x
+
+@[simp] lemma map_smul [module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E) : e (c • x) = c • e x :=
+e.1.map_smul c x
 
 @[simp] lemma nnnorm_map (x : E) : nnnorm (e x) = nnnorm x := e.to_linear_isometry.nnnorm_map x
 
@@ -343,12 +386,14 @@ e.isometry.comp_continuous_on_iff
   continuous (e ∘ f) ↔ continuous f :=
 e.isometry.comp_continuous_iff
 
+include σ₂₁
 /-- Construct a linear isometry equiv from a surjective linear isometry. -/
-noncomputable def of_surjective (f : E₁ →ₗᵢ[R] F)
+noncomputable def of_surjective (f : F →ₛₗᵢ[σ₁₂] E₂)
   (hfr : function.surjective f) :
-  E₁ ≃ₗᵢ[R] F :=
+  F ≃ₛₗᵢ[σ₁₂] E₂ :=
 { norm_map' := f.norm_map,
   .. linear_equiv.of_bijective f.to_linear_map f.injective hfr }
+omit σ₂₁
 
 variables (R)
 /-- The negation operation on a normed space `E`, considered as a linear isometry equivalence. -/

src/analysis/normed_space/multilinear.lean

@@ -446,8 +446,8 @@ def prodL :
 /-- `continuous_multilinear_map.pi` as a `linear_isometry_equiv`. -/
 def piₗᵢ {ι' : Type v'} [fintype ι'] {E' : ι' → Type wE'} [Π i', normed_group (E' i')]
   [Π i', normed_space 𝕜 (E' i')] :
-  @linear_isometry_equiv 𝕜 (Π i', continuous_multilinear_map 𝕜 E (E' i'))
-    (continuous_multilinear_map 𝕜 E (Π i, E' i)) _ _ _
+  @linear_isometry_equiv 𝕜 𝕜 _ _ (ring_hom.id 𝕜) _ _ _
+    (Π i', continuous_multilinear_map 𝕜 E (E' i')) (continuous_multilinear_map 𝕜 E (Π i, E' i)) _ _
       (@pi.module ι' _ 𝕜 _ _ (λ i', infer_instance)) _ :=
 { to_linear_equiv :=
   -- note: `pi_linear_equiv` does not unify correctly here, presumably due to issues with dependent