refactor(algebra/restrict_scalars): remove global instance on module_…

…orig (#13759)

The global instance was conceptually wrong, unnecessary (after avoiding a hack in algebra/lie/base_change.lean), and wreaking havoc in #13713.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/algebra/restrict_scalars.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import algebra.algebra.basic
+import algebra.algebra.tower
 
 /-!
 
@@ -16,10 +16,14 @@ typeclass instead.
 ## Main definitions
 
 * `restrict_scalars R S M`: the `S`-module `M` viewed as an `R` module when `S` is an `R`-algebra.
-* `restrict_scalars.linear_equiv : restrict_scalars R S M ≃ₗ[S] M`: the equivalence as an
-  `S`-module between the restricted and origianl space.
-* `restrict_scalars.alg_equiv : restrict_scalars R S A ≃ₐ[S] A`: the equivalence as an `S`-algebra
-   between the restricted and original space.
+  Note that by default we do *not* have a `module S (restrict_scalars R S M)` instance
+  for the original action.
+  This is available as a def `restrict_scalars.module_orig` if really needed.
+* `restrict_scalars.add_equiv : restrict_scalars R S M ≃+ M`: the additive equivalence
+  between the restricted and original space (in fact, they are definitionally equal,
+  but sometimes it is helpful to avoid using this fact, to keep instances from leaking).
+* `restrict_scalars.ring_equiv : restrict_scalars R S A ≃+* A`: the ring equivalence
+   between the restricted and original space when the module is an algebra.
 
 ## See also
 
@@ -76,16 +80,19 @@ instance [I : add_comm_monoid M] : add_comm_monoid (restrict_scalars R S M) := I
 
 instance [I : add_comm_group M] : add_comm_group (restrict_scalars R S M) := I
 
-instance restrict_scalars.module_orig [semiring S] [add_comm_monoid M] [I : module S M] :
+section module
+
+section
+variables [semiring S] [add_comm_monoid M]
+
+/-- We temporarily install an action of the original ring on `restrict_sclars R S M`. -/
+def restrict_scalars.module_orig [I : module S M] :
   module S (restrict_scalars R S M) := I
 
-/-- `restrict_scalars.linear_equiv` is an equivalence of modules over the semiring `S`. -/
-def restrict_scalars.linear_equiv [semiring S] [add_comm_monoid M] [module S M] :
-  restrict_scalars R S M ≃ₗ[S] M :=
-linear_equiv.refl S M
+variables [comm_semiring R] [algebra R S] [module S M]
 
-section module
-variables [semiring S] [add_comm_monoid M] [comm_semiring R] [algebra R S] [module S M]
+section
+local attribute [instance] restrict_scalars.module_orig
 
 /--
 When `M` is a module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
@@ -96,17 +103,44 @@ The preferred way of setting this up is `[module R M] [module S M] [is_scalar_to
 instance : module R (restrict_scalars R S M) :=
 module.comp_hom M (algebra_map R S)
 
+/--
+This instance is only relevant when `restrict_scalars.module_orig` is available as an instance.
+-/
+instance : is_scalar_tower R S (restrict_scalars R S M) :=
+⟨λ r S M, by { rw [algebra.smul_def, mul_smul], refl }⟩
+
+end
+
+/--
+The `R`-algebra homomorphism from the original coefficient algebra `S` to endomorphisms
+of `restrict_scalars R S M`.
+-/
+def restrict_scalars.lsmul : S →ₐ[R] module.End R (restrict_scalars R S M) :=
+begin
+  -- We use `restrict_scalars.module_orig` in the implementation,
+  -- but not in the type.
+  letI : module S (restrict_scalars R S M) := restrict_scalars.module_orig R S M,
+  exact algebra.lsmul R (restrict_scalars R S M),
+end
+
+end
+
+variables [add_comm_monoid M]
+
+/-- `restrict_scalars.add_equiv` is the additive equivalence with the original module. -/
+@[simps] def restrict_scalars.add_equiv : restrict_scalars R S M ≃+ M :=
+add_equiv.refl M
+
+variables [comm_semiring R] [semiring S] [algebra R S] [module S M]
+
 lemma restrict_scalars_smul_def (c : R) (x : restrict_scalars R S M) :
   c • x = ((algebra_map R S c) • x : M) := rfl
 
-@[simp] lemma restrict_scalars.linear_equiv_map_smul (t : R) (x : restrict_scalars R S M) :
-  restrict_scalars.linear_equiv R S M (t • x)
-  = (algebra_map R S t) • restrict_scalars.linear_equiv R S M x :=
+@[simp] lemma restrict_scalars.add_equiv_map_smul (t : R) (x : restrict_scalars R S M) :
+  restrict_scalars.add_equiv R S M (t • x)
+  = (algebra_map R S t) • restrict_scalars.add_equiv R S M x :=
 rfl
 
-instance : is_scalar_tower R S (restrict_scalars R S M) :=
-⟨λ r S M, by { rw [algebra.smul_def, mul_smul], refl }⟩
-
 end module
 
 section algebra
@@ -116,16 +150,17 @@ instance [I : ring A] : ring (restrict_scalars R S A) := I
 instance [I : comm_semiring A] : comm_semiring (restrict_scalars R S A) := I
 instance [I : comm_ring A] : comm_ring (restrict_scalars R S A) := I
 
-variables [comm_semiring S] [semiring A]
-
-instance restrict_scalars.algebra_orig [I : algebra S A] : algebra S (restrict_scalars R S A) := I
+variables [semiring A]
 
-variables [algebra S A]
+/-- Tautological ring isomorphism `restrict_scalars R S A ≃+* A`. -/
+def restrict_scalars.ring_equiv : restrict_scalars R S A ≃+* A := ring_equiv.refl _
 
-/-- Tautological `S`-algebra isomorphism `restrict_scalars R S A ≃ₐ[S] A`. -/
-def restrict_scalars.alg_equiv : restrict_scalars R S A ≃ₐ[S] A := alg_equiv.refl
+variables [comm_semiring S] [algebra S A] [comm_semiring R] [algebra R S]
 
-variables [comm_semiring R] [algebra R S]
+@[simp] lemma restrict_scalars.ring_equiv_map_smul (r : R) (x : restrict_scalars R S A) :
+  restrict_scalars.ring_equiv R S A (r • x)
+  = (algebra_map R S r) • restrict_scalars.ring_equiv R S A x :=
+rfl
 
 /-- `R ⟶ S` induces `S-Alg ⥤ R-Alg` -/
 instance : algebra R (restrict_scalars R S A) :=
@@ -134,4 +169,9 @@ instance : algebra R (restrict_scalars R S A) :=
   smul_def' := λ _ _, algebra.smul_def _ _,
   .. (algebra_map S A).comp (algebra_map R S) }
 
+@[simp] lemma restrict_scalars.ring_equiv_algebra_map (r : R) :
+  restrict_scalars.ring_equiv R S A (algebra_map R (restrict_scalars R S A) r) =
+    algebra_map S A (algebra_map R S r) :=
+rfl
+
 end algebra

src/algebra/lie/base_change.lean

@@ -141,10 +141,9 @@ instance : lie_ring (restrict_scalars R A L) := h
 
 variables [comm_ring A] [lie_algebra A L]
 
-@[nolint unused_arguments]
 instance lie_algebra [comm_ring R] [algebra R A] : lie_algebra R (restrict_scalars R A L) :=
-{ lie_smul := λ t x y, (lie_smul _ (show L, from x) (show L, from y) : _),
-  .. (by apply_instance : module R (restrict_scalars R A L)), }
+{ lie_smul := λ t x y, (lie_smul (algebra_map R A t)
+    (restrict_scalars.add_equiv R A L x) (restrict_scalars.add_equiv R A L y) : _) }
 
 end restrict_scalars
 

src/analysis/normed_space/basic.lean

@@ -474,11 +474,17 @@ instance {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [I : semi_normed_group E] :
 instance {𝕜 : Type*} {𝕜' : Type*} {E : Type*} [I : normed_group E] :
   normed_group (restrict_scalars 𝕜 𝕜' E) := I
 
-instance module.restrict_scalars.normed_space_orig {𝕜 : Type*} {𝕜' : Type*} {E : Type*}
-  [normed_field 𝕜'] [semi_normed_group E] [I : normed_space 𝕜' E] :
-  normed_space 𝕜' (restrict_scalars 𝕜 𝕜' E) := I
-
 instance : normed_space 𝕜 (restrict_scalars 𝕜 𝕜' E) :=
 (normed_space.restrict_scalars 𝕜 𝕜' E : normed_space 𝕜 E)
 
+/--
+The action of the original normed_field on `restrict_scalars 𝕜 𝕜' E`.
+This is not an instance as it would be contrary to the purpose of `restrict_scalars`.
+-/
+-- If you think you need this, consider instead reproducing `restrict_scalars.lsmul`
+-- appropriately modified here.
+def module.restrict_scalars.normed_space_orig {𝕜 : Type*} {𝕜' : Type*} {E : Type*}
+  [normed_field 𝕜'] [semi_normed_group E] [I : normed_space 𝕜' E] :
+  normed_space 𝕜' (restrict_scalars 𝕜 𝕜' E) := I
+
 end restrict_scalars

src/analysis/normed_space/extend.lean

@@ -132,12 +132,12 @@ noncomputable def linear_map.extend_to_𝕜 (fr : (restrict_scalars ℝ 𝕜 F)
 fr.extend_to_𝕜'
 
 lemma linear_map.extend_to_𝕜_apply (fr : (restrict_scalars ℝ 𝕜 F) →ₗ[ℝ] ℝ) (x : F) :
-  fr.extend_to_𝕜 x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
+  fr.extend_to_𝕜 x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x : _) := rfl
 
 /-- Extend `fr : restrict_scalars ℝ 𝕜 F →L[ℝ] ℝ` to `F →L[𝕜] 𝕜`. -/
 noncomputable def continuous_linear_map.extend_to_𝕜 (fr : (restrict_scalars ℝ 𝕜 F) →L[ℝ] ℝ) :
   F →L[𝕜] 𝕜 :=
 fr.extend_to_𝕜'
 
 lemma continuous_linear_map.extend_to_𝕜_apply (fr : (restrict_scalars ℝ 𝕜 F) →L[ℝ] ℝ) (x : F) :
-  fr.extend_to_𝕜 x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x) := rfl
+  fr.extend_to_𝕜 x = (fr x : 𝕜) - (I : 𝕜) * fr ((I : 𝕜) • x : _) := rfl

src/ring_theory/algebra_tower.lean

@@ -65,13 +65,6 @@ end is_scalar_tower
 
 namespace algebra
 
-theorem adjoin_algebra_map' {R : Type u} {S : Type v} {A : Type w}
-  [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] (s : set S) :
-  adjoin R (algebra_map S (restrict_scalars R S A) '' s) = (adjoin R s).map
-  ((algebra.of_id S (restrict_scalars R S A)).restrict_scalars R) :=
-le_antisymm (adjoin_le $ set.image_subset_iff.2 $ λ y hy, ⟨y, subset_adjoin hy, rfl⟩)
-  (subalgebra.map_le.2 $ adjoin_le $ λ y hy, subset_adjoin ⟨y, hy, rfl⟩)
-
 theorem adjoin_algebra_map (R : Type u) (S : Type v) (A : Type w)
   [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A]
   [is_scalar_tower R S A] (s : set S) :