left vs right modules in tensor products

Stream: maths

[Jakob von Raumer]

@Eric Wieser What's your proposal then? "Use left modules everywhere, except if you intend to use it on the left side of a tensor product, then use symmetric ones" still sounds weird to me

[Eric Wieser]

I'm afraid that the length of this thread has gotten to the point where I'm no longer certain which problem we're trying to solve any more

[Eric Wieser]

(deleted)

[Eric Wieser]

Oh, you mean "using a type M on the left side of a tensor product means it needs a right-action by R"?

[Kevin Buzzard]

The underlying problem is that we don't have a good theory of non-commutative algebra, and it's getting to the point where we are really going to need this (e.g. we want to do some representation theory), and I would actively encourage @Jakob von Raumer to work on this important problem and thank them for initiating the discussion! Maybe Reid's suggestion about just going with left_module and right_module is worth trying?

[Eric Wieser]

I agree, it's great that @Jakob von Raumer is thinking hard about this

[Eric Wieser]

(Oh, also I remembered the other place where I wanted symmetric actions; I wanted to generalize docs#derivation so that I could use it on square matrices, without breaking all the existing commutative uses)

[Eric Wieser]

Jakob von Raumer said:

But I'd be happy for you to PR it, happy for everything that breaks my PR into smaller pieces ^^

I plan to do this once #10302 has gone through

[Eric Wieser]

And then we can use the current module + the is_symmetric_smul from that future PR to compare the other proposals in this thread against.

[Jakob von Raumer]

Yes, let me recap the problem again, how do I move a huge chunk of messages to a new topic? This is still called "ideals in non-comm rings" which is a bit misleading ^^'

[Eric Wieser]

If you can find the message that you think changed the topic, you can edit the topic for that message, and every message after it will change too

[Eric Wieser]

If there are individual message that end up in the wrong place after that, you can PM me or another maintainer to move them using our zulip powers

[Jakob von Raumer]

I think the discussions never went back to being about ideals :D

[Eric Wieser]

Ideal

[Jakob von Raumer]

So to recap:

• Commutative algebraists want to have "If $M$ and $N$ are $R$-modules, so is $M \otimes_R N$, also $(rm) \otimes n = m \otimes (rn)$ is part of the definition of the tensor product".
• On the other hand non-commutative algebraists want "If $M$ is an $S$-$R$-bimodule and $N$ is a left $R$-module, then $M \otimes_R N$ is an $S$-module and the defn of the tensor product includes $(mr) \otimes n = m \otimes rn$.
• The current implementation satisfies the first version, but not the second one. One way to change this is to remove the commutativity requirement and (to get) the equation $(rm) \otimes n = m \otimes (rn)$, which is used a lot all over mathlib, require that in many cases $M$ is not just an $R$-module but a symmetric $R$-$R$-bimodule. But this means we have to add an instance of module (opposite R) M whenever we want to talk about $M \otimes_R N$ as an $R$ module. Which is quite often.
• As @Oliver Nash mentions, the whole dilemma doubles pretty analogously in with the $R$-module of $R$-linear maps $M \to N$.
• Several people now have told me that it's more common to use the term "$R$-module" meaning "symmetric $R$-$R$-bimodule" in general, even if we only write the $$r$$s on the left. It's definitely more intuitive than needing to provide two extra instances whenever we want to plug in a module in a tensor product.

[Jakob von Raumer]

To give another good example: We get the category of Module Rs but can't get the monoidal category of Module Rs even if R is commutative.

[Eric Wieser]

How far does the following get us:

• Rename module to left_module
• Define abbreviation right_module := left_module (Rᵒᵖ) M. We won't make any instances of this (beyond docs#semiring.to_opposite_module), but it's good for a human reader
• Do the above for the other typeclasses like mul_action too
• Define class module (R M) extends left_module R M, right_module R M, is_symmetric_smul R Rᵒᵖ M

[Johan Commelin]

Jakob von Raumer said:

"[...] also $(rm) \otimes n = m \otimes (rn)$ is part of the definition of the tensor product"

I use this formula all the time. But I've never considered it part of the definition. The definition uses $mr ⊗ n$. And the formula is obtained in the special case that $M$ is a symmetric $R$-$R$-bimodule.

[Johan Commelin]

@Eric Wieser If there are no instances of right_module, how would notation for right actions work?

[Eric Wieser]

Well it just finds instances of left_module (opposite R) M because it's an abbreviation

[Johan Commelin]

And m <• r would be notation for (to_opposite r) • m, or something like that?

[Jakob von Raumer]

Johan Commelin said:

I use this formula all the time. But I've never considered it part of the definition. The definition uses $mr ⊗ n$. And the formula is obtained in the special case that $M$ is a symmetric $R$-$R$-bimodule.

Okay, thanks. That's in line with my PR then. :grinning: Unfortunately it's at odds with a good chunk of mathlib.

[Johan Commelin]

Yes, so I would assume symm R-R-bimod everywhere, in a first refactor PR.

[Johan Commelin]

Later PRs can then weaken those assumptions, by flipping the sides of some actions.

[Jakob von Raumer]

Eric Wieser said:

How far does the following get us:

• Rename module to left_module
• Define abbreviation right_module := left_module (Rᵒᵖ) M. We won't make any instances of this (beyond docs#semiring.to_opposite_module), but it's good for a human reader
• Do the above for the other typeclasses like mul_action too
• Define class module (R M) extends left_module R M, right_module R M, is_symmetric_smul R Rᵒᵖ M

That's roughly what Reid suggested. IIRC the issue you mentioned is that we will have lots of lemmas/construction about left_module R M which will not automatically carry over to module R M in the case where R is commutative, do you think that's a problem?

[Eric Wieser]

Why wouldn't they carry over?

[Eric Wieser]

There'd be a module.to_left_module instance

[Eric Wieser]

[module R M] would be nothing but a shorthand for [left_module R M] [left_module (opposite R) M] [is_symmetric_smul R M]

[Jakob von Raumer]

Oh right, yes. Thanks. I flipped the directions around in my head. So we will make sure we prove as little as possible about module and as much as possible about left_module...

[Eric Wieser]

Yes, exactly; it's the same as docs#is_domain vs docs#nontrivial and docs#no_zero_divisors

[Eric Wieser]

Where the former exists only because the latter is an annoying spelling

[Eric Wieser]

I would probably recommend doing the rename separately from the tensor product refactor

[Eric Wieser]

Perhaps afterwards

[Jakob von Raumer]

Doing it afterwards has the advantage of knowing exactly where we have to assume the symmetry. So I'll just continue and add module (opposite R) M and is_symmetric_smul R M where needed, ok?

[Reid Barton]

Eric Wieser said:

How far does the following get us:

• Define abbreviation right_module := left_module (Rᵒᵖ) M. We won't make any instances of this (beyond docs#semiring.to_opposite_module), but it's good for a human reader

So the advantage of using this encoding is we don't have to duplicate a lot of definitions/lemmas, but I suspect we would need to do some work anyways to make sure the encoding does not "leak", e.g., we will need a lemma that says (m <• r) <• s = m <• (r * s) without any mention of opposite.

Though I can't think of any examples where this would happen, there's also the possibility that someone might want to consider an $R^{\mathrm{op}}$-$R$-bimodule, which seems very difficult with this encoding. That's why I would tend to prefer a more "nominal" distinction between left and right actions.

[Johan Commelin]

I guess it will happen, but maybe not often. E.g., at some point you want to relate K-theory of Rᵒᵖ with K-theory of R. Things like that.

[Jakob von Raumer]

Reid Barton said:

which seems very difficult with this encoding

Why?

[Reid Barton]

Because it means you have to reason about two different instances of left_module (Rᵒᵖ) M at once, right?

[Jakob von Raumer]

Ah right, it might work to make an irreducible definition for $R' := R^{op}$ in this case

[Jakob von Raumer]

Reid Barton said:

we will need a lemma that says (m <• r) <• s = m <• (r * s) without any mention of opposite

smul_smul would still be the right lemma, it might just be that the naming for some lemmas is off because they don't read from left to right anymore.

[Yaël Dillies]

Reid Barton said:

Because it means you have to reason about two different instances of left_module (Rᵒᵖ) M at once, right?

Sounds like a job for another type synonym.

[Reid Barton]

But that's not really satisfactory because Rᵒᵖ was something that already existed and we might want to prove things about. e.g. continuing Johan's suggestion, two rings R and S are Morita equivalent if there is an R-S-bimodule and an S-R-bimodule such that tensoring them together yields R or S (depending on the order). Now Rᵒᵖ sometimes is Morita equivalent to R (e.g. for R commutative) and sometimes isn't; for example I randomly found https://arxiv.org/abs/1305.5139 which is about this question.

If it's impractical to talk about Morita equivalence of Rᵒᵖ and R (because Rᵒᵖ was "used up" by right_module; I am not sure whether this would really be a problem in practice), then it's not really satisfactory to say "welp, let's just phrase this theorem in terms of Rᵒᵖ' instead".

[Eric Wieser]

Reid Barton said:

two rings R and S are Morita equivalent if there is an R-S-bimodule and an S-R-bimodule such that tensoring them together yields R or S (depending on the order).

Are we anywhere close to being able to state this anyway? Does "yields" mean "isomorphic as a module"?

[Yaël Dillies]

And what ifright_module is the one consuming the new op-like type synonym?

[Eric Wieser]

I would lean towards just going ahead with "using up" opposite in this way, for the sake of:

So the advantage of using this encoding is we don't have to duplicate a lot of definitions/lemmas

and then revaluate once we have a working implementation to see what the problems look like

[Johan Commelin]

I think that once we have a definition of the tensor product in the non-commutative setting, then defining Morita equivalence is easy.
So in that sense, we are just as close to stating Morita equivalence as to solving the problems in this thread :wink:

[Reid Barton]

Yaël Dillies said:

And what ifright_module is the one consuming the new op-like type synonym?

Then you don't have this problem, but you might have to do more work to relate right modules over R to left modules over Rᵒᵖ instead, I guess?

[Reid Barton]

Eric Wieser said:

Reid Barton said:

two rings R and S are Morita equivalent if there is an R-S-bimodule and an S-R-bimodule such that tensoring them together yields R or S (depending on the order).

Are we anywhere close to being able to state this anyway? Does "yields" mean "isomorphic as a module"?

e.g. "yields R" means "is isomorphic to R as an R-R-bimodule"

[Eric Wieser]

"N is isomorphic to M as an R-S-bimodule" feels like something we're quite a way from being able to state

[Eric Wieser]

We'd need maps that are linear over multiple rings

[Eric Wieser]

Unless we phrase it as "N is isomorphic to M as an R ⊗[nat] S-module", assuming that makes any sense

[Reid Barton]

Eric Wieser said:

We'd need maps that are linear over multiple rings

Not "multiple" rings. Two rings! There are only two places where a ring can act, the left and the right

[Johan Commelin]

Nevertheless. We just had a pretty impressive refactor that gave us semi-linear maps. I don't know what Lean will think of us if we start explaining it about bi-semi-linear maps. If we want to keep it readable, we'll put quite some strain on the system, I fear.

[Reid Barton]

Anyways I think the more important question is whether it actually helps to use this encoding of right modules as left modules over the opposite ring at all

[Reid Barton]

I guess it only solves part of the problem anyways because right modules over Rᵒᵖ will be left modules over(Rᵒᵖ)ᵒᵖ which is not what we want

[Reid Barton]

I don't know what's best, but the point I wanted to make is it's not a "free win" to use the encoding with opposite

[Yaël Dillies]

Dumb question, why "left and "right"? Does it never happen to consider more than two actions?

[Jakob von Raumer]

Either its $(rs)m=r(sm)$ or it's $m(rs)=(mr)s$, so there are only two ways mulitplication and action can associate.

[Oliver Nash]

Number theorists love count the number of embeddings of a number field into the real / complex numbers so this gives multiple (left) actions of the same ring on the same target but I can't think of a situation where we'd want to regard anything like this as a module.

[Jakob von Raumer]

Reid Barton said:

Anyways I think the more important question is whether it actually helps to use this encoding of right modules as left modules over the opposite ring at all

We should keep in mind that in Lean 4

• We can write the feature providing to_additive in a more general way which could auto-generate rsmul-lemmas from smul-lemmas.
• We can have cycles in the type class system, so we will be able to have instance [comm_ring R] [left_module R M] : symmetric_module R M.

[Kevin Buzzard]

@Yaël Dillies It's like how the ring of a x a matrices acts on the left on the vector space of a x b matrices, and the ring of b x b matrices acts on the right.

[Eric Wieser]

We can have cycles in the type class system, so we will be able to have instance [comm_ring R] [left_module R M] : symmetric_module R M.

This isn't true, that instance constructs data in a way that will almost certainly create diamonds

[Eric Wieser]

Kevin Buzzard said:

Yaël Dillies It's like how the ring of a x a matrices acts on the left on the vector space of a x b matrices, and the ring of b x b matrices acts on the right.

Do we have that instance? If not, that sounds like an easy undergrad warmup project

[Yaël Dillies]

Ah so it's stemming the fact that multplication is binary?

[Jakob von Raumer]

Eric Wieser said:

This isn't true, that instance constructs data in a way that will almost certainly create diamonds

Well, diamonds would appear exactly in the cases where we had a right_module R M beforehand?

[Eric Wieser]

Yaël Dillies said:

Ah so it's stemming the fact that multplication is binary?

Fundamentally there are four types of instance in mathlib:

• Instances that derive from left-multiplication, docs#has_mul.to_has_scalar
• Instances that derive from right-multiplication, docs#has_mul.to_has_opposite_scalar
• Instances that derive from application, docs#function.End.apply_mul_action
• weird special cases that don't really fit with the rest of the picture

By "derive" I mean "products get this elementwise, polynomials get this coefficient-wise, functions get this codomain-wise, ..."

[Reid Barton]

What I meant is that there are exactly two ways in which a (noncommutative) ring can act, from the left or from the right. I guess you could also consider something with multiple compatible left actions (presumably by different rings to avoid confusion).

[Reid Barton]

Yaël Dillies said:

Ah so it's stemming the fact that multplication is binary?

It's ultimately because multiplication in a noncommutative ring is multiplication of a sequence of elements $abc...xyz$, and this sequence has two ends (a left end and a right end) where you could put a module instead.

[Reid Barton]

In the commutative case you just multiply an unordered collection of elements together and so there's only one "place" to put an element of a module, so there is only one kind of module over a commutative ring

[Eric Wieser]

Jakob von Raumer said:

Well, diamonds would appear exactly in the cases where we had a right_module R M beforehand?

Yes, but for any sort of composite type there will likely always be a right_module R M instance available; If M is a product type, the instance will exist that derives the instance from a right action on each half of the product.

That instance will be incompatible with the instance that derives a right_module from a symm_module, and derives a symm_module from each half, because even in a commutative ring a * b = b * a is not defeq

[Jakob von Raumer]

Thanks, good point.

[Eric Wieser]

Usually the way to avoid this type of diamond is to avoid ever constructing new data when inferring foo A from bar A

[Jakob von Raumer]

I was just fixing a file which requires a symmetric version of [algebra R A]. It's probably sufficient to do it with [algebra R A] [has_scalar (opposite R) A] [is_symmetric_smul R A] and derive an instance [algebra (opposite R) A] instead of creating a new class for the symmetry of algebras...

[Eric Wieser]

and derive an instance [algebra (opposite R) A]

This instance should already exist in the places you need it

[Eric Wieser]

That is, you should be using [algebra R A] [algebra (opposite R) A] [is_symmetric_smul R A]

[Jakob von Raumer]

But doesn't that introduce maps f : R →+* A and g : (opposite R) →+* A which have no connection with each other?

[Jakob von Raumer]

is_symmetric_smul only matches up the scalar part, not the ring hom

[Eric Wieser]

Sure, but you can prove the ring_homs are equal via docs#algebra.smul_def; it already is fully defined by the scalar part

[Jakob von Raumer]

don't know how to synthesize placeholder
context:
R : Type ?,
N : Type ?,
_inst_1 : monoid R,
_inst_2 : add_monoid N,
_inst_3 : distrib_mul_action Rᵒᵖ N
⊢ distrib_mul_action (units R)ᵒᵖ N

Any ideas on this? Probably worth first tranferring various classes of actions along equivalences...

[Eric Wieser]

docs#units.distrib_mul_action?

[Eric Wieser]

Combined with docs#mul_opposite.distrib_mul_action

[Eric Wieser]

Are you missing an import of group_theory.group_action.opposite?

[Jakob von Raumer]

Eric Wieser said:

Combined with docs#mul_opposite.distrib_mul_action

That's taking the opposite on the type that's operated on.

[Jakob von Raumer]

Eric Wieser said:

Are you missing an import of group_theory.group_action.opposite?

Do you mean algebra.opposites? That's the file I'm working in

[Eric Wieser]

algebra.opposites was split in two three, you must be behind master

[Jakob von Raumer]

Ouch, okay, I'll rebase

[Jakob von Raumer]

(Though the question still stands)

[Eric Wieser]

I assume distrib_mul_action (units Rᵒᵖ) N works fine?

[Jakob von Raumer]

Eric Wieser said:

I assume distrib_mul_action (units Rᵒᵖ) N works fine?

Yes, and we have an equivalence between units Rᵒᵖ and (units R)ᵒᵖ...

[Eric Wieser]

Yeah, I think the instance is missing and needs to be added manually, and can't be reasonably inferred transitively

[Jakob von Raumer]

There are probably quite some of these that might pop up...

[Eric Wieser]

I think I have a local unsaved buffer with the relevant code in it...

[Eric Wieser]

Yep

[Eric Wieser]

import group_theory.group_action.units
import algebra.opposites

-- turn off the bad instance we're tring to fix
local attribute [-instance] units.mul_action'

namespace units

open opposite

variables {G M α : Type*}

/-! Right actions on units - I can't think if a good way to inherit these from anything we already
have -/

instance units.op_has_scalar [monoid M] [has_scalar Mᵒᵖ α] : has_scalar (units M)ᵒᵖ α :=
{ smul := λ um a, op (um.unop : M) • a }

instance units.op_mul_action [monoid M] [mul_action Mᵒᵖ α] : mul_action (units M)ᵒᵖ α :=
{ smul := λ um a, op (um.unop : M) • a,
  one_smul := (one_smul Mᵒᵖ : _),
  mul_smul := λ um un, mul_smul (op (um.unop : M)) (op (un.unop : M)), }

/-! Notation just to make the intent behind the sorried lemma clear. -/

notation g` •> `:73 m:72 := g • m
notation m` <• `:73 g:72 := opposite.op g • m

variables [group G] [monoid M] [mul_action G M] [mul_action Gᵒᵖ M]

lemma smul_mul_inv_smul [is_scalar_tower G M M] (g : G) (m : units M)
  : (g •> (m : M)) * (↑(m⁻¹) <• g⁻¹) = 1 :=
calc (g •> (m : M)) * (↑(m⁻¹) <• g⁻¹)
    = g •> ((m : M) * (↑(m⁻¹) <• g⁻¹)) : by rw [←smul_eq_mul, ←smul_eq_mul, smul_assoc]
... = g •> ((m : M) * ↑(m⁻¹)) <• g⁻¹ : by {
    congr' 1,
    rw [←op_smul_eq_mul, ←op_smul_eq_mul],
    sorry -- we need `is_scalar_tower` for right actions
    }
... = g •> 1 <• g⁻¹ : by rw units.mul_inv
... = (g * g⁻¹) •> 1 : sorry  -- `smul_comm_class` is too strong here
... = 1 : by rw [mul_right_inv, one_smul]

#print group

lemma inv_smul_mul_smul [is_scalar_tower G Mᵒᵖ Mᵒᵖ] (g : G) (m : units M) : (↑(m⁻¹) <• g⁻¹) * (g •> (m : M)) = 1 :=
opposite.op_injective $ smul_mul_inv_smul g (units.op_equiv.symm (op m))

/-- A fixed version of `units.mul_action'`. -/
instance better_mul_action' [is_scalar_tower G M M] : mul_action G (units M) :=
{ smul := λ g m, ⟨g •> (m : M), ↑(m⁻¹) <• g⁻¹, smul_mul_inv_smul _ _, inv_smul_mul_smul _ _⟩,
  one_smul := λ m, units.ext $ one_smul _ _,
  mul_smul := λ g₁ g₂ m, units.ext $ mul_smul _ _ _ }

-- note: now only needs monoid not comm_monoid!
example {α : Type*} [monoid α] :
  (units.better_mul_action' : mul_action (units α) (units α)) = monoid.to_mul_action _ :=
rfl -- ok, no diamond any more

end units

[Eric Wieser]

I guess that was in response to some thread about units.mul_action' being bad

[Jakob von Raumer]

Ah, okay, units.mul_action' should not interfere with the PR

[Jakob von Raumer]

Jakob von Raumer said:

Ouch, okay, I'll rebase

That's one messy rebase :face_palm:

[Jakob von Raumer]

https://github.com/leanprover-community/mathlib/pull/10345/files Why is this showing a real diff for algebra.opposites if that file doesn't exist anymore in master?

[Eric Wieser]

A merge would likely be a lot easier

[Eric Wieser]

If you rebase n commits you can end up solving n conflicts, with a merge there's just one conflict.

[Jakob von Raumer]

Eric Wieser said:

A merge would likely be a lot easier

I don't think it made a difference, it's mostly the renamings from opposite to mul_opposite...

[Jakob von Raumer]

Made some progress today, but linear_algebra.alternating is still a bit stubborn. There is something wrong with a type class in there, but the issue seems so just have been patched over before. Here is one of the problematic lines, the other is were it fails at the bottom of the file...

[Jakob von Raumer]

FWIW the trace of the problematic search is here

[Jakob von Raumer]

The message at the bottom looks more like a diamond, but I'm not sure what's going on there either

type mismatch at application
  tensor_product.tmul_smul
term
  units.is_symmetric_smul
has type
  @is_symmetric_smul (@units ℤ int.monoid) ?m_1 (@units.has_scalar ℤ ?m_1 int.monoid ?m_2)
    (@units.op_has_scalar ℤ ?m_1 int.monoid ?m_3)
but is expected to have type
  @is_symmetric_smul (@units ℤ int.monoid) ?m_1
    (@mul_action.to_has_scalar (@units ℤ int.monoid) ?m_1
       (@div_inv_monoid.to_monoid (@units ℤ int.monoid)
          (@group.to_div_inv_monoid (@units ℤ int.monoid) (@units.group ℤ int.monoid)))
       (@distrib_mul_action.to_mul_action (@units ℤ int.monoid) ?m_1
          (@div_inv_monoid.to_monoid (@units ℤ int.monoid)
             (@group.to_div_inv_monoid (@units ℤ int.monoid) (@units.group ℤ int.monoid)))
          (@add_comm_monoid.to_add_monoid ?m_1 ?m_2)
          ?m_3))
    ?m_4

[Jakob von Raumer]

These are the typeclasses need for algebra_tensor_module.assoc:

_inst_1: comm_semiring R
_inst_2: comm_semiring A
_inst_3: algebra R A
_inst_4: algebra Rᵐᵒᵖ A
_inst_5: is_symmetric_smul R A
_inst_6: add_comm_monoid M
_inst_7: module R M
_inst_8: module Rᵐᵒᵖ M
_inst_9: is_scalar_tower Rᵐᵒᵖ R M
_inst_10: module A M
_inst_11: module Aᵐᵒᵖ M
_inst_12: is_symmetric_smul A M
_inst_13: is_scalar_tower R A M
_inst_14: is_scalar_tower Rᵐᵒᵖ A M
_inst_15: add_comm_monoid N
_inst_16: module R N
_inst_17: module Rᵐᵒᵖ N
_inst_18: is_symmetric_smul R N
_inst_19: add_comm_monoid P
_inst_20: module R P
_inst_21: module A P
_inst_22: is_scalar_tower R A P
_inst_23: module Rᵐᵒᵖ P
_inst_24: is_symmetric_smul R P
_inst_25: smul_comm_class Aᵐᵒᵖ Rᵐᵒᵖ M
_inst_26: is_scalar_tower Rᵐᵒᵖ A P
_inst_27: module Aᵐᵒᵖ P
_inst_28: is_symmetric_smul A P
_inst_29: is_scalar_tower Rᵐᵒᵖ R P
_inst_30: smul_comm_class Aᵐᵒᵖ R M

[Eric Wieser]

(deleted)

[Eric Wieser]

docs#algebra_tensor_module.assoc

[Jakob von Raumer]

Some of these might be made into instances, certain combination if is_scalar_tower and is_symmetric_smul especially.

[Jakob von Raumer]

Eric Wieser said:

docs#algebra_tensor_module.assoc

docs#tensor_product.algebra_tensor_module.assoc

[Jakob von Raumer]

I think we need tensor_product.left_action to be accompanied by a second file about the respective right action. ring_theory.tensor_product is missing this at some points

[Jakob von Raumer]

Jakob von Raumer said:

I think we need tensor_product.left_action to be accompanied by a second file about the respective right action. ring_theory.tensor_product is missing this at some points

Okay, the next issue is that these things overlap: We want the right action of $S$ on $M \otimes_R N$ to come from a right action on $N$ and the left action of $S$ on $M \otimes_R N$ to come from a left action on $M$. But if for example $M$ is an $S$-$S$-bimodule, there's already the $S^{op}$ action on $M$ that induces an action on the tensor product, that is because right actions are defined as a special case of left actions.

Any ideas on how to deal with this?

[Eric Wieser]

Yes, this was the problem I was describing much earlier, and I'm not sure how to solve it

[Eric Wieser]

Having separate right_mul R and left_mul R types instead of opposite R and R would work, but I suspect that would be very painful

[Eric Wieser]

My suspicion is that when such a case arises in practice the two actions are equal anyway propositionally, and to just accept the definitional typeclass diamond for now

[Jakob von Raumer]

We only have an instance algebra R (A ⊗[R] B) but need one for the "right algebra" (do people actually consider those?), too. So I guess we should find a good generalisation of algebra.tensor_product.tensor_product.algebra (that name...) that captures both

[Johan Commelin]

I guess the problem would be solved if we completely uncouple left and right actions. But that would mean a lot of duplication.

[Reid Barton]

AFAIK "$R$-algebra" only ever makes sense when $R$ is commutative

[Julian Külshammer]

To comment on Reid's point: "R-algebra" indeed requires R to be commutative and furthermore that the action of R is central in the algebra, i.e. the image of R is in the center of the algebra. There is the more general notion, sometimes called an R-ring, where R can be non-commutative (a reformulation is that an R-ring is a monoid object in the category of R-R-bimodules.

[Jakob von Raumer]

Reid Barton said:

AFAIK "$R$-algebra" only ever makes sense when $R$ is commutative

Sure, but right now that's decoupled from the question of whether the scalar can act on the right. So with the current approach of my PR, we need algebra Rᵐᵒᵖ (A ⊗[R] B)

[Jakob von Raumer]

Johan Commelin said:

I guess the problem would be solved if we completely uncouple left and right actions. But that would mean a lot of duplication.

Hm, I'm not sure if I should continue the current PR until there's a decision on this :(

[Jakob von Raumer]

(The tensor product algebra issue is an issue dependent on this, though, sorry for brining both points up at once ^^)

[Johan Commelin]

Completely uncoupling only seems feasible if there is a tactic @[to_right_action] that autogenerates all the duplicate lemmas.

[Reid Barton]

Jakob von Raumer said:

Reid Barton said:

AFAIK "$R$-algebra" only ever makes sense when $R$ is commutative

Sure, but right now that's decoupled from the question of whether the scalar can act on the right. So with the current approach of my PR, we need algebra Rᵐᵒᵖ (A ⊗[R] B)

It always acts on the right too, by the same action (because R is central).

[Jakob von Raumer]

So, generally speaking, algebra R A should induce algebra Rᵐᵒᵖ A, even if A is not commutative?

[Jakob von Raumer]

Ah, I guess that makes sense if the action is central...

[Reid Barton]

An R-algebra is a monoid in R-modules taken in the commutative sense, where there is no "left" or "right".

[Jakob von Raumer]

In the current hierarchy where it extends module, it inherits a sense of "left" and "right"

[Jakob von Raumer]

But yea, if there's no conceivable scenario where there's a distinction, we should just have an instance adding the symmetric action

[Eric Wieser]

It's not safe today to add that instance, we already discussed why much earlier in the thread

[Eric Wieser]

Probably the way to go here is to add an op_smul_def and op_smul field to algebras, so that they can decay to either left or right modules with the right definitional equality

[Eric Wieser]

How many docs#algebra instances would that mean we have to fix?

[Jakob von Raumer]

Eric Wieser said:

It's not safe today to add that instance, we already discussed why much earlier in the thread

Sorry, I keep forgetting about that issue...

[Jakob von Raumer]

Eric Wieser said:

Probably the way to go here is to add an op_smul_def and op_smul field to algebras, so that they can decay to either left or right modules with the right definitional equality

That would mean that algebra R A implies an instance of both module R A, module (opposite R) A and is_symmetric_smul R A, right?

[Eric Wieser]

Yes, exactly

[Eric Wieser]

And smul_comm_class R Rᵒᵖ A too

[Jakob von Raumer]

It probably being enough to constitute another PR, I'll nevertheless go ahead and just add an instance for algebra Rᵐᵒᵖ (A ⊗[R] B) as a workaround until then...

[Jakob von Raumer]

Johan Commelin said:

Completely uncoupling only seems feasible if there is a tactic @[to_right_action] that autogenerates all the duplicate lemmas.

Uncoupling would also solve the issue about "usability". The way it is now, we have variables r : opposite R, which we have to rewrite backwards op_unop to really get the notation on the right side we'd expect....

[Eric Wieser]

I just made a spinoff PR (#10543) that defines is_symmetric_smul, but with all the instances as early as possible instead of all in one place

[Jakob von Raumer]

Just fixed to spots where apply @tensor_product.ext_threefold R gave a timeout but apply @tensor_product.ext_threefold R _ works fine :thinking:

[Johan Commelin]

@Eric Wieser Thanks for that PR. I guess there is no harm in merging it, even if we later decide that completely uncoupling left and right actions is the way to go. Right?

[Eric Wieser]

Even if we uncouple we'll still want a class for that compatibility

[Eric Wieser]

Eric Wieser said:

Probably the way to go here is to add an op_smul_def and op_smul field to algebras, so that they can decay to either left or right modules with the right definitional equality

I started having a go at this in #10716

[Jakob von Raumer]

Did the search and replace now, but I guess for everything else, #10716 should be merged first

[Johan Commelin]

The diamonds from #10716 probably will not be a problem for the time being.

[Johan Commelin]

Still, I wonder if we should find a once-and-for-all solution to these problems. Making add_comm_monoid bigger and bigger all the time doesn't seem like the correct solution to me.

[Johan Commelin]

Or maybe it is?

[Kevin Buzzard]

I showed one of my kids the definition yesterday and they said "oh cool you can override powers, you can use that to make exponentiation more computationally efficient"

[Johan Commelin]

And you replied: "but we want it to be more efficient for proving!" :rofl:

[Kevin Buzzard]

but we have the API for that!

[Jakob von Raumer]

Johan Commelin said:

The diamonds from #10716 probably will not be a problem for the time being.

Yes, but all algebras being central will save me lots of edits...

[Kevin Buzzard]

Maybe now is a good time to define central simple algebras?

[Julian Külshammer]

I would be very happy to see these generalisations merged. I think they are very important to get (different flavours of) non-commutative algebra going.

[Jakob von Raumer]

I don't know what's the status of #10716. @Eric Wieser ?

[Eric Wieser]

It needed a few other dependent PRs first I think

[Eric Wieser]

And generally working through all 70 instances of algebra

[Eric Wieser]

I think I'm through about 25 of them

[Eric Wieser]

The most annoying part of the change seems to be that module.End R M is now only an algebra when M is a bimodule

[Eric Wieser]

But mathematically the distinction is meaningless given R is commutative anyway, so it's nothing more than an annoyance

[Eric Wieser]

I share Johan's view that the new diamonds are unlikely to cause any trouble any time soon.

[Julian Külshammer]

Eric Wieser said:

The most annoying part of the change seems to be that module.End R M is now only an algebra when M is a bimodule

This makes sense to me as Hom_R(M,N) has the structure of an S-T-bimodule if M is an R-S-bimodule and N is an R-T-bimodule. You should have to assume an instance is_central_scalar to get an algebra structure on End R M.

[Eric Wieser]

That comment worries me, as it seems to describe a S action on f : M →ₗ[R] N that comes from M alone. Is that action(s • f) m = f (s • m)? We don't have any actions like that in mathlib right now, and if we did we'd have some troubling diamonds

[Julian Külshammer]

That is the action, but it is a right action. Why it is a problem for Hom and not for the tensor product? There the analogue is that if M is an R-S-bimodule and N is an S-T-bimodule, then M\otimes N is an R-T-bimodule. (The standard convention is that when saying R-S-bimodule, the R-action is from the left while the S-action is from the right.)

[Eric Wieser]

We have a lot of precedent for function-like types that says "actions operate on the codomain", where actions includes left and right actions. We don't have much precedent for tensor products to worry about in comparison.

[Eric Wieser]

(I tried to edit the above to reflect the correct right/left-ness of the actions)

[Julian Külshammer]

Do you have some proposal what to do about that? Non-commutative algebraists definitely want to take about both actions, an action on Hom_R(M,N) induced by a right action on M as well as an action induced by a left action on N. And in general they are different.

[Eric Wieser]

The only suggestion I can think of is a dom_act type alias to force the action to apply to the domain

[Eric Wieser]

But even that doesn't work very well if we want to apply to the second argument of a bilinear function, unless we also have cod_act

[Eric Wieser]

If we go down that route, then scaling of fin 3 -> R ends up being written as cod_act r • v which is pretty unpleasant

[Julian Külshammer]

There is an important difference between the arrows here (again informally speaking, I don't know how easy it would be for lean to figure out the difference): If you talk about the undecorated arrow fin 3 -> R, then the (left) action on R should come from a (left) action on R. On the other hand, when talking about an action on the decorated arrow M \to_l [R] N, then the (left) R-action is, loosely speaking, already used, so any left action on this space should come from a right action on M whereas any right action should come from a right action on N.

[Oliver Nash]

@Julian Külshammer is right of course: in the special case of linear maps (between compatible bimodules) all is well, at least mathematically, because the space of maps carries just one left action and one right action.

[Oliver Nash]

But we still have the problem that Mathlib cannot talk about the scalar actions (contravariantly) induced from actions on the domain for general classes of functions. To take a concrete example, I might well want to formalise something about the regular representation of a finite subgroup of non-zero complex numbers.

[Oliver Nash]

import algebra.group.units
import data.complex.basic

variables (G : subgroup (units ℂ)) (f : G → ℂ) (z : G)

/- OK so now what does `z • f` mean?

Informally I might be talking about the (left) regular representation or
I might be talking about a pi action, regarding `z` as an element of `ℂ`.

Because we have so many diamonds (all fortunately defeq) it's not even easy
to "switch off" the unwanted action locally. E.g., uncomment any one of these
`local attribute [-instance]` statements and the `example` below succeeds. -/

local attribute [-instance] pi.has_scalar
local attribute [-instance] pi.mul_action
local attribute [-instance] pi.mul_action_with_zero
local attribute [-instance] pi.module
local attribute [-instance] pi.algebra

example (w : G) : (z • f) w = z * (f w) := rfl

[Oliver Nash]

Of course what we really have above is a $G × G$ action on $G \to ℂ$ and in Mathlib we single out the first (covariant) factor for priority. More generally:

[Oliver Nash]

import group_theory.group_action.pi

open mul_opposite

variables {M N : Type*} (A B C D : Type*)
variables [monoid A] [monoid B] [monoid C] [monoid D]

-- Give M left `A` and right `B` action, aka (A, B)-biaction
variables [mul_action A M] [mul_action Bᵐᵒᵖ M]

-- Give N left `C` and right `D` action, aka (C, D)-biaction
variables [mul_action C N] [mul_action Dᵐᵒᵖ N]

-- What we really have is a (B × C, A × D)-biaction.
instance pi.mul_action_prod : mul_action (B × C) (M → N) :=
{ smul     := λ bc f x, bc.snd • f ((op bc.fst) • x),
  one_smul := by simp,
  mul_smul := λ b₁ b₂ f, by { ext, simp [mul_smul], }, }

-- needed because `Aᵐᵒᵖᵐᵒᵖ ≠ A` so have missing `[mul_action Aᵐᵒᵖᵐᵒᵖ M]` issue
instance pi.mul_action_prod_op : mul_action (Aᵐᵒᵖ × Dᵐᵒᵖ) (M → N) :=
{ smul     := λ ad f x, ad.snd • f (ad.fst.unop • x),
  one_smul := by simp,
  mul_smul := λ a₁ a₂ f, by { ext, simp [mul_smul], }, }

[Oliver Nash]

I also cannot think of a way to solve this problem except by means of a type synonym for the contravariantly-induced actions.

[Oliver Nash]

I think we can avoid facing up to this for bimodules but we'll have to confront it eventually.

[Julian Külshammer]

@Oliver Nash Just to have an example in this conversation: In what area of maths is your more general situation needed?

[Oliver Nash]

@Julian Külshammer how about the example I gave above of the regular representation of a finite group, or more generally the permutation representation associated to the action of a group G on a set X? Given this data one can pick some scalars k and study the representation of G induced on X → k.

[Oliver Nash]

I gave the example where G is a finite subgroup of ℂ* acting on itself by multiplication and the scalars ℂ above to show that even informally there can be ambiguity.

[Julian Külshammer]

@Oliver Nash Thanks for the examples, but as far as I understand, this seems to be a general pattern for group actions: That there is often more than one you can consider. I remember there being an extensive discussion whether the regular action of a group on itself should be an instance in light of there also being the conjugation action, etc. Do you see an issue with going ahead with the bimodule case?

[Oliver Nash]

I don't see an issue with bimodules for the reason you highlighted: restricting to the left/right-linear maps cuts out two of the group actions so the ambiguity vanishes on these maps.

[Oliver Nash]

We'll probably just keep putting off issues like this until we are forced to solve / work around them.

[Oliver Nash]

As I said above, there is even ambiguity when working informally. If $f : ℂ^* → ℂ$ and $z ∈ ℂ^*$ then what do I mean by $z • f$?

[Kevin Buzzard]

Certainly if G acts on A and B and we have f:A->B then sometimes (gf)(a) means g(f(a)) and sometimes g(f(g^{-1}a)). Empirically I think that the former is common when f is known to be G-equivariant (because then the latter action is trivial) and conversely the latter is common when f is just an abelian group homomorphism (in which case the G-equivariant homs are the fixed points under the latter action)

[Julian Külshammer]

So it seems that there is agreement that no action should be preferred for maps f:A->B but that there is no harm registering an action on f:M->[R] N for bimodules M and N.

[Oliver Nash]

Yes, to the second clause (about registering an action on linear maps between bimodules) but no to the first clause since we already have a preferred action registered, namely docs#pi.has_scalar

[Eric Wieser]

Jakob von Raumer said:

I don't know what's the status of #10716. Eric Wieser ?

I made some more progress, but am now concluding that normed_space and seminormed_space probably want to be two-sided too. That refactor would be twice as easy if #8218 weren't hitting problems

[Eric Wieser]

A status update on #10716: I was able to get past the normed_space and seminormed_space problems, and am back to finding random types that are missing is_central_scalar instances (next up: continuous_linear_map,affine_map, continuous_map)

[Eric Wieser]

Next up is docs#smooth_map.algebra (: algebra 𝕜 C^∞⟮I, N; 𝓘(𝕜, A), A⟯), which is well beyond my paygrade. What's missing is the fact that this currently requires 𝕜-multiplication to be smooth in values of k, even though that's obviously not necessary as the smooth functions are a nat-algebra (and I assume this doesn't count as smooth).

To express that, I'd need a smooth_const_smul variant of smooth_smul with much weaker requirements on 𝕜.

[Heather Macbeth]

@Eric Wieser I can try to help here but I don't understand what you're asking -- what do you mean by "the smooth functions are a nat-algebra"?

[Eric Wieser]

Sorry, my statement was a little murky and #xy'd there. The actual missing piece is a module 𝕜ᵐᵒᵖ C^∞⟮I, N; 𝓘(𝕜, A), A⟯ instance. It's easy to write that instance specifically, but it would be nice if it fell out as a specialization of a more general docs#smooth_map.has_scalar like it does on most other types.

[Eric Wieser]

The nat comment was simply a remark that "the generalized version would optimistically work for nat-actions too"

[Eric Wieser]

Update: #10716 now builds! Unfortunately the fails_quickly linter is unhappy, but I suspect that's just because a bunch of typeclass searches got longer.

[Eric Wieser]

(I've got it building again and resolved conflicts, but the fails_quickly problem remains)

[Eric Wieser]

CI is fully green :tada:

[Johan Commelin]

Thanks for that massive effort. I would be happy to merge this asap. But it would be good if some others also take a look.

[Johan Commelin]

From the PR message:

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.

[Riccardo Brasca]

Having a look.

[Riccardo Brasca]

I am only a little bit worried that now we often have to write

variables [add_comm_group M] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M]

to mean that M is a R module (even if R is commutative), but I don't see a simpler way of avoiding this.

[Eric Wieser]

I'm happy to split the PR into two if necessary - the merge conflicts are usually straightforward, and I don't envisage any similar timeouts

[Eric Wieser]

(the split would be; add random missing right actions, then do the actual titular change)

[Eric Wieser]

Riccardo Brasca said:

I am only a little bit worried that now we often have to write

variables [add_comm_group M] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M]

to mean that M is a R module (even if R is commutative), but I don't see a simpler way of avoiding this.

In lean4 we can have class really_a_module extends module R M, module Rᵐᵒᵖ M, is_central_scalar R M and things should work out ok

[Eric Wieser]

(c.f.my_sql_real_escape_string, the version of my_sql_escape_string that ... actually escapes the string. /s)

[Eric Wieser]

In lean 3 if we want to do that we have to add a new (trivial) instance next to every docs#module instance (there are 133 of them); which is certainly doable, but annoying.

[Eric Wieser]

(I guess in practice it would just be next to the docs#is_central_scalar instances, of which there are only 52)

[Eric Wieser]

Eric Wieser said:

I'm happy to split the PR into two if necessary - the merge conflicts are usually straightforward, and I don't envisage any similar timeouts

Two easy splits: #13995 and #13996

[Eric Wieser]

The first of those is merged, but @Scott Morrison expressed some hesitation on the second

[Scott Morrison]

Okay, re: #13996, I think that if M has commuting actions of L and R (maybe you can think of these as left and right actions, so R is syntactically Bᵒᵖ for some B, but it should really matter), and L is an A algebra, then restrict_scalars A L M should have an action of A and an action of R, and an instance saying these commute.

[Scott Morrison]

(It should not have an action of L anymore.)

[Scott Morrison]

In particular, for the instance I complained about in the PR, the docstring says:

/--
When `M` is a right-module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
right-module structure over `R`.
The preferred way of setting this up is
`[module Rᵐᵒᵖ M] [module Sᵐᵒᵖ M] [is_scalar_tower Rᵐᵒᵖ Sᵐᵒᵖ M]`.
-/

and I agree with that doc-string completely.

However the instance we need in this situation is module Rᵐᵒᵖ (restrict_scalars Rᵐᵒᵖ Sᵐᵒᵖ M), and this already exists, by ignoring the presence of all the ᵐᵒᵖs.

[Scott Morrison]

In the situation (not mentioned in the doc-string, but in the comment) where you have something that is an R and Rᵐᵒᵖ module with commuting actions (i.e. in normal language an R-R-bimodule), and R is an S-algebra and you want to obtain the resulting S-S-bimodule, then I think you either need to say

restrict_scalars S R (restrict_scalars Sᵐᵒᵖ Rᵐᵒᵖ M)

or invent a new type synonym (or abbreviation?) for this situation.

[Scott Morrison]

The problem is just that we are going to have L-R bimodules, and subalgebras A in L and B in R, and we want to restrict an L-R bimodule M to obtain the A-B bimodule. We have to have a way to express this. And then, in the special case that L = R, we need to make sure we use the same language.

[Eric Wieser]

restrict_scalars A L M should have an action of A and an action of R, and an instance saying these commute.

Putting aside the actual contents of my PR, I don't think it is even possible to define this R action without adding back the L action (that you wanted to get rid of) by accident

[Eric Wieser]

Perhaps it helps to remember that restrict_scalars is really just a hack to avoid writing out annoying is_scalar_tower arguments; the latter spelling already works for considering the L-R bimodule as an A-B bimodule.

[Eric Wieser]

The option of defining a new type synonym restrict_scalars₂ A B L R M is at least a viable one, but I'd be hesitant to add it until we actually need it.

[Scott Morrison]

Eric Wieser said:

Putting aside the actual contents of my PR, I don't think it is even possible to define this R action without adding back the L action (that you wanted to get rid of) by accident

Oh you mean that (maybe only for a commutative L?) the original L action would commute with itself, so if we wanted to carry along the R action on the restrict_scalars synonym, the same mechanism would bring along the L action as well.

[Scott Morrison]

Hmmm

[Oliver Nash]

Eric Wieser said:

Perhaps it helps to remember that restrict_scalars is really just a hack to avoid writing out annoying is_scalar_tower arguments

I said this before and I didn't convince anyone but FWIW I think our restrict_scalars is a misnomer and would be better called enrich_scalars. True restriction of scalars happens invisibly for us via the forgetful functors that the typeclass mechanism constantly applies. Also, although it can be incorrectly used as a hack to avoid writing out is_scalar_tower arguments, restrict_scalars is a necessary tool in some situations (e.g., if one has a vector space
over a field of characteristic zero and wishes to make use of the ℚ-algebra structure).

Anyway I don't want to derail this thread.

[Scott Morrison]

Okay, so I guess I want to retract the statement that you quoted, @Eric Wieser. Instead we should look at the syntactic form of the rings acting, and only "carrying along" an Rᵐᵒᵖ action on a generic restrict_scalars A L M, but additionally carrying along any L action on restrict_scalars Bᵐᵒᵖ Rᵐᵒᵖ M.

[Scott Morrison]

I think then restrict_scalars A L M will then correctly be an A-R bimodule (ie commuting actions of A and Rᵐᵒᵖ), and nothing else,

[Scott Morrison]

while restrict_scalars Bᵐᵒᵖ Rᵐᵒᵖ M will be an L-B bimodule (ie commuting actions of L and Bᵐᵒᵖ).

[Eric Wieser]

Doesn't this suggestion mean we need a different spelling of restricting the scalars of an algebra to an algebra over a smaller ring?

[Eric Wieser]

Namely, we have to use restrict_scalars S R (restrict_scalars Sᵐᵒᵖ Rᵐᵒᵖ A) for that case, which is rather annoying

[Eric Wieser]

Scott Morrison said:

but additionally carrying along any L action on restrict_scalars Bᵐᵒᵖ Rᵐᵒᵖ M.

furthermore this isn't actually possible, since L has nothing to match syntactically against

[Eric Wieser]

Oliver Nash said:

Also, although it can be incorrectly used as a hack to avoid writing out is_scalar_tower arguments, restrict_scalars is a necessary tool in some situations (e.g., if one has a vector space
over a field of characteristic zero and wishes to make use of the ℚ-algebra structure).

(this could be framed as a hack to avoid writing out the "nonsense" [algebra ℚ A] [is_scalar_tower ℚ K A])

[Scott Morrison]

Okay, I think I am retreating to the position that restrict_scalars A L M should carry no additional instances (beyond module A ...).

[Scott Morrison]

and if you need additional instances for a commuting right action, we ought to have a different type synonym...

[Eric Wieser]

So [algebra S R] [algebra R A] : algebra S (restrict_scalars S R A) should no longer be true?

[Eric Wieser]

I think it's innocuous enough to copy across the right action just so that for the two frequence cases (restricting a left module and restricting a bimodule over a commutative ring), it does the sensible thing.

[Eric Wieser]

Note in particular that docs#restrict_scalars.lsmul only makes sense if restrict_scalar R S M is a bimodule over R, otherwise module.End R (restrict_scalars R S M) isn't actually an algebra.

[Scott Morrison]

Eric Wieser said:

So [algebra S R] [algebra R A] : algebra S (restrict_scalars S R A) should no longer be true?

Sorry, I'm being slow. Why couldn't we have this?

[Eric Wieser]

In the wider context of this thread, the proposed change is that algebra R A induces module Rᵐᵒᵖ A

[Eric Wieser]

So to produce algebra S (restrict_scalars S R A), we need to produce a module Sᵐᵒᵖ (restrict_scalars S R A) along the way

[Eric Wieser]

We can't get away with only doing it when A is an algebra though (which is what I initially tried); we also need this instance if we want

instance [algebra S R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] :
  algebra S (module.End S (restrict_scalars S R M))

to be allowed, which we need for what I described in this message

[Notification Bot]

27 messages were moved from this topic to #PR reviews > #13996 right actions on restrict_scalars by Eric Wieser.

[Eric Wieser]

Both are now merged and #10716 is green again; I'd appreciate any suggestions for further splits

[Jakob von Raumer]

Wow, happy to see this finally done :smiley:

[Eric Wieser]

Ok, I was perhaps wrong about it being easy to keep up to date with master. It's green once more

[Eric Wieser]

Unfortunately this is now definitely lost to the mathlib4 porting tide, and will need to wait now until the port is over. It turns out though that the is_central_scalar class was still useful for defining the dual numbers over a non-commutative ring in #18384

[Eric Wieser]

Eric Wieser said:

(Oh, also I remembered the other place where I wanted symmetric actions; I wanted to generalize docs#derivation so that I could use it on square matrices, without breaking all the existing commutative uses)

I had a go at this in #18936; I don't think this has any future in mathlib3, but it was surprisingly easy.
The difficulty arises when it comes to maps which are both left- and right- linear.