algebra_map as coercion, and norm_cast

Stream: maths

[Kevin Buzzard]

import ring_theory.localization.fraction_ring
import data.polynomial.div
import tactic.field_simp

open_locale polynomial

variables (R : Type) [comm_ring R] [is_domain R]
variables (K : Type) [field K] [algebra R[X] K] [is_fraction_ring R[X] K]

-- example (f : R[X]) : K := f -- fails

namespace polynomial

noncomputable instance : has_coe R[X] K := ⟨algebra_map R[X] K⟩ -- I'm so cunning

example (f g h : R[X]) : (f : K) + g * h = (f + g * h : R[X]) := begin
  norm_cast, -- fails
end

end polynomial

Is there a way of getting norm_cast to work on a custom coercion? Note that algebra_map is a ring_hom.

[Yakov Pechersky]

You'd have to make the simp lemma and tag the appropriate lemmas with norm_cast, which I think you can do just with attribute ...

[Junyan Xu]

To make full use of norm_cast you need move, elim and squash lemmas, as mentioned in p.4 of the paper.

[Heather Macbeth]

I also think this would be a nice idea, I've asked about it before, but @Rob Lewis at the time thought it would be impractical.

[Eric Wieser]

Separately, I think we've had multiple discussions about the canonical notation for algebra_map be has_lift_t or sometimes even has_coe_t.

[Eric Wieser]

That's much more appealing now that the diamonds for nat.cast, int.cast, and rat.cast are all gone

[Kevin Buzzard]

For what it's worth, I got this working fine:

import data.polynomial.algebra_map
import ring_theory.localization.fraction_ring

namespace polynomial

variables {R A : Type*} [comm_ring R] [comm_ring A] [algebra R A]

instance : has_coe R A := ⟨algebra_map R A⟩

@[norm_cast] lemma coe_algebra_map_add (a b : R) : ((a + b : R) : A) = a + b :=
map_add (algebra_map R A) a b

@[norm_cast] lemma coe_algebra_map_mul (a b : R) : ((a * b : R) : A) = a * b :=
map_mul (algebra_map R A) a b

@[norm_cast] lemma coe_algebra_map_zero : ((0 : R) : A) = 0 :=
map_zero (algebra_map R A)

@[norm_cast] lemma coe_algebra_map_pow (a : R) (n : ℕ) : ((a ^ n : R) : A) = a ^ n :=
map_pow (algebra_map R A) _ _

-- random extra one for the case I was interested in
@[norm_cast] lemma coe_algebra_map_inj_iff [is_fraction_ring R A] (a b : R) : (a : A) = b ↔ a = b :=
⟨λ h, is_fraction_ring.injective R A h, by rintro rfl; refl⟩

end polynomial

variables {R A : Type*} [comm_ring R] [comm_ring A] [algebra R A]

example (x y z : R) : (x : A) + y * z = (x + y * z : R) := by norm_cast