Characteristics of fraction_ring

Stream: maths

[Jon Eugster]

Sorry hit the wrong button.

I have troubles expression certain coes as towers of multiple coe
. For characteristics zero, the definition says that the coe:\N \to R is injective. Moreover for an R-algebra K one has a "coe" (algebra map) R \to K so I think the coe: \N \to K should factor through R, but how would I express that?

import algebra.char_zero
import algebra.char_p.basic
import ring_theory.localization     -- for `fraction_ring`

variables (R: Type*) [integral_domain R]
local notation `K` := fraction_ring R

lemma algebra_map_fraction_ring_injective: function.injective (algebra_map R K) :=
  (fraction_map.injective (fraction_ring.of R))

instance [h: char_zero R]: char_zero K :=
{
  cast_injective :=
  begin
    have q := function.injective.comp (algebra_map_fraction_ring_injective R) (h.cast_injective),
    sorry
    -- The "cast" `coe:ℕ → K` should be factored as two casts `ℕ → R → K`, but I don't know how to state that...
  end,
}

[Anne Baanen]

simp knows there is only one ring hom from ℕ to K:

import algebra.char_zero
import algebra.char_p.basic
import ring_theory.localization     -- for `fraction_ring`

variables (R: Type*) [integral_domain R]
local notation `K` := fraction_ring R

lemma algebra_map_fraction_ring_injective: function.injective (algebra_map R K) :=
(fraction_map.injective (fraction_ring.of R))

instance [h: char_zero R]: char_zero K :=
{ cast_injective :=
  begin
    convert function.injective.comp (algebra_map_fraction_ring_injective R) (h.cast_injective),
    ext,
    simp
  end }

[Anne Baanen]

The relevant lemma is docs#ring_hom.map_nat_cast

[Jon Eugster]

Oh I haven't seen convertbefore, thank you!

[Anne Baanen]

The other way would be to replace coe with algebra_map ℕ K resp. algebra_map ℕ R using docs#ring_hom.eq_nat_cast, ∘ with ring_hom.comp using docs#ring_hom.coe_comp and finishing with docs#is_scalar_tower.algebra_map_eq.

[Anne Baanen]

Jon Eugster said:

Oh I haven't seen convertbefore, thank you!

convert and congr are very useful for pointing out exactly where your "obviously the same" and Lean's "obviously the same" disagree :grinning: