feat(algebra/algebra/basic): Algebras are bimodules

[eric-wieser]

This changes the definition of algebra to include a right action, such that algebra R A automatically implies a compatible left- and right- R-module structure.

The module ℕᵐᵒᵖ R and module ℤᵐᵒᵖ R instances this introduces create diamonds when R=ℕ and R=ℤ with semiring.to_opposite_module (since mul_comm is not true definitionally), but fixing those would require adding an op_nsmul field to add_comm_monoid which would make this PR huge!

The same change that is made to algebra R A also ends up being made to lie_algebra R L, although this is less in the way since lie_algebra R L already extends module R L, unlike algebra R A which does not directly extend module R A.

Most of the extra typeclass arguments that are needed in various places stem from module.End R M now only being an R-algebra if M is an R-bimodule.

---

This is running into an issue flagged by the fails_quickly linter, which can be reproduced as:

import algebra.algebra.restrict_scalars

variables {R S M : Type*} [comm_semiring R] [add_comm_monoid M]

-- works as expected
example [semiring S] [algebra R S] [module Sᵐᵒᵖ M] : module Rᵐᵒᵖ (restrict_scalars R S M) :=
by apply_instance

-- fails as expected
example [comm_semiring S] [algebra R S] : module Rᵐᵒᵖ (restrict_scalars R S M) := by apply_instance 

section disabled_instance
local attribute [-instance] algebra.to_opposite_module
-- fails as expected
example [semiring S] [algebra R S] : module Rᵐᵒᵖ (restrict_scalars R S M) := by apply_instance  
end disabled_instance

-- timeout, trace repeats `cached failure for comm_semiring S` forever
example [semiring S] [algebra R S] : module Rᵐᵒᵖ (restrict_scalars R S M) := by apply_instance 

• depends on: [Merged by Bors] - chore(algebra/module/submodule): missing is_central_scalar instance #10720
• depends on: [Merged by Bors] - chore(group_theory/group_action/defs): add instances to copy statements about left actions to right actions when the two are equal #10949
• depends on: [Merged by Bors] - feat(algebra/{monoid_algebra/basic,free_non_unital_non_assoc_algebra,lie/free}): generalize typeclasses #11283
• depends on: [Merged by Bors] - chore(topology/algebra/module/basic): add continuous_linear_map.is_central_scalar #11291
• depends on: [Merged by Bors] - feat(algebra,linear_algebra,ring_theory): more is_central_scalar instances #11297
• depends on: [Merged by Bors] - chore(topology/algebra/module/multilinear): relax typeclass arguments #11972
• depends on: [Merged by Bors] - chore(linear_algebra/affine_space/affine_map,topology/algebra/continuous_affine_map): generalized scalar instances #11978
• depends on: [Merged by Bors] - feat(topology/continuous_function/algebra): generalize algebra instances #12055
• depends on: [Merged by Bors] - feat(topology/metric_space): multiplicative opposites inherit the same (pseudo_?)(e?)metric and uniform_space #12120
• depends on: [Merged by Bors] - feat(measure_theory/function/ae_eq_fun): generalize scalar actions #12248
• depends on: [Merged by Bors] - chore(topology/continuous_function/bounded): add an is_central_scalar instance #12272
• depends on: [Merged by Bors] - test(instance_diamonds): verify that restrict_scalars produces no diamonds on the complex numbers #12273
• depends on: [Merged by Bors] - chore(topology/algebra/uniform_mul_action): add has_uniform_continuous_const_smul.op #12434
• depends on: [Merged by Bors] - chore(topology/continuous_function/zero_at_infty): add is_central_scalar instance #13710
• depends on: [Merged by Bors] - chore(analysis/normed_space/basic): reorder the restrict_scalars definitions #13995
• depends on: [Merged by Bors] - chore(algebra/algebra/restrict_scalars): put a right action on restricted scalars #13996
• depends on: [Merged by Bors] - chore(algebra/lie/quotient): golf some instances #14480

[Vierkantor]

This is running into an issue flagged by the fails_quickly linter, which can be reproduced as:

What was the resolution of this issue?

[Vierkantor]

I'm a bit worried about the loss of usability we'll get, especially because of having to insert [module Rᵐᵒᵖ M] [is_central_scalar R M] everywhere. I'd like to see a nicer way (ideally closer to standard mathematical notation), how about a new typeclass [bimodule R M]?

[Vierkantor]

I'd argue that it would be more convenient, adding a field op_smul and making to_has_opposite_smul an instance.

[eric-wieser]

The advantage of this spelling is that lean automatically picks up the instance as an instance argument if it already exists

[Vierkantor]

What should be fixed, or has it been fixed now?

[eric-wieser]

I think this is referring to the fact that we would need a add_comm_group.rzsmul field otherwise we end up with another diamond again.

[eric-wieser]

This is running into an issue flagged by the fails_quickly linter, which can be reproduced as:

What was the resolution of this issue?

It was to mess with the unfolding of some of the mul_opposite instances