refactor(field_theory/intermediate_field): introduce `restrict_scalar…

…s` which replaces `lift2` (#15191)

This brings the API in line with `submodule` and `subalgebra` by removing `intermediate_field.lift2` and `intermediate_field.has_lift2`, and replacing them with `intermediate_field.restrict_scalars`. This definition is strictly more general than the previous `intermediate_field.lift2` definition was. A few downstream lemma statements have been generalized in the same way.

The handful of API lemmas for `restrict_scalars` that this adds were already missing for `lift2`.

`intermediate_field.lift2_alg_equiv` has been removed since we didn't appear to have anything similar for `subalgebra` or `submodule`, but it's possible I missed it. At any rate, it's only needed in one proof, and we can just use `show` or `refl` instead.

Note that `(↑x : intermediate_field F E)` is not actually a shorter spelling than `x.restrict_scalars F`, especially when `E` is more than a single character.

Finally this renames `lift1` to `lift` now that no ambiguity remains.

src/algebra/algebra/tower.lean

@@ -212,8 +212,8 @@ variables (R) {S A B} [comm_semiring R] [comm_semiring S] [semiring A] [semiring
 variables [algebra R S] [algebra S A] [algebra R A] [algebra S B] [algebra R B]
 variables [is_scalar_tower R S A] [is_scalar_tower R S B]
 
-/-- Given a scalar tower `R`, `S`, `A` of algebras, reinterpret an `S`-subalgebra of `A` an as an
-`R`-subalgebra. -/
+/-- Given a tower `A / ↥U / S / R` of algebras, where `U` is an `S`-subalgebra of `A`, reinterpret
+`U` as an `R`-subalgebra of `A`. -/
 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 }

src/field_theory/adjoin.lean

@@ -180,12 +180,14 @@ This is the intermediate field version of `subalgebra.top_equiv`. -/
 @[simp] lemma top_equiv_symm_apply_coe (a : E) :
   ↑((top_equiv.symm) a : (⊤ : intermediate_field F E)) = a := rfl
 
-@[simp] lemma coe_bot_eq_self (K : intermediate_field F E) : ↑(⊥ : intermediate_field K E) = K :=
-by { ext, rw [mem_lift2, mem_bot], exact set.ext_iff.mp subtype.range_coe x }
+@[simp] lemma restrict_scalars_bot_eq_self (K : intermediate_field F E) :
+  (⊥ : intermediate_field K E).restrict_scalars _ = K :=
+by { ext, rw [mem_restrict_scalars, mem_bot], exact set.ext_iff.mp subtype.range_coe x }
 
-@[simp] lemma coe_top_eq_top (K : intermediate_field F E) :
-  ↑(⊤ : intermediate_field K E) = (⊤ : intermediate_field F E) :=
-set_like.ext_iff.mpr $ λ _, mem_lift2.trans (iff_of_true mem_top mem_top)
+@[simp] lemma restrict_scalars_top {K : Type*} [field K] [algebra K E] [algebra K F]
+  [is_scalar_tower K F E] :
+  (⊤ : intermediate_field F E).restrict_scalars K = ⊤ :=
+rfl
 
 end lattice
 
@@ -251,7 +253,8 @@ lemma adjoin_subset_adjoin_iff {F' : Type*} [field F'] [algebra F' E]
   λ ⟨hF, hS⟩, subfield.closure_le.mpr (set.union_subset hF hS)⟩
 
 /-- `F[S][T] = F[S ∪ T]` -/
-lemma adjoin_adjoin_left (T : set E) : ↑(adjoin (adjoin F S) T) = adjoin F (S ∪ T) :=
+lemma adjoin_adjoin_left (T : set E) :
+  (adjoin (adjoin F S) T).restrict_scalars _ = adjoin F (S ∪ T) :=
 begin
   rw set_like.ext'_iff,
   change ↑(adjoin (adjoin F S) T) = _,
@@ -273,7 +276,7 @@ le_antisymm
 
 /-- `F[S][T] = F[T][S]` -/
 lemma adjoin_adjoin_comm (T : set E) :
-  ↑(adjoin (adjoin F S) T) = (↑(adjoin (adjoin F T) S) : (intermediate_field F E)) :=
+  (adjoin (adjoin F S) T).restrict_scalars F = (adjoin (adjoin F T) S).restrict_scalars F :=
 by rw [adjoin_adjoin_left, adjoin_adjoin_left, set.union_comm]
 
 lemma adjoin_map {E' : Type*} [field E'] [algebra F E'] (f : E →ₐ[F] E') :
@@ -356,10 +359,10 @@ by { conv_rhs { rw ← adjoin_simple.algebra_map_gen F α },
      rw is_integral_algebra_map_iff (algebra_map F⟮α⟯ E).injective,
      apply_instance }
 
-lemma adjoin_simple_adjoin_simple (β : E) : ↑F⟮α⟯⟮β⟯ = F⟮α, β⟯ :=
+lemma adjoin_simple_adjoin_simple (β : E) : F⟮α⟯⟮β⟯.restrict_scalars F = F⟮α, β⟯ :=
 adjoin_adjoin_left _ _ _
 
-lemma adjoin_simple_comm (β : E) : ↑F⟮α⟯⟮β⟯ = (↑F⟮β⟯⟮α⟯ : intermediate_field F E) :=
+lemma adjoin_simple_comm (β : E) : F⟮α⟯⟮β⟯.restrict_scalars F = F⟮β⟯⟮α⟯.restrict_scalars F :=
 adjoin_adjoin_comm _ _ _
 
 -- TODO: develop the API for `subalgebra.is_field_of_algebraic` so it can be used here
@@ -615,7 +618,8 @@ lemma fg_of_noetherian (S : intermediate_field F E)
 S.fg_of_fg_to_subalgebra S.to_subalgebra.fg_of_noetherian
 
 lemma induction_on_adjoin_finset (S : finset E) (P : intermediate_field F E → Prop) (base : P ⊥)
-  (ih : ∀ (K : intermediate_field F E) (x ∈ S), P K → P ↑K⟮x⟯) : P (adjoin F ↑S) :=
+  (ih : ∀ (K : intermediate_field F E) (x ∈ S), P K → P (K⟮x⟯.restrict_scalars F)) :
+  P (adjoin F ↑S) :=
 begin
   apply finset.induction_on' S,
   { exact base },
@@ -625,15 +629,15 @@ begin
 end
 
 lemma induction_on_adjoin_fg (P : intermediate_field F E → Prop)
-  (base : P ⊥) (ih : ∀ (K : intermediate_field F E) (x : E), P K → P ↑K⟮x⟯)
+  (base : P ⊥) (ih : ∀ (K : intermediate_field F E) (x : E), P K → P (K⟮x⟯.restrict_scalars F))
   (K : intermediate_field F E) (hK : K.fg) : P K :=
 begin
   obtain ⟨S, rfl⟩ := hK,
   exact induction_on_adjoin_finset S P base (λ K x _ hK, ih K x hK),
 end
 
 lemma induction_on_adjoin [fd : finite_dimensional F E] (P : intermediate_field F E → Prop)
-  (base : P ⊥) (ih : ∀ (K : intermediate_field F E) (x : E), P K → P ↑K⟮x⟯)
+  (base : P ⊥) (ih : ∀ (K : intermediate_field F E) (x : E), P K → P (K⟮x⟯.restrict_scalars F))
   (K : intermediate_field F E) : P K :=
 begin
   letI : is_noetherian F E := is_noetherian.iff_fg.2 infer_instance,
@@ -765,7 +769,7 @@ let key : (minpoly x.1 s).splits x.2.to_ring_hom :=
   splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero h1))
   ((splits_map_iff _ _).mpr (by {convert h2, exact ring_hom.ext (λ y, x.2.commutes y)}))
   (minpoly.dvd_map_of_is_scalar_tower _ _ _) in
-⟨↑x.1⟮s⟯, (@alg_hom_equiv_sigma F x.1 (↑x.1⟮s⟯ : intermediate_field F E) K _ _ _ _ _ _ _
+⟨x.1⟮s⟯.restrict_scalars F, (@alg_hom_equiv_sigma F x.1 (x.1⟮s⟯.restrict_scalars F) K _ _ _ _ _ _ _
   (intermediate_field.algebra x.1⟮s⟯) (is_scalar_tower.of_algebra_map_eq (λ _, rfl))).inv_fun
   ⟨x.2, (@alg_hom_adjoin_integral_equiv x.1 _ E _ _ s K _ x.2.to_ring_hom.to_algebra
   h3).inv_fun ⟨root_of_splits x.2.to_ring_hom key (ne_of_gt (minpoly.degree_pos h3)), by

src/field_theory/galois.lean

@@ -329,23 +329,28 @@ end
 
 variables {F} {E} {p : F[X]}
 
-lemma of_separable_splitting_field_aux [hFE : finite_dimensional F E]
-  [sp : p.is_splitting_field F E] (hp : p.separable) (K : intermediate_field F E) {x : E}
-  (hx : x ∈ (p.map (algebra_map F E)).roots) :
-  fintype.card ((↑K⟮x⟯ : intermediate_field F E) →ₐ[F] E) =
+lemma of_separable_splitting_field_aux
+  [hFE : finite_dimensional F E]
+  [sp : p.is_splitting_field F E] (hp : p.separable)
+  (K : Type*) [field K] [algebra F K] [algebra K E] [is_scalar_tower F K E]
+  {x : E} (hx : x ∈ (p.map (algebra_map F E)).roots)
+  -- these are both implied by `hFE`, but as they carry data this makes the lemma more general
+  [fintype (K →ₐ[F] E)] [fintype (K⟮x⟯.restrict_scalars F →ₐ[F] E)] :
+  fintype.card (K⟮x⟯.restrict_scalars F →ₐ[F] E) =
     fintype.card (K →ₐ[F] E) * finrank K K⟮x⟯ :=
 begin
   have h : is_integral K x := is_integral_of_is_scalar_tower x
     (is_integral_of_noetherian (is_noetherian.iff_fg.2 hFE) x),
   have h1 : p ≠ 0 := λ hp, by rwa [hp, polynomial.map_zero, polynomial.roots_zero] at hx,
   have h2 : (minpoly K x) ∣ p.map (algebra_map F K),
   { apply minpoly.dvd,
-    rw [polynomial.aeval_def, polynomial.eval₂_map, ←polynomial.eval_map],
+    rw [polynomial.aeval_def, polynomial.eval₂_map, ←polynomial.eval_map,
+      ←is_scalar_tower.algebra_map_eq],
     exact (polynomial.mem_roots (polynomial.map_ne_zero h1)).mp hx },
-  let key_equiv : ((↑K⟮x⟯ : intermediate_field F E) →ₐ[F] E) ≃ Σ (f : K →ₐ[F] E),
-    @alg_hom K K⟮x⟯ E _ _ _ _ (ring_hom.to_algebra f) :=
-  equiv.trans (alg_equiv.arrow_congr (intermediate_field.lift2_alg_equiv K⟮x⟯) (alg_equiv.refl))
-    alg_hom_equiv_sigma,
+  let key_equiv : (K⟮x⟯.restrict_scalars F →ₐ[F] E) ≃ Σ (f : K →ₐ[F] E),
+    @alg_hom K K⟮x⟯ E _ _ _ _ (ring_hom.to_algebra f),
+  { change (K⟮x⟯ →ₐ[F] E) ≃ Σ (f : K →ₐ[F] E), _,
+    exact alg_hom_equiv_sigma },
   haveI : Π (f : K →ₐ[F] E), fintype (@alg_hom K K⟮x⟯ E _ _ _ _ (ring_hom.to_algebra f)) := λ f, by
   { apply fintype.of_injective (sigma.mk f) (λ _ _ H, eq_of_heq ((sigma.mk.inj H).2)),
     exact fintype.of_equiv _ key_equiv },
@@ -391,7 +396,8 @@ begin
   rw [of_separable_splitting_field_aux hp K (multiset.mem_to_finset.mp hx),
     hK, finrank_mul_finrank],
   symmetry,
-  exact linear_equiv.finrank_eq (alg_equiv.to_linear_equiv (intermediate_field.lift2_alg_equiv _))
+  refine linear_equiv.finrank_eq _,
+  refl,
 end
 
 /--Equivalent characterizations of a Galois extension of finite degree-/

src/field_theory/intermediate_field.lean

@@ -18,15 +18,14 @@ i.e. it is a `subfield L` and a `subalgebra K L`.
 
 ## Main definitions
 
- * `intermediate_field K L` : the type of intermediate fields between `K` and `L`.
-
- * `subalgebra.to_intermediate_field`: turns a subalgebra closed under `⁻¹`
-   into an intermediate field
-
- * `subfield.to_intermediate_field`: turns a subfield containing the image of `K`
-   into an intermediate field
-
+* `intermediate_field K L` : the type of intermediate fields between `K` and `L`.
+* `subalgebra.to_intermediate_field`: turns a subalgebra closed under `⁻¹`
+  into an intermediate field
+* `subfield.to_intermediate_field`: turns a subfield containing the image of `K`
+  into an intermediate field
 * `intermediate_field.map`: map an intermediate field along an `alg_hom`
+* `intermediate_field.restrict_scalars`: restrict the scalars of an intermediate field to a smaller
+  field in a tower of fields.
 
 ## Implementation notes
 
@@ -376,44 +375,46 @@ variables {S}
 section tower
 
 /-- Lift an intermediate_field of an intermediate_field -/
-def lift1 {F : intermediate_field K L} (E : intermediate_field K F) : intermediate_field K L :=
-  map E (val F)
+def lift {F : intermediate_field K L} (E : intermediate_field K F) : intermediate_field K L :=
+map E (val F)
 
-/-- Lift an intermediate_field of an intermediate_field -/
-def lift2 {F : intermediate_field K L} (E : intermediate_field F L) : intermediate_field K L :=
+instance has_lift {F : intermediate_field K L} :
+  has_lift_t (intermediate_field K F) (intermediate_field K L) := ⟨lift⟩
+
+section restrict_scalars
+variables (K) [algebra L' L] [is_scalar_tower K L' L]
+
+/-- Given a tower `L / ↥E / L' / K` of field extensions, where `E` is an `L'`-intermediate field of
+`L`, reinterpret `E` as a `K`-intermediate field of `L`. -/
+def restrict_scalars (E : intermediate_field L' L) :
+  intermediate_field K L :=
 { carrier := E.carrier,
-  zero_mem' := zero_mem E,
-  add_mem' := λ x y (hx : x ∈ E), add_mem hx,
-  neg_mem' := λ x (hx : x ∈ E), neg_mem hx,
-  one_mem' := one_mem E,
-  mul_mem' := λ x y (hx : x ∈ E), mul_mem hx,
-  inv_mem' := λ x (hx : x ∈ E), inv_mem hx,
-  algebra_map_mem' := λ x, algebra_map_mem E (algebra_map K F x) }
+  ..E.to_subfield,
+  ..E.to_subalgebra.restrict_scalars K }
 
-instance has_lift1 {F : intermediate_field K L} :
-  has_lift_t (intermediate_field K F) (intermediate_field K L) := ⟨lift1⟩
+@[simp] lemma coe_restrict_scalars {E : intermediate_field L' L} :
+  (restrict_scalars K E : set L) = (E : set L) := rfl
 
-instance has_lift2 {F : intermediate_field K L} :
-  has_lift_t (intermediate_field F L) (intermediate_field K L) := ⟨lift2⟩
+@[simp] lemma restrict_scalars_to_subalgebra {E : intermediate_field L' L} :
+  (E.restrict_scalars K).to_subalgebra = E.to_subalgebra.restrict_scalars K :=
+set_like.coe_injective rfl
 
-@[simp] lemma mem_lift2 {F : intermediate_field K L} {E : intermediate_field F L} {x : L} :
-  x ∈ (↑E : intermediate_field K L) ↔ x ∈ E := iff.rfl
+@[simp] lemma restrict_scalars_to_subfield {E : intermediate_field L' L} :
+  (E.restrict_scalars K).to_subfield = E.to_subfield :=
+set_like.coe_injective rfl
 
-/-- This was formerly an instance called `lift2_alg`, but an instance above already provides it. -/
-example {F : intermediate_field K L} {E : intermediate_field F L} : algebra K E :=
-by apply_instance
+@[simp] lemma mem_restrict_scalars {E : intermediate_field L' L} {x : L} :
+  x ∈ restrict_scalars K E ↔ x ∈ E := iff.rfl
 
-lemma lift2_algebra_map {F : intermediate_field K L} {E : intermediate_field F L} :
-  algebra_map K E = (algebra_map F E).comp (algebra_map K F) := rfl
+lemma restrict_scalars_injective :
+  function.injective (restrict_scalars K : intermediate_field L' L → intermediate_field K L) :=
+λ U V H, ext $ λ x, by rw [← mem_restrict_scalars K, H, mem_restrict_scalars]
 
-instance lift2_tower {F : intermediate_field K L} {E : intermediate_field F L} :
-  is_scalar_tower K F E :=
-E.is_scalar_tower
+end restrict_scalars
 
-/-- `lift2` is isomorphic to the original `intermediate_field`. -/
-def lift2_alg_equiv {F : intermediate_field K L} (E : intermediate_field F L) :
-  (↑E : intermediate_field K L) ≃ₐ[K] E :=
-alg_equiv.refl
+/-- This was formerly an instance called `lift2_alg`, but an instance above already provides it. -/
+example {F : intermediate_field K L} {E : intermediate_field F L} : algebra K E :=
+by apply_instance
 
 end tower
 

src/field_theory/primitive_element.lean

@@ -178,7 +178,7 @@ begin
   rcases is_empty_or_nonempty (fintype F) with F_inf|⟨⟨F_finite⟩⟩,
   { let P : intermediate_field F E → Prop := λ K, ∃ α : E, F⟮α⟯ = K,
     have base : P ⊥ := ⟨0, adjoin_zero⟩,
-    have ih : ∀ (K : intermediate_field F E) (x : E), P K → P ↑K⟮x⟯,
+    have ih : ∀ (K : intermediate_field F E) (x : E), P K → P (K⟮x⟯.restrict_scalars F),
     { intros K β hK,
       cases hK with α hK,
       rw [←hK, adjoin_simple_adjoin_simple],