Should `algebra_map` be a coercion?

Stream: general

[Kevin Buzzard]

I have a Xena project student working on partial fraction decomposition. Here's an example of the sort of lemma they're proving: if $R$ is an integral domain and $f\in R[X]$ is a polynomial and $g_j\in R[X]$ are monic polynomials for $j$ running through a finite set $\iota$, then one can write $f/\prod_j g_j$ in the form $q+\sum_j r_j/g_j$ with $q$ and $r_j$ polynomials and $\deg(r_j)<\deg(f_j)$. and $K$ is the field of fractions of the polynomial ring $R[X]$. This is lemma div_eq_quo_add_sum_rem_div in file data/polynomial/partial_fractions.lean on branch xena-partial-fractions. The divisions are all taking place in the field of fractions of $R[X]$ and right now this statement in Lean looks like the rather unwieldy

∃ (q : R[X]) (r : ι → R[X]),
  (∀ (i : ι), (r i).degree < (g i).degree) ∧
    (algebra_map R[X] K).to_fun f / ∏ (x : ι) in s, (algebra_map R[X] K).to_fun (g x) =
      (algebra_map R[X] K).to_fun q +
        ∑ (x : ι) in s, (algebra_map R[X] K).to_fun (r x) / (algebra_map R[X] K).to_fun (g x)

If however, after variables (K : Type) [field K] [algebra R[X] K] [is_fraction_ring R[X] K] I put

noncomputable instance : has_coe R[X] K := ⟨algebra_map R[X] K⟩

then the goal becomes the far more readable

∃ (q : R[X]) (r : ι → R[X]),
  (∀ (i : ι), (r i).degree < (g i).degree) ∧
    ↑f / ∏ (i : ι) in s, ↑(g i) = ↑q + ∑ (i : ι) in s, ↑(r i) / ↑(g i)

So this is some evidence that at least in this situation, algebra_map being a coercion leads to less clutter. If you add lemmas such as

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

@[simp, norm_cast] lemma coe_algebra_map_zero : ((0 : R[X]) : K) = 0 := map_zero (algebra_map R[X] K)

@[norm_cast] lemma coe_algebra_map_neg (x : R[X]) : ((-x : R[X]) : K) = -x := map_neg (algebra_map R[X] K) x

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

@[simp, norm_cast] lemma coe_algebra_map_one : ((1 : R[X]) : K) = 1 := map_one (algebra_map R[X] K)

then simp and norm_cast work how you would expect and it's been a more pleasant experience all round.

Are there arguments against making algebra_map a coercion in general? For me, algebra_map R A means not just "there is a ring hom from $R$ to $A$" but the stronger "there is a canonical ring hom from $R$ to $A$", which is the kind of situation where one might expect a coercion.

@Eric Wieser you suggested making it a lift but then I don't think I can do (f : K) when f : R[X].

[Eric Wieser]

(↑k : K) isn't much longer to write, and often you can drop the : K due to context. Thinking of (_ : _) as a coercion is the wrong mental model anyway.

[Eric Wieser]

Also this should probably be has_lift_t not has_lift.

[Yaël Dillies]

Wasn't Anne having projects for a has_ring_coe typeclass? That would be basically the same as algebra except that the hom is supposed canonical, which seems to be what you want.

[Eric Wieser]

That also has the advantage that it helps for towers of non-commutative rings (it can replace docs#polynomial.C and docs#matrix.scalar)

[Kevin Buzzard]

@Anne Baanen can I help with this? What's your vision here?

My impression is that one way to push forward with the UG degree project now is not, as in the past, just to wait for things to organically happen, but to take these annoying things which are still on the list and actually match them up with undergraduates I run into who are interested in doing projects and then actually supervising them through the process. The student in question for the partial fractions project, Sidharth Hariharan, has got to the point now where he can start making PRs for partial fractions and this question of how, if at all, to coerce from $R[X]$ to its field of fractions is what's currently stopping us.

[Kevin Buzzard]

If you add the instance as a coercion in algebra.algebra.basic then alg_hom.coe_mk explodes.

@[simp, norm_cast] lemma coe_mk {f : A → B} (h₁ h₂ h₃ h₄ h₅) :
  ⇑(⟨f, h₁, h₂, h₃, h₄, h₅⟩ : A →ₐ[R] B) = f :=
-- error on last `f`, maximum class-instance resolution depth has been reached

Proof used to be rfl, now statement doesn't compile.

[Kevin Buzzard]

MWE

import algebra.algebra.basic

instance foo (R A : Type*) [comm_semiring R] [semiring A] [algebra R A] :
  has_coe R A := ⟨λ r, algebra_map R A r⟩

@[simp, norm_cast] lemma alg_hom.coe_mk'' {A B R : Type*} [comm_ring R]
  [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] {f : A → B} (h₁ h₂ h₃ h₄ h₅) :
  ⇑(⟨f, h₁, h₂, h₃, h₄, h₅⟩ : A →ₐ[R] B) = f := -- boom

[Kevin Buzzard]

@[simp, norm_cast] lemma alg_hom.coe_mk'' {A B R : Type*} [comm_ring R]
  [comm_ring A] [algebra R A] [comm_ring B] [algebra R B] {f : A → B} (h₁ h₂ h₃ h₄ h₅) :
  ⇑(⟨f, h₁, h₂, h₃, h₄, h₅⟩ : A →ₐ[R] B) = (f : A → B) := rfl

works. I am coercing the function f to a function?

[Kevin Buzzard]

Do I need to worry about priorities here? Why did that just happen?

[Kevin Buzzard]

Sorry about the primes, turns out there's already a coe_mk'

[Kevin Buzzard]

@[simp, norm_cast] lemma coe_mk {f : A → B} (h₁ h₂ h₃ h₄ h₅) :
  ⇑(⟨f, h₁, h₂, h₃, h₄, h₅⟩ : A →ₐ[R] B) = (f : A → B) := rfl
set_option pp.all true
#check @coe_mk -- ∀ blah, blah = f even with pp.all true

Why do I have to change f to (f : A \to B) and does lean not even detect this change afterwards?

[Kevin Buzzard]

Proof of rat.smul_one_eq_coe breaks, I think because rat.cast_coe = coe_base is no longer rfl or something? I'm way out of my depth.

[Kevin Buzzard]

Can't seem to fix with priorities on the new instance.

[Kevin Buzzard]

Oh has_lift seems to be OK (this was Eric's original suggestion) in the sense that it doesn't break algebra.algebra.basic. I've now understood that I can still do (↑r : A) if I want to direct the coercion.

[Kevin Buzzard]

Oh this is great. I can confirm that has_lift solves my original problem very nicely, so my current proposal is that

instance algebra.has_lift (R A : Type*) [comm_semiring R] [semiring A] [algebra R A] :
  has_lift R A := ⟨λ r, algebra_map R A r⟩

be added to mathlib. Right now I'm compiling to see if it breaks anything else.

[Eric Wieser]

My claim is that should be has_lift_t so that if we have a tower R S A the coercion from R to A doesn't try docs#lift_trans

[Eric Wieser]

Also, we should probably decide which spelling to make the simp-normal form

[Kevin Buzzard]

My instinct is to make the coercion the simp normal form. The fact that you always have to spell it out makes it very appealing, instead of algebra_map R A r you have (\u r : A) and I think that the latter is much more readable for mathematicians.

[Kevin Buzzard]

I can confirm that has_lift_t also works great in my use case, so the current proposal is to make it a has_lift_t and also to make the coercion the simp normal form.

[Jireh Loreaux]

I'm a fan of this assuming it works essentially everywhere. When I'm dealing with algebra_map frequently I introduce local notation for it.

[Junyan Xu]

∃ (q : R[X]) (r : ι → R[X]),
  (∀ (i : ι), (r i).degree < (g i).degree) ∧
    (algebra_map R[X] K).to_fun f / ∏ (x : ι) in s, (algebra_map R[X] K).to_fun (g x) =
      (algebra_map R[X] K).to_fun q +
        ∑ (x : ι) in s, (algebra_map R[X] K).to_fun (r x) / (algebra_map R[X] K).to_fun (g x)

I'm wondering why in you write .to_fun instead of simply algebra_map R[X] K f etc.?

[Kevin Buzzard]

Oh lol you're totally right. I wrote the Zulip post after I'd got the coercion working and so I had to reverse-engineer what I had before the coercion; I used the unfold_coes tactic to do this but it appears to have unfolded more than I expected...

[Kevin Buzzard]

Even without the .to_fun the point stands

[Kevin Buzzard]

The point is that that a mathematician like me can just read

∃ (q : R[X]) (r : ι → R[X]),
  (∀ (i : ι), (r i).degree < (g i).degree) ∧
    ↑f / ∏ (i : ι) in s, ↑(g i) = ↑q + ∑ (i : ι) in s, ↑(r i) / ↑(g i)

without having to think too much, we can just switch the arrows off mentally and occasionally norm_cast or push_cast to keep us on track.

[Kevin Buzzard]

With this notation I found that I could use Lean as a calculator when I was working out the algebra relating to partial fraction decomposition. It was really great.

[Kevin Buzzard]

On my branch with

instance 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⟩

there are now two non-defeq coercions from fin n to fin n:

example : comm_ring (zmod n) := infer_instance
def foo (R : Type) [comm_ring R] (a : zmod n) : R := ↑a -- defined recursively
example (a : zmod n) : foo (zmod n) a = (algebra_map.has_lift_t (zmod n) (zmod n)).1 a := rfl -- fails
-- because foo is recursively defined and my coercion is id.

[Kevin Buzzard]

The proof of int.cast_id is now rflas opposed to an induction.

[Kevin Buzzard]

I can tone down the priority of algebra_map.has_lift_t but is this acceptable or are diamonds banned?

[Eric Rodriguez]

urgh this is the char_p diamond that needs fixing

[Eric Rodriguez]

(at least this is my guess)

[Kevin Buzzard]

The part of the diamond already in mathlib is docs#zmod.has_coe_t, which is the (mathematically crazy) map (not a ring hom in general!) from zmod n to an arbitary ring R. But it's being used in a situation where n=0 in R where you could certainly argue that it was a natural coercion, unfortunately defined recursively in general. There should be a subsingleton instance I guess.

[Eric Rodriguez]

there is a subsingleton instance I think

[Eric Rodriguez]

or is that again in the char_p case?

[Kevin Buzzard]

Oh the issue is that it's not in general a ring hom so it's not a subsingleton

[Eric Wieser]

The proof of src#int.cast_id should already be rfl

[Anne Baanen]

Kevin Buzzard said:

Anne Baanen can I help with this? What's your vision here?

Here's the original thread. I did try to get some undergrad to do it for us :grinning_face_with_smiling_eyes: but I don't expect there will be undergrads available until the end of this academic year.

I think there is a relatively safe upgrade path as follows:

• Define a new class coe_ring_hom [semiring R] [semiring S] [has_lift_t R S] := (coe_add := ↑(x + y) = ↑x + ↑ y) (coe_etc : etc), flesh out the API somewhat. I think unbundled inheritance would the best choice, so we don't have to worry about extra diamonds arising from transitivity. It also means we can extend has_lift_t here while defining the instances on has_coe_t instead.
• Define a new map ring_hom.coe : R →+* S := { to_fun := coe, map_foo := coe_foo } which will take the role of algebra_map whenever a bundled map is needed.
• Add a way to translate between algebra and coe_ring_hom. I don't expect we can really do this automatically, so this probably means adding a has_lift_t + coe_ring_hom instance for each existing algebra instance.
• Switch over simp normal form to prefer coe or ring_hom.coe over algebra_map
• Maybe add an instance coe_ring_hom.to_algebra?
• Maybe totally remove algebra_map from the algebra class so the non-unital people are satisfied.

[Eric Wieser]

I don't see why point 3 can't be automatic, via new algebra.to_has_lift_t and algebra.to_coe_ring_hom instances

[Eric Wieser]

Point 4 sounds like a bad idea to me, algebras have more structure than ring home coercions

[Anne Baanen]

We have lots of existing instances of algebra and has_coe on the same types, and those are not always defeq. Add in transitivity and it starts to get quite hairy to avoid diamonds.

[Eric Wieser]

Can you give an example of where they're not defeq?

[Eric Rodriguez]

We just had this with the adjoin_root coe

[Eric Rodriguez]

Obviously there was an underlying issue but these will be everywhere and crop up a lot more now

[Michael Stoll]

Kevin Buzzard said:

The point is that that a mathematician like me can just read

∃ (q : R[X]) (r : ι → R[X]),
  (∀ (i : ι), (r i).degree < (g i).degree) ∧
    ↑f / ∏ (i : ι) in s, ↑(g i) = ↑q + ∑ (i : ι) in s, ↑(r i) / ↑(g i)

without having to think too much, we can just switch the arrows off mentally and occasionally norm_cast or push_cast to keep us on track.

@Kevin Buzzard Don't you need some coprimality assumption on the $g_j$? Think of $1/(x \cdot x) = ?/x+ ?/x$...

[Kevin Buzzard]

Ha ha yes, I deleted some hypotheses to make the result look clearer :-)

[Anne Baanen]

Remember this old thread? :grinning: I just got branch#coe_hom to build (on an old mathlib), which provides classes for e.g. ↑(x + y) = ↑x + ↑y and ring_hom.coe.

[Anne Baanen]

Now in PR form: #17048