From d840349db150e13809a02a4f3021cbf0850c9b1c Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Tue, 11 Oct 2022 03:45:35 +0000 Subject: [PATCH] feat(algebra/algebra/basic): make algebra_map a low prio has_lift_t (#16567) Make `algebra_map` a coercion (or more precisely a `has_lift_t`). I have an example where making algebra_map a coercion makes a lot of code far less messy and I'm wondering whether it's a good idea in general. Co-authored-by: Vierkantor --- src/algebra/algebra/basic.lean | 68 +++++++++++++++++++++++++ src/data/complex/is_R_or_C.lean | 10 ++-- src/topology/algebra/uniform_field.lean | 3 +- 3 files changed, 74 insertions(+), 7 deletions(-) diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index c81a009eb39b1..29a545f6e3660 100644 --- a/src/algebra/algebra/basic.lean +++ b/src/algebra/algebra/basic.lean @@ -124,6 +124,74 @@ end prio def algebra_map (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] : R →+* A := algebra.to_ring_hom +namespace algebra_map + +def has_lift_t (R A : Type*) [comm_semiring R] [semiring A] [algebra R A] : + has_lift_t R A := ⟨λ r, algebra_map R A r⟩ + +attribute [instance, priority 900] algebra_map.has_lift_t + +section comm_semiring_semiring + +variables {R A : Type*} [comm_semiring R] [semiring A] [algebra R A] + +@[simp, norm_cast] lemma coe_zero : (↑(0 : R) : A) = 0 := map_zero (algebra_map R A) +@[simp, norm_cast] lemma coe_one : (↑(1 : R) : A) = 1 := map_one (algebra_map R A) +@[norm_cast] lemma coe_add (a b : R) : (↑(a + b : R) : A) = ↑a + ↑b := +map_add (algebra_map R A) a b +@[norm_cast] lemma coe_mul (a b : R) : (↑(a * b : R) : A) = ↑a * ↑b := +map_mul (algebra_map R A) a b +@[norm_cast] lemma coe_pow (a : R) (n : ℕ) : (↑(a ^ n : R) : A) = ↑a ^ n := +map_pow (algebra_map R A) _ _ + +end comm_semiring_semiring + +section comm_ring_ring + +variables {R A : Type*} [comm_ring R] [ring A] [algebra R A] + +@[norm_cast] lemma coe_neg (x : R) : (↑(-x : R) : A) = -↑x := +map_neg (algebra_map R A) x + +end comm_ring_ring + +section comm_semiring_comm_semiring + +variables {R A : Type*} [comm_semiring R] [comm_semiring A] [algebra R A] + +open_locale big_operators + +-- direct to_additive fails because of some mix-up with polynomials +@[norm_cast] lemma coe_prod {ι : Type*} {s : finset ι} (a : ι → R) : + (↑( ∏ (i : ι) in s, a i : R) : A) = ∏ (i : ι) in s, (↑(a i) : A) := +map_prod (algebra_map R A) a s + +-- to_additive fails for some reason +@[norm_cast] lemma coe_sum {ι : Type*} {s : finset ι} (a : ι → R) : + ↑(( ∑ (i : ι) in s, a i)) = ∑ (i : ι) in s, (↑(a i) : A) := +map_sum (algebra_map R A) a s + +attribute [to_additive] coe_prod + +end comm_semiring_comm_semiring + +section field_nontrivial + +variables {R A : Type*} [field R] [comm_semiring A] [nontrivial A] [algebra R A] + +@[norm_cast, simp] lemma coe_inj {a b : R} : (↑a : A) = ↑b ↔ a = b := +⟨λ h, (algebra_map R A).injective h, by rintro rfl; refl⟩ + +@[norm_cast, simp] lemma lift_map_eq_zero_iff (a : R) : (↑a : A) = 0 ↔ a = 0 := +begin + rw (show (0 : A) = ↑(0 : R), from (map_zero (algebra_map R A)).symm), + norm_cast, +end + +end field_nontrivial + +end algebra_map + /-- Creating an algebra from a morphism to the center of a semiring. -/ def ring_hom.to_algebra' {R S} [comm_semiring R] [semiring S] (i : R →+* S) (h : ∀ c x, i c * x = x * i c) : diff --git a/src/data/complex/is_R_or_C.lean b/src/data/complex/is_R_or_C.lean index f8b57dac29b84..c517bf360b99e 100644 --- a/src/data/complex/is_R_or_C.lean +++ b/src/data/complex/is_R_or_C.lean @@ -114,17 +114,17 @@ theorem ext : ∀ {z w : K}, re z = re w → im z = im w → z = w := by { simp_rw ext_iff, cc } -@[simp, norm_cast, is_R_or_C_simps, priority 900] lemma of_real_zero : ((0 : ℝ) : K) = 0 := +@[norm_cast] lemma of_real_zero : ((0 : ℝ) : K) = 0 := by rw [of_real_alg, zero_smul] @[simp, is_R_or_C_simps] lemma zero_re' : re (0 : K) = (0 : ℝ) := re.map_zero -@[simp, norm_cast, is_R_or_C_simps, priority 900] lemma of_real_one : ((1 : ℝ) : K) = 1 := +@[norm_cast] lemma of_real_one : ((1 : ℝ) : K) = 1 := by rw [of_real_alg, one_smul] @[simp, is_R_or_C_simps] lemma one_re : re (1 : K) = 1 := by rw [←of_real_one, of_real_re] @[simp, is_R_or_C_simps] lemma one_im : im (1 : K) = 0 := by rw [←of_real_one, of_real_im] -@[simp, norm_cast, priority 900] theorem of_real_inj {z w : ℝ} : (z : K) = (w : K) ↔ z = w := +@[norm_cast] theorem of_real_inj {z w : ℝ} : (z : K) = (w : K) ↔ z = w := { mp := λ h, by { convert congr_arg re h; simp only [of_real_re] }, mpr := λ h, by rw h } @@ -137,7 +137,6 @@ by simp only [bit0, map_add] @[simp, is_R_or_C_simps] lemma bit1_im (z : K) : im (bit1 z) = bit0 (im z) := by simp only [bit1, add_right_eq_self, add_monoid_hom.map_add, bit0_im, one_im] -@[simp, is_R_or_C_simps, priority 900] theorem of_real_eq_zero {z : ℝ} : (z : K) = 0 ↔ z = 0 := by rw [←of_real_zero]; exact of_real_inj @@ -558,7 +557,8 @@ begin end lemma re_eq_self_of_le {a : K} (h : abs a ≤ re a) : (re a : K) = a := -by { rw ← re_add_im a, simp only [im_eq_zero_of_le h, add_zero, zero_mul] with is_R_or_C_simps } +by { rw ← re_add_im a, simp only [im_eq_zero_of_le h, add_zero, zero_mul, algebra_map.coe_zero] + with is_R_or_C_simps, } lemma abs_add (z w : K) : abs (z + w) ≤ abs z + abs w := (mul_self_le_mul_self_iff (abs_nonneg _) diff --git a/src/topology/algebra/uniform_field.lean b/src/topology/algebra/uniform_field.lean index 7539f91be14b0..f8a53e5876f01 100644 --- a/src/topology/algebra/uniform_field.lean +++ b/src/topology/algebra/uniform_field.lean @@ -144,8 +144,7 @@ begin dsimp [c, f], rw hat_inv_extends z_ne, norm_cast, - rw mul_inv_cancel z_ne, - norm_cast }, + rw mul_inv_cancel z_ne, }, replace fxclo := closure_mono this fxclo, rwa [closure_singleton, mem_singleton_iff] at fxclo end