chore(ring_theory/power_series/well_known): generalize (#5491)

* generalize `power_series.exp`, `power_series.cos`, and `power_series.sin` to a `ℚ`-algebra;
* define `alg_hom.mk'`;
* rename `alg_hom_nat` to `ring_hom.to_nat_alg_hom`;
* drop `alg_hom_int` (was equal to `ring_hom.to_int_alg_hom`);
* add `ring_hom.to_rat_alg_hom`.

src/algebra/algebra/basic.lean

@@ -197,7 +197,7 @@ The canonical ring homomorphism `algebra_map R A : R →* A` for any `R`-algebra
 packaged as an `R`-linear map.
 -/
 protected def linear_map : R →ₗ[R] A :=
-{ map_smul' := λ x y, begin dsimp, simp [algebra.smul_def], end,
+{ map_smul' := λ x y, by simp [algebra.smul_def],
   ..algebra_map R A }
 
 @[simp]
@@ -477,6 +477,14 @@ lemma map_finsupp_sum {α : Type*} [has_zero α] {ι : Type*} (f : ι →₀ α)
 @[simp] lemma map_bit1 (x) : φ (bit1 x) = bit1 (φ x) :=
 φ.to_ring_hom.map_bit1 x
 
+/-- If a `ring_hom` is `R`-linear, then it is an `alg_hom`. -/
+def mk' (f : A →+* B) (h : ∀ (c : R) x, f (c • x) = c • f x) : A →ₐ[R] B :=
+{ to_fun := f,
+  commutes' := λ c, by simp only [algebra.algebra_map_eq_smul_one, h, f.map_one],
+  .. f }
+
+@[simp] lemma coe_mk' (f : A →+* B) (h : ∀ (c : R) x, f (c • x) = c • f x) : ⇑(mk' f h) = f := rfl
+
 section
 
 variables (R A)
@@ -971,6 +979,32 @@ def comap : algebra.comap R S A →ₐ[R] algebra.comap R S B :=
 
 end alg_hom
 
+namespace ring_hom
+
+variables {R S : Type*}
+
+/-- Reinterpret a `ring_hom` as an `ℕ`-algebra homomorphism. -/
+def to_nat_alg_hom [semiring R] [semiring S] [algebra ℕ R] [algebra ℕ S] (f : R →+* S) :
+  R →ₐ[ℕ] S :=
+{ to_fun := f, commutes' := λ n, by simp, .. f }
+
+/-- Reinterpret a `ring_hom` as a `ℤ`-algebra homomorphism. -/
+def to_int_alg_hom [ring R] [ring S] [algebra ℤ R] [algebra ℤ S] (f : R →+* S) :
+  R →ₐ[ℤ] S :=
+{ commutes' := λ n, by simp, .. f }
+
+@[simp] lemma map_rat_algebra_map [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] (f : R →+* S)
+  (r : ℚ) :
+  f (algebra_map ℚ R r) = algebra_map ℚ S r :=
+ring_hom.ext_iff.1 (subsingleton.elim (f.comp (algebra_map ℚ R)) (algebra_map ℚ S)) r
+
+/-- Reinterpret a `ring_hom` as a `ℚ`-algebra homomorphism. -/
+def to_rat_alg_hom [ring R] [ring S] [algebra ℚ R] [algebra ℚ S] (f : R →+* S) :
+  R →ₐ[ℚ] S :=
+{ commutes' := f.map_rat_algebra_map, .. f }
+
+end ring_hom
+
 namespace rat
 
 instance algebra_rat {α} [division_ring α] [char_zero α] : algebra ℚ α :=
@@ -1065,18 +1099,11 @@ section nat
 
 variables (R : Type*) [semiring R]
 
-/-- Reinterpret a `ring_hom` as an `ℕ`-algebra homomorphism. -/
-def alg_hom_nat
-  {R : Type u} [semiring R] [algebra ℕ R]
-  {S : Type v} [semiring S] [algebra ℕ S]
-  (f : R →+* S) : R →ₐ[ℕ] S :=
-{ commutes' := λ i, show f _ = _, by simp, .. f }
-
 /-- Semiring ⥤ ℕ-Alg -/
 instance algebra_nat : algebra ℕ R :=
 { commutes' := nat.cast_commute,
   smul_def' := λ _ _, nsmul_eq_mul _ _,
-  .. nat.cast_ring_hom R }
+  to_ring_hom := nat.cast_ring_hom R }
 
 section span_nat
 open submodule
@@ -1098,25 +1125,11 @@ section int
 
 variables (R : Type*) [ring R]
 
-/-- Reinterpret a `ring_hom` as a `ℤ`-algebra homomorphism. -/
-def alg_hom_int
-  {R : Type u} [comm_ring R] [algebra ℤ R]
-  {S : Type v} [comm_ring S] [algebra ℤ S]
-  (f : R →+* S) : R →ₐ[ℤ] S :=
-{ commutes' := λ i, show f _ = _, by simp, .. f }
-
 /-- Ring ⥤ ℤ-Alg -/
 instance algebra_int : algebra ℤ R :=
 { commutes' := int.cast_commute,
   smul_def' := λ _ _, gsmul_eq_mul _ _,
-  .. int.cast_ring_hom R }
-
-/--
-Promote a ring homomorphisms to a `ℤ`-algebra homomorphism.
--/
-def ring_hom.to_int_alg_hom {R S : Type*} [ring R] [ring S] (f : R →+* S) : R →ₐ[ℤ] S :=
-{ commutes' := λ n, by simp,
-  .. f }
+  to_ring_hom := int.cast_ring_hom R }
 
 variables {R}
 

src/ring_theory/power_series/well_known.lean

@@ -54,30 +54,30 @@ end ring
 
 section field
 
-variables (k k' : Type*) [field k] [field k']
+variables (A A' : Type*) [ring A] [ring A'] [algebra ℚ A] [algebra ℚ A']
 
 open_locale nat
 
 /-- Power series for the exponential function at zero. -/
-def exp : power_series k := mk $ λ n, 1 / n!
+def exp : power_series A := mk $ λ n, algebra_map ℚ A (1 / n!)
 
 /-- Power series for the sine function at zero. -/
-def sin : power_series k :=
-mk $ λ n, if even n then 0 else (-1) ^ (n / 2) / n!
+def sin : power_series A :=
+mk $ λ n, if even n then 0 else algebra_map ℚ A ((-1) ^ (n / 2) / n!)
 
 /-- Power series for the cosine function at zero. -/
-def cos : power_series k :=
-mk $ λ n, if even n then (-1) ^ (n / 2) / n! else 0
+def cos : power_series A :=
+mk $ λ n, if even n then algebra_map ℚ A ((-1) ^ (n / 2) / n!) else 0
 
-variables {k k'} (n : ℕ) (f : k →+* k')
+variables {A A'} (n : ℕ) (f : A →+* A')
 
-@[simp] lemma coeff_exp : coeff k n (exp k) = 1 / n! := coeff_mk _ _
+@[simp] lemma coeff_exp : coeff A n (exp A) = algebra_map ℚ A (1 / n!) := coeff_mk _ _
 
-@[simp] lemma map_exp : map f (exp k) = exp k' := by { ext, simp [f.map_inv] }
+@[simp] lemma map_exp : map (f : A →+* A') (exp A) = exp A' := by { ext, simp }
 
-@[simp] lemma map_sin : map f (sin k) = sin k' := by { ext, simp [sin, apply_ite f, f.map_div] }
+@[simp] lemma map_sin : map f (sin A) = sin A' := by { ext, simp [sin, apply_ite f] }
 
-@[simp] lemma map_cos : map f (cos k) = cos k' := by { ext, simp [cos, apply_ite f, f.map_div] }
+@[simp] lemma map_cos : map f (cos A) = cos A' := by { ext, simp [cos, apply_ite f] }
 
 end field