Overuse of algebra type class

Stream: maths

[Chris Hughes]

I think we might have taken the algebra type class a little far. I think it was originally motivated by the need to put an R-module structure on a ring S given a ring hom R →+* S, but now a lot of stuff is stated in terms of the algebra type class when it should just be stated in terms of a ring hom. The current approach seems to work okay when building up the theory because you can always assume algebra R S when the rings are just arbitrary rings but on more concrete examples the ring homs might not be canonical. An example came up the other day when dealing with transcendence bases. I wanted to prove that a ring is an algebraic extension of the subring generated by a transcendence basis. The statement was

lemma is_transcendence_basis.is_algebraic [nontrivial R] {v :  → A}
  (hv : is_transcendence_basis R v) : is_algebraic (adjoin R (range v)) A

I would actually prefer to state this theorem as is_algebraic (mv_polynomial ι R) A - the rings adjoin R (range v) and mv_polynomial ι R, are isomorphic, but the map mv_polynomial ι R -> A is given by v, so it is not an algebra instance. The mv_polynomial statement is preferable because I know a lot more about mv_polynomial.

The current setup does seem to leave you in a world of pain if you're dealing with a ring hom that isn't canonical enough.

[Kevin Buzzard]

algebra is just "ring hom but a typeclass" and this point of view says that it should thus only be used when the ring hom is "canonical" (in the sense that you definitely won't be considering any more ring homs from R to A). [PS your lemma is missing something, you have {v : → A} as I write]

[Eric Wieser]

Canonical has a stricter meaning here, namely algebra_map R A r = r • 1 which leaves wriggle room only up to propositional equality; the choice of canonicity is usually already made by the has_scalar instance

[Anne Baanen]

Here's an evil thought I just had: can't we get the best of both worlds using an auto_param hack? Namely, state everything that currently uses algebra R A as a "ring-hom-as-typeclass" to take a parameter of the form (f : R →+* A . `[apply algebra_map]) instead. Then the map can be left out when it is canonical, and supplied explicitly when it is not.

[Eric Wieser]

That doesn't work for lemmas about algebras that use • because you no longer have the fact that it is compatible with the algebra_map

[Chris Hughes]

Honestly I think that we're going to have to do that a lot for that sort of thing in other classes. A lot of classes are used in places where the structure is not that canonical. There's only ever one ring structure on a type, but for other classes there isn't always one canonical instance. We've had the same problem with group actions, and there are a bunch of ways of making $\mathbb{R}^n$ an $\mathbb{R}[X]$ module. In the long term, I think we need good notation to be able to explicitly provide a module structure or a group action or an algebra structure, whilst still being able to provide them implicitly most of the time.

[Chris Hughes]

Eric Wieser said:

That doesn't work for lemmas about algebras that use • because you no longer have the fact that it is compatible with the algebra_map

Ideally, my solution to this is to be able to have some nice notation for explicitly proving the module structure. It would be something like •[a] where a is some algebra structure being coerced to a module structure or something. It'll take quite a bit of thought to implement something like this nicely though.