Zulip Chat Archive

Stream: general

Topic: Eliminating `algebra {ℕ,ℤ,ℚ} R` diamonds


Anne Baanen (Jun 20 2022 at 16:08):

I have been getting annoyed by the diamonds you get with docs#algebra_nat, docs#algebra_int and docs#algebra_rat versus e.g. docs#algebra.id. The correct solution is to use forgetful inheritance to define the algebra_{nat,int,rat} instances: the to_fun and smul fields in algebra_nat should be set using the [semiring R] instance being passed in; an analogous statement should hold for algebra_int and algebra_rat. More specifically,

  • a semiring R instance should contain of_nat : ℕ → R in addition to the nsmul field
  • a ring R instance should contain of_int : ℤ → R in addition to the zsmul field
  • the combination of division_ring R and char_zero R should contain of_rat : ℚ → R and qsmul : ℚ → R → R

First issue: it's not totally trivial where of_rat should come from, since the current algebra_rat definition takes two instance params. I suppose putting it in division_ring works well enough.

Second issue: if we redefine the algebra instances, should we also redefine the docs#nat.cast_coe, docs#int.cast_coe and docs#rat.cast_coe instances? In particular, the current state of defeq is @@algebra_map _ some_other_algebra ℕ R ≠ @@algebra_map _ algebra_nat ℕ R 0 = ↑0 = 0, should we move the non-defeq one or two steps to the right? Similar for and .

Assuming we also redefine docs#nat.cast_coe, where should of_nat actually live, since cast_coe currently requires only notation ([has_zero α] [has_one α] [has_add α]) and no proofs? Similar for . For , docs#rat.cast_coe takes a division_ring as parameter so it works fine if we put of_rat in division_ring.

Anne Baanen (Jun 20 2022 at 16:11):

And restricting the coercion from to only (non-assoc) semirings isn't going to work, since docs#with_top currently has a coercion from but isn't a semiring.

Eric Rodriguez (Jun 20 2022 at 16:11):

I think @Gabriel Ebner was working on a solution for of_nat with add_monoid_with_one, but I'm not sure where the PR is

Eric Rodriguez (Jun 20 2022 at 16:12):

it's a pretty big one IIRC

Anne Baanen (Jun 20 2022 at 16:13):

For the moment I'll concentrate on the algebra diamond only, since I don't see any big obstacles at this moment.

Eric Wieser (Jun 20 2022 at 17:03):

Note that #12182 already adds of_nat and of_int (edit: that's the PR @Eric Rodriguez is referring to)

Anne Baanen (Jun 22 2022 at 11:47):

I created the PR series fixing the ℚ algebra diamond (once I've resolved any build errors). First a set of PRs for readjusting the import hierarchy:

  • #14849
  • #14890
  • #14893
    And the PR redefining algebra_rat to make use of new of_rat and qsmul fields in division_ring

  • #14894


Last updated: Dec 20 2023 at 11:08 UTC