Q-algebra diamond

Stream: maths

[Yury G. Kudryashov]

Currently we have two non-defeq instances for algbera ℚ ℚ: one is based on the fact ℚ = ℚ, and the other is based on the fact [division_ring ℚ] [char_zero ℚ].

[Yury G. Kudryashov]

I suggest the following solution (motivated by @Sebastien Gouezel 's refactor of nsmul/gsmul):

1. Move the definition of rat to a separate file that does not depend on division_ring.
2. Add the following fields to the definition of division_ring k:

(of_rat : ℚ → k := λ r, gsmul r.num 1 / nsmul r.denom 1)
(of_rat_eq : ∀ r, of_rat r = gsmul r.num 1 / nsmul r.denom 1 . try_refl_tac)

3. Make sure that ℚ has of_rat = id.
4. Use of_rat in the definitions of rat.cast and rat.algebra_rat.

[Yury G. Kudryashov]

P.S.: To make things worse (unless we fix the diamond), I'm going to add an instance for [algebra ℝ A] → [algebra ℚ A].

[Eric Wieser]

What about division rings that aren't char_zero?

[Eric Wieser]

We should fix this for int and nat algebras too

[Alex J. Best]

Those won't be algebras over Q right, what are you asking more specifically Eric? There was a thread a long time about whether there should be a coe from Q to non-char zero division rings where i think i argued that yes there should still be as it's nice to be able to write 1/2 as a number in finite fields for instance.

[Yury G. Kudryashov]

Algebras over int and nat can use gsmul and nsmul.

[Eric Wieser]

That forms a diamond with the algebra map that's just id though

[Eric Wieser]

We need a semiring.of_nat field to fix that

[Yury G. Kudryashov]

Indeed, you're right. Alternative proposal: we remove algebra_map from the definition of algebra, reformulate axioms in terms of properties of smul, and add rsmul instead of of_rat to the definition of division_ring.

[Yury G. Kudryashov]

This is a larger refactor but it removes one more source of diamonds.

[Yury G. Kudryashov]

And we can split it in two halves (“redefine algebra” and “add rsmul”).

[Yury G. Kudryashov]

I think that we only need r • (x * y) = (r • x) * y and r • (x * y) = x * (r • y).

[Yury G. Kudryashov]

I don't know if we can replace some of x/y with 1.

[Yury G. Kudryashov]

@Kenny Lau @Johan Commelin :up:

[Yury G. Kudryashov]

I suggest that we extend module R A and add axioms from is_scalar_tower and smul_comm_class.

[Yury G. Kudryashov]

I mean something like

@[nolint has_inhabited_instance]
class algebra (R : Type u) (A : Type v) [comm_semiring R] [semiring A]
  extends module R A, is_scalar_tower R A A, smul_comm_class R A A

[Eric Rodriguez]

I've always felt yucky that we have to do these sorts of hacks instead of just writing what we want to write as mathematicians :/ I wish there was a better solution, e.g. being able to specifically feed to the typeclass system "these two instances are equal, here's my proof, please stop fussing about it"

[Eric Rodriguez]

This (and similar) issues will also only keep getting worse the more maths we do

[Eric Wieser]

Yury G. Kudryashov said:

Indeed, you're right. Alternative proposal: we remove algebra_map from the definition of algebra, ...

I think the argument goes that it is useful to have definitional control of the algebra map. Of course, the cost of definitional control anywhere is that we have to control it through diamonds too

[Yury G. Kudryashov]

Why do you want to have defeq for algebra map?

[Kevin Buzzard]

This is the price you pay for dependent types, and if it enables us to do maths we wouldn't be able to do otherwise then I'm prepared to pay the price. It's not the case that it's spiralling out of control. Everyone knows that abelian groups are the same as ℤ-modules and it's really convenient to make this as definitional as possible because we seem to use it all the time. Similarly char 0 division rings are ℚ-algebras and maybe it's best we make this as definitional as possible. This isn't going to go on forever, this is clear.

[Yury G. Kudryashov]

@Kevin Buzzard Who did you answer?

[Kevin Buzzard]

This (and similar) issues will also only keep getting worse the more maths we do

[Yury G. Kudryashov]

@Eric Wieser OTOH, we'll have defeq algebra_map r x = (r • 1) * x.

[Yury G. Kudryashov]

Why docs#add_comm_group.int_module.unique is not an instance?

[Yury G. Kudryashov]

A similar statement about algebras (with subsingleton instead of unique) is an instance.

[Yury G. Kudryashov]

Found #6025

[Yury G. Kudryashov]

branch#redefine-algebra (fixed algebra.algebra.basic, DID NOT update docstrings)

[Yury G. Kudryashov]

cherry-picked changes to other files in branch#extra-instances

[Johan Commelin]

I guess that loosing defeq-control over algebra_map will be mildly annoying, but it probably will not create diamonds. So that might be the right balance.

[Oliver Nash]

I'm really grateful when I see issues like this identified and fixed. Thank you! We'd never have the problem if we didn't put data in typeclasses though, right?

[Oliver Nash]

Not doing so would come at the cost of having to write things like "let G, 1, * be a group" instead of "let G be a group" and this would get a painful with more complicated objects ("let K, 0, 1, +, *, ∥ ∥, < be a normed ordered field") but I think I can imagine a setup where we tried to get the best of both worlds by splitting every typeclass in two: a base with only Prop-valued fields and another which consumes the base and fills in defaults for the data-valued fields.

[Oliver Nash]

I think this might have the advantage that we could have multiple variants of the data-bearing typeclasses and this might give us the extra wiggle room to resolve issues like this.

[Eric Wieser]

#9525 contains an outline of the of_nat / of_rat approach

[Eric Wieser]

Idealy we'd pushnat.castearlier in the imports (before we have rings defined) so that we can use that earlier

[Eric Wieser]

Yury G. Kudryashov said:

Eric Wieser OTOH, we'll have defeq algebra_map r x = (r • 1) * x.

I assume you meant algebra_map R A r = r • 1. The downside of not having algebra_map is we lose the fact that algebra_map R R r = r is defeq.

[Eric Wieser]

Yury G. Kudryashov said:

branch#redefine-algebra (fixed algebra.algebra.basic, DID NOT update docstrings)

There's a lot of good stuff in this branch even if we don't decide to change the definition of algebra; would you mind PRing all the new lemmas about smul_comm_class etc separately?

[Yury G. Kudryashov]

IMHO definitional equalities that are not important for TC diamonds can go away.

[Yury G. Kudryashov]

See branch#extra-instances for lemmas/instances from branch#redefine-algebra

[Eric Wieser]

That new branch looks pr-ready to me

[Yury G. Kudryashov]

I'm waiting for CI.

[Yury G. Kudryashov]

Though let me create a PR already.