redefining alg_equiv_class

Stream: general

[Jireh Loreaux]

I propose redefining alg_equiv and alg_equiv_class so that they avoid the commutes field, and instead use the map_smul field. The reasoning is as follows: it would be nice to have a unified structure that handles both the unital and non-unital settings simultaneously, much like ring_equiv. However, because of the current commutes field, we are required to have an [algebra R A] hypothesis, which forces A to be unital. Note how my alg_equiv_class' below has much weaker type class assumptions, but when they are strengthened to those of alg_equiv_class they imply it.

Any objections to this?

import algebra.algebra.basic
import algebra.module.equiv

set_option old_structure_cmd true

class alg_equiv_class' (F : Type*) (R A B : out_param Type*)
  [semiring R] [add_comm_monoid A] [add_comm_monoid B] [module R A] [module R B] [has_mul A]
  [has_mul B] extends semilinear_equiv_class F (ring_hom.id R) A B, ring_equiv_class F A B

instance foo (F R A B : Type*) [comm_semiring R] [semiring A] [semiring B] [algebra R A]
  [algebra R B] [alg_equiv_class' F R A B] : alg_equiv_class F R A B :=
{ commutes := λ f r, by simp only [algebra.algebra_map_eq_smul_one, map_smul, map_one],
  .. alg_equiv_class'.to_ring_equiv_class F R A B }

[Eric Wieser]

Isn't A forced to be unital anyway by extending ring_equiv_class?

[Eric Wieser]

Oh nevermind, ring_equiv_class is less assuming that its name would suggest

[Jireh Loreaux]

That's because it doesn't have to be :grinning_face_with_smiling_eyes:

[Anne Baanen]

Sounds like a good plan to me!

[Junyan Xu]

Would you change alg_hom_class as well?

[Anne Baanen]

Why not, if the inheritance from non_unital_alg_hom_class would work correctly.

[Jireh Loreaux]

No, I'm not changing alg_hom_class as well, because in that case map_one has to be part of the structure, which already forces the algebras to be unital.

In the equiv case, you don't need to assume map_one because it comes for free from bijectivity and preserving multiplication (see ring_equiv), which is why the unital and non-unital cases can be unified in this context.

[Jireh Loreaux]

Although I guess we don't have any sort of unital algebra morphisms for non-associative algebras. We could potentially go with map_smul for alg_hom_class too, in order to fix this problem, and then just make commutes a theorem for things of this class with strong enough type class assumptions.