Right multiplication as a mul_action

Stream: general

[Eric Wieser]

We have docs#monoid.to_mul_action which defines ∀ x y : R, x • y = x * y. Is there (or should there be) some alias such that ∀ x y : R, foo x • y = y * x?

[Adam Topaz]

This won't satisfy the associativity condition for a mul action

[Adam Topaz]

We need a notion of an action on the right (right mul action, right modules, etc.)

[Mario Carneiro]

it will in a comm ring, but I guess there is no point in a separate definition in that case

[Mario Carneiro]

I hope we can get by with mul actions by the opposite ring instead of right modules

[Eric Wieser]

This won't satisfy the associativity condition for a mul action

Won't it?

instance monoid.opposite_to_mul_action (R : Type*) [monoid R] : mul_action (opposite R) R :=
{ smul := λ c x, x * c.unop,
  one_smul := by simp,
  mul_smul := λ r s x, by simp [mul_assoc] }

instance (R : Type*) [monoid R] : mul_action (opposite R) (fin 3 → R) :=
by apply_instance

[Adam Topaz]

We have the has_pow class, why not have a pow_action?

[Adam Topaz]

Which would really just be a right action

[Adam Topaz]

$(a^x)^y = a^{xy}$

[Mario Carneiro]

@Eric Wieser isn't that just monoid.to_mul_action using the opposite mul?

[Eric Wieser]

I don't understand your question. It seems to satisfy my original request:

example (R : Type*) [monoid R] (x y : R) : opposite.op x • y = y * x := rfl

[Eric Wieser]

Does that instance above seem like a good idea to you?

[Eric Wieser]

(along with a similar one for semiring.to_semimodule etc)

[Eric Wieser]

The instance would be useful here: https://github.com/leanprover-community/mathlib/pull/7572/files#r633152366

[Mario Carneiro]

I'm basically wondering how this instance relates to the mul_action (opposite R) (opposite R) instance coming from monoid.to_mul_action. Is it the same?

[Eric Wieser]

Yes, they're definitionally equal but only if you abuse the type aliases a bit

[Eric Wieser]

#7630

[Eric Wieser]

Should we introduce a notation for this? notation a ` •← `:72 b:73 := op b • a is pretty bad but is a start:

import algebra.module.opposites

notation a ` •← `:72 b:73 := op b • a

-- precedence:
example {R} (a b c d e : R) [monoid R] :
  (a • b • c •← d •← e) = (((a • (b • c)) •← d) •← e) := rfl

[Oliver Nash]

Probably this is worse but we could also consider a↶b.

[Eric Wieser]

Here's a fun vscode unicode rendering bug:

-- safe: ≃, •⃖
-- fail: =, •⃖
-- safe: ≃, •⃖

The symbol at the end of each line is the same, but in my vscode and chrome they render differently

[Gabriel Ebner]

Should there be difference between the three lines? For me, only the ≃ and = differs (in both vscode and chromium).

[Bryan Gin-ge Chen]

The symbols at the end of each line all appear the same in Firefox on macOS, using DejaVu Sans Mono:
Screen-Shot-2021-05-26-at-12.43.22-PM.png

[Gabriel Ebner]

This is a weird bug seemingly connected to font fallback. I've been playing around with the Zulip CSS:

font-family: "Source Code Pro", monospace; /* default, broken */
font-family: "Source Code Pro", "DejaVu Sans Mono";
 /* works, reported fallback font is DejaVu Sans */
font-family: "Source Code Pro"; /* works as well, reported fallback font is DejaVu Sans */

[Eric Wieser]

In chrome on windows:

image.png

[Eric Wieser]

At any rate, that probably means the syntax I was trying is _not_ a good idea!

[Gabriel Ebner]

Chromium (actually electron) on linux:
weird_glyph.png