[Merged by Bors] - feat(algebra/algebra/{basic,tower}): add alg_equiv.comap and alg_equiv.restrict_scalars

src/algebra/algebra/basic.lean

@@ -1041,19 +1041,28 @@ theorem to_comap_apply (x) : to_comap R S A x = algebra_map S A x := rfl
 
 end algebra
 
-namespace alg_hom
+section
 
 variables {R : Type u} {S : Type v} {A : Type w} {B : Type u₁}
 variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B]
-variables [algebra R S] [algebra S A] [algebra S B] (φ : A →ₐ[S] B)
+variables [algebra R S] [algebra S A] [algebra S B]
 include R
 
-/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
-def comap : algebra.comap R S A →ₐ[R] algebra.comap R S B :=
+/-- R ⟶ S induces S-Alg ⥤ R-Alg.#print
+
+See `alg_hom.restrict_base` for the version that uses `is_scalar_tower` instead of `comap`. -/
+def alg_hom.comap (φ : A →ₐ[S] B) : algebra.comap R S A →ₐ[R] algebra.comap R S B :=
 { commutes' := λ r, φ.commutes (algebra_map R S r)
   ..φ }
 
-end alg_hom
+/-- `alg_hom.comap` for `alg_equiv`.
+
+See `alg_equiv.restrict_base` for the version that uses `is_scalar_tower` instead of `comap`. -/
+def alg_equiv.comap (φ : A ≃ₐ[S] B) : algebra.comap R S A ≃ₐ[R] algebra.comap R S B :=
+{ commutes' := λ r, φ.commutes (algebra_map R S r)
+  ..φ }
+
+end
 
 namespace ring_hom
 

src/algebra/algebra/tower.lean

@@ -127,17 +127,6 @@ ring_hom.ext $ λ _, rfl
 rfl
 
 variables (R) {S A B}
-/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
-def restrict_base (f : A →ₐ[S] B) : A →ₐ[R] B :=
-{ commutes' := λ r, by { rw [algebra_map_apply R S A, algebra_map_apply R S B],
-    exact f.commutes (algebra_map R S r) },
-  .. (f : A →+* B) }
-
-lemma restrict_base_apply (f : A →ₐ[S] B) (x : A) : restrict_base R f x = f x := rfl
-
-@[simp] lemma coe_restrict_base (f : A →ₐ[S] B) : (restrict_base R f : A →+* B) = f := rfl
-
-@[simp] lemma coe_restrict_base' (f : A →ₐ[S] B) : (restrict_base R f : A → B) = f := rfl
 
 instance right : is_scalar_tower S A A :=
 ⟨λ x y z, by rw [smul_eq_mul, smul_eq_mul, algebra.smul_mul_assoc]⟩
@@ -176,6 +165,51 @@ end division_ring
 
 end is_scalar_tower
 
+section homs
+
+variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B]
+variables [algebra R S] [algebra S A] [algebra S B]
+variables [algebra R A] [algebra R B]
+variables [is_scalar_tower R S A] [is_scalar_tower R S B]
+
+variables (R) {A S B}
+
+open is_scalar_tower
+
+namespace alg_hom
+
+/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
+def restrict_base (f : A →ₐ[S] B) : A →ₐ[R] B :=
+{ commutes' := λ r, by { rw [algebra_map_apply R S A, algebra_map_apply R S B],
+    exact f.commutes (algebra_map R S r) },
+  .. (f : A →+* B) }
+
+lemma restrict_base_apply (f : A →ₐ[S] B) (x : A) : f.restrict_base R x = f x := rfl
+
+@[simp] lemma coe_restrict_base (f : A →ₐ[S] B) : (f.restrict_base R : A →+* B) = f := rfl
+
+@[simp] lemma coe_restrict_base' (f : A →ₐ[S] B) : (restrict_base R f : A → B) = f := rfl
+
+end alg_hom
+
+namespace alg_equiv
+
+/-- R ⟶ S induces S-Alg ⥤ R-Alg -/
+def restrict_base (f : A ≃ₐ[S] B) : A ≃ₐ[R] B :=
+{ commutes' := λ r, by { rw [algebra_map_apply R S A, algebra_map_apply R S B],
+    exact f.commutes (algebra_map R S r) },
+  .. (f : A ≃+* B) }
+
+lemma restrict_base_apply (f : A ≃ₐ[S] B) (x : A) : f.restrict_base R x = f x := rfl
+
+@[simp] lemma coe_restrict_base (f : A ≃ₐ[S] B) : (f.restrict_base R : A ≃+* B) = f := rfl
+
+@[simp] lemma coe_restrict_base' (f : A ≃ₐ[S] B) : (restrict_base R f : A → B) = f := rfl
+
+end alg_equiv
+
+end homs
+
 namespace subalgebra
 
 open is_scalar_tower

src/field_theory/normal.lean

@@ -158,7 +158,7 @@ begin
   haveI : is_scalar_tower F C D := of_algebra_map_eq (λ x, adjoin_root.lift_of.symm),
   haveI : is_scalar_tower F C E := of_algebra_map_eq (λ x, adjoin_root.lift_of.symm),
   suffices : nonempty (D →ₐ[C] E),
-  { exact nonempty.map (restrict_base F) this },
+  { exact nonempty.map (alg_hom.restrict_base F) this },
   let S : set D := ((p.map (algebra_map F E)).roots.map (algebra_map E D)).to_finset,
   suffices : ⊤ ≤ intermediate_field.adjoin C S,
   { refine intermediate_field.alg_hom_mk_adjoin_splits' (top_le_iff.mp this) (λ y hy, _),
@@ -257,7 +257,7 @@ variables {F} {K} (E : Type*) [field E] [algebra F E] [algebra K E] [is_scalar_t
 /-- If `E/K/F` is a tower of fields with `E/F` normal then we can lift
   an algebra homomorphism `ϕ : K →ₐ[F] K` to `ϕ.lift_normal E : E →ₐ[F] E`. -/
 noncomputable def alg_hom.lift_normal [h : normal F E] : E →ₐ[F] E :=
-@restrict_base F K E E _ _ _ _ _ _
+@alg_hom.restrict_base F K E E _ _ _ _ _ _
   ((is_scalar_tower.to_alg_hom F K E).comp ϕ).to_ring_hom.to_algebra _ _ _ _
   (nonempty.some (@intermediate_field.alg_hom_mk_adjoin_splits' K E E _ _ _ _
   ((is_scalar_tower.to_alg_hom F K E).comp ϕ).to_ring_hom.to_algebra ⊤ rfl

src/ring_theory/algebra_tower.lean

@@ -262,8 +262,8 @@ variables {B}
 def alg_hom_equiv_sigma :
   (C →ₐ[A] D) ≃ Σ (f : B →ₐ[A] D), @alg_hom B C D _ _ _ _ f.to_ring_hom.to_algebra :=
 { to_fun := λ f, ⟨f.restrict_domain B, f.extend_scalars B⟩,
-  inv_fun := λ fg, @is_scalar_tower.restrict_base A _ _ _ _ _ _ _ _ _
-    fg.1.to_ring_hom.to_algebra _ _ _ _ fg.2,
+  inv_fun := λ fg,
+    let alg := fg.1.to_ring_hom.to_algebra in by exactI fg.2.restrict_base A,
   left_inv := λ f, by { dsimp only, ext, refl },
   right_inv :=
   begin