fix(algebra/algebra/tower): remove subalgebra.res which duplicates subalgebra.restrict_scalars (#9251)

We use the name `restrict_scalars` everywhere else, so I kept that one instead of `res`.

`res` was here first, but the duplicate was added by #7949 presumably because the `res` name wasn't discoverable.

Author: eric-wieser

src/algebra/algebra/tower.lean

@@ -158,18 +158,6 @@ variables (R) {A S B}
 
 open is_scalar_tower
 
-/-- Given a scalar tower `R`, `S`, `A` of algebras, reinterpret an `S`-subalgebra of `A` an as an
-`R`-subalgebra. -/
-def subalgebra.restrict_scalars (iSB : subalgebra S A) :
-  subalgebra R A :=
-{ one_mem' := iSB.one_mem,
-  mul_mem' := λ _ _, iSB.mul_mem,
-  algebra_map_mem' := λ r, begin
-    rw is_scalar_tower.algebra_map_eq R S,
-    exact iSB.algebra_map_mem' _,
-  end,
-  .. iSB.to_submodule.restrict_scalars R }
-
 namespace alg_hom
 
 /-- R ⟶ S induces S-Alg ⥤ R-Alg -/
@@ -221,19 +209,25 @@ section semiring
 variables (R) {S A} [comm_semiring R] [comm_semiring S] [semiring A]
 variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
-/-- If A/S/R is a tower of algebras then the `res`triction of a S-subalgebra of A is
-an R-subalgebra of A. -/
-def res (U : subalgebra S A) : subalgebra R A :=
+/-- Given a scalar tower `R`, `S`, `A` of algebras, reinterpret an `S`-subalgebra of `A` an as an
+`R`-subalgebra. -/
+def restrict_scalars (U : subalgebra S A) : subalgebra R A :=
 { algebra_map_mem' := λ x, by { rw algebra_map_apply R S A, exact U.algebra_map_mem _ },
   .. U }
 
-@[simp] lemma res_top : res R (⊤ : subalgebra S A) = ⊤ :=
-algebra.eq_top_iff.2 $ λ _, show _ ∈ (⊤ : subalgebra S A), from algebra.mem_top
+@[simp] lemma restrict_scalars_top : restrict_scalars R (⊤ : subalgebra S A) = ⊤ :=
+set_like.coe_injective rfl
+
+@[simp] lemma restrict_scalars_to_submodule {U : subalgebra S A} :
+  (U.restrict_scalars R).to_submodule = U.to_submodule.restrict_scalars R :=
+set_like.coe_injective rfl
 
-@[simp] lemma mem_res {U : subalgebra S A} {x : A} : x ∈ res R U ↔ x ∈ U := iff.rfl
+@[simp] lemma mem_restrict_scalars {U : subalgebra S A} {x : A} :
+  x ∈ restrict_scalars R U ↔ x ∈ U := iff.rfl
 
-lemma res_inj {U V : subalgebra S A} (H : res R U = res R V) : U = V :=
-ext $ λ x, by rw [← mem_res R, H, mem_res]
+lemma restrict_scalars_injective :
+  function.injective (restrict_scalars R : subalgebra S A → subalgebra R A) :=
+λ U V H, ext $ λ x, by rw [← mem_restrict_scalars R, H, mem_restrict_scalars]
 
 /-- Produces a map from `subalgebra.under`. -/
 def of_under {R A B : Type*} [comm_semiring R] [comm_semiring A] [semiring B]
@@ -254,7 +248,7 @@ variables [comm_semiring R] [comm_semiring S] [comm_semiring A]
 variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
 theorem range_under_adjoin (t : set A) :
-  (to_alg_hom R S A).range.under (algebra.adjoin _ t) = res R (algebra.adjoin S t) :=
+  (to_alg_hom R S A).range.under (algebra.adjoin _ t) = (algebra.adjoin S t).restrict_scalars R :=
 subalgebra.ext $ λ z,
 show z ∈ subsemiring.closure (set.range (algebra_map (to_alg_hom R S A).range A) ∪ t : set A) ↔
   z ∈ subsemiring.closure (set.range (algebra_map S A) ∪ t : set A),

src/field_theory/normal.lean

@@ -177,9 +177,11 @@ begin
           ←aeval_def, minpoly.aeval F z, ring_hom.map_zero] } },
   rw [←intermediate_field.to_subalgebra_le_to_subalgebra, intermediate_field.top_to_subalgebra],
   apply ge_trans (intermediate_field.algebra_adjoin_le_adjoin C S),
-  suffices : (algebra.adjoin C S).res F = (algebra.adjoin E {adjoin_root.root q}).res F,
-  { rw [adjoin_root.adjoin_root_eq_top, subalgebra.res_top, ←@subalgebra.res_top F C] at this,
-    exact top_le_iff.mpr (subalgebra.res_inj F this) },
+  suffices : (algebra.adjoin C S).restrict_scalars F
+           = (algebra.adjoin E {adjoin_root.root q}).restrict_scalars F,
+  { rw [adjoin_root.adjoin_root_eq_top, subalgebra.restrict_scalars_top,
+      ←@subalgebra.restrict_scalars_top F C] at this,
+    exact top_le_iff.mpr (subalgebra.restrict_scalars_injective F this) },
   dsimp only [S],
   rw [←finset.image_to_finset, finset.coe_image],
   apply eq.trans (algebra.adjoin_res_eq_adjoin_res F E C D

src/field_theory/splitting_field.lean

@@ -655,7 +655,7 @@ rw [roots_mul hmf0, map_sub, map_X, map_C, roots_X_sub_C, multiset.to_finset_add
     adjoin_root.adjoin_root_eq_top, algebra.map_top,
     is_scalar_tower.range_under_adjoin K (adjoin_root f.factor)
       (splitting_field_aux n f.remove_factor (nat_degree_remove_factor' hfn)),
-    ih, subalgebra.res_top] }
+    ih, subalgebra.restrict_scalars_top] }
 
 end splitting_field_aux
 
@@ -715,7 +715,8 @@ variables {K}
 instance map (f : polynomial F) [is_splitting_field F L f] :
   is_splitting_field K L (f.map $ algebra_map F K) :=
 ⟨by { rw [splits_map_iff, ← is_scalar_tower.algebra_map_eq], exact splits L f },
- subalgebra.res_inj F $ by { rw [map_map, ← is_scalar_tower.algebra_map_eq, subalgebra.res_top,
+ subalgebra.restrict_scalars_injective F $
+  by { rw [map_map, ← is_scalar_tower.algebra_map_eq, subalgebra.restrict_scalars_top,
     eq_top_iff, ← adjoin_roots L f, algebra.adjoin_le_iff],
   exact λ x hx, @algebra.subset_adjoin K _ _ _ _ _ _ hx }⟩
 
@@ -742,7 +743,7 @@ theorem mul (f g : polynomial F) (hf : f ≠ 0) (hg : g ≠ 0) [is_splitting_fie
       roots_map (algebra_map K L) ((splits_id_iff_splits $ algebra_map F K).2 $ splits K f),
       multiset.to_finset_map, finset.coe_image, algebra.adjoin_algebra_map, adjoin_roots,
       algebra.map_top, is_scalar_tower.range_under_adjoin, ← map_map, adjoin_roots,
-      subalgebra.res_top]⟩
+      subalgebra.restrict_scalars_top]⟩
 
 end scalar_tower
 

src/ring_theory/algebra_tower.lean

@@ -81,10 +81,11 @@ theorem adjoin_algebra_map (R : Type u) (S : Type v) (A : Type w)
 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⟩)
 
-lemma adjoin_res (C D E : Type*) [comm_semiring C] [comm_semiring D] [comm_semiring E]
+lemma adjoin_restrict_scalars (C D E : Type*) [comm_semiring C] [comm_semiring D] [comm_semiring E]
   [algebra C D] [algebra C E] [algebra D E] [is_scalar_tower C D E] (S : set E) :
-(algebra.adjoin D S).res C = ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)).under
-  (algebra.adjoin ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)) S) :=
+(algebra.adjoin D S).restrict_scalars C =
+  ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)).under
+    (algebra.adjoin ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)) S) :=
 begin
   suffices : set.range (algebra_map D E) =
     set.range (algebra_map ((⊤ : subalgebra C D).map (is_scalar_tower.to_alg_hom C D E)) E),
@@ -101,11 +102,12 @@ lemma adjoin_res_eq_adjoin_res (C D E F : Type*) [comm_semiring C] [comm_semirin
   [comm_semiring E] [comm_semiring F] [algebra C D] [algebra C E] [algebra C F] [algebra D F]
   [algebra E F] [is_scalar_tower C D F] [is_scalar_tower C E F] {S : set D} {T : set E}
   (hS : algebra.adjoin C S = ⊤) (hT : algebra.adjoin C T = ⊤) :
-(algebra.adjoin E (algebra_map D F '' S)).res C =
-  (algebra.adjoin D (algebra_map E F '' T)).res C :=
-by { rw [adjoin_res, adjoin_res, ←hS, ←hT, ←algebra.adjoin_image, ←algebra.adjoin_image,
-  ←alg_hom.coe_to_ring_hom, ←alg_hom.coe_to_ring_hom, is_scalar_tower.coe_to_alg_hom,
-  is_scalar_tower.coe_to_alg_hom, ←adjoin_union_eq_under, ←adjoin_union_eq_under, set.union_comm] }
+(algebra.adjoin E (algebra_map D F '' S)).restrict_scalars C =
+  (algebra.adjoin D (algebra_map E F '' T)).restrict_scalars C :=
+by rw [adjoin_restrict_scalars, adjoin_restrict_scalars, ←hS, ←hT, ←algebra.adjoin_image,
+  ←algebra.adjoin_image, ←alg_hom.coe_to_ring_hom, ←alg_hom.coe_to_ring_hom,
+  is_scalar_tower.coe_to_alg_hom, is_scalar_tower.coe_to_alg_hom, ←adjoin_union_eq_under,
+  ←adjoin_union_eq_under, set.union_comm]
 
 end algebra
 
@@ -118,7 +120,7 @@ lemma algebra.fg_trans' {R S A : Type*} [comm_ring R] [comm_ring S] [comm_ring A
 let ⟨s, hs⟩ := hRS, ⟨t, ht⟩ := hSA in ⟨s.image (algebra_map S A) ∪ t,
 by rw [finset.coe_union, finset.coe_image, algebra.adjoin_union_eq_under,
   algebra.adjoin_algebra_map, hs, algebra.map_top, is_scalar_tower.range_under_adjoin, ht,
-  subalgebra.res_top]⟩
+  subalgebra.restrict_scalars_top]⟩
 end
 
 section algebra_map_coeffs