Multiplication by an element as a linear map

Stream: mathlib4

[Michael Stoll]

Is there a definition that gives (left) multiplication by an element of an R-algebra on the algebra as an R-linear map?
@loogle ⊢ LinearMap .., Algebra, _ * _

[loogle]

:search: Submodule.mulMap'

[Michael Stoll]

(This involves tensor products and is not what I'm looking for.)

[Yaël Dillies]

docs#LinearMap.mulLeft ?

[Michael Stoll]

I'll never learn that I may have to look for docs#SMulCommClass instead of docs#Algebra ...
Can loogle be made smarter in this respect?

[Eric Wieser]

exact? will help youhere I think

[Michael Stoll]

Even when looking for a specific term of a type and not a Prop?

[Eric Wieser]

I guess for that specific type it might choose id

[Michael Stoll]

or the zero map...

[Michael Stoll]

Indeed:

import Mathlib

variable {R S : Type*} [CommRing R] [Ring S] [Algebra R S]

example : S →ₗ[R] S := by exact? -- Try this: exact LinearMap.id

[Eric Wieser]

@loogle (_ : ?R →ₗ[_] ?R) ?x = ?y * ?x

[loogle]

:exclamation: <input>:1:17: expected end of input

[Eric Wieser]

I don't understand that loogle error

[Edward van de Meent]

i think there may be some weird space characters in there?

[Edward van de Meent]

specifically, those around the ?x

[Edward van de Meent]

strangely, i can't seem to reproduce the issue when trying to find out what kind of space it is... but replacing the spaces and then searching at the loogle site does fix the issue...

[Junyan Xu]

Yeah, it seems copying from VSCode or the online docs both have chances to confuse Loogle. Maybe it's some kind of rich text being copied?

[Eric Wieser]

I typed this literally into loogle

[Eric Wieser]

I think it likes inserting non-breaking spaces as part of the symbol replacement

[Jireh Loreaux]

I still think it would be nice to have a NonUnitalAlgebra class, as often whether you need SMulCommClass or IsScalarTower is sometimes just an artifact of on which side things happen, and in a (even non-unital) algebra the answer is: I just don't care.

[Jireh Loreaux]

I've experienced this too with typing things directly into loogle. Eric, are you using m17n for globally available input? I am. I think I didn't experience this before loogle supported it's own input mechanism.

[Kim Morrison]

Michael Stoll said:

Indeed:

import Mathlib

variable {R S : Type*} [CommRing R] [Ring S] [Algebra R S]

example : S →ₗ[R] S := by exact? -- Try this: exact LinearMap.id

You might try exact? using x.

[Andrew Yang]

Or if you know that the map is actually a ring homomorphism then this works

 import Mathlib

variable {R S : Type*} [CommRing R] [Ring S] [Algebra R S]

example : R →+* S →ₗ[R] S := by exact? -- Try this: exact Module.toModuleEnd R S

[Eric Wieser]

Jireh Loreaux said:

I've experienced this too with typing things directly into loogle. Eric, are you using m17n for globally available input? I am. I think I didn't experience this before loogle supported it's own input mechanism.

No, I am only using Loogle's own input method.

[Michael Stoll]

Kim Morrison said:

You might try exact? using x

It's close:

import Mathlib

variable {R S : Type*} [CommRing R] [Ring S] [Algebra R S]

example (x : S) : S →ₗ[R] S := by exact? using x -- Try this: exact LinearMap.mulRight R x

(However, my experience is that apply? using in real-life situations almost always says that it didn't find anything, even though a blank apply? finds something involving the exact same hypothesis. I'll try to remember posting a concrete example when I'm runnnig into that the next time.)

[Kim Morrison]

Yes, the using clause seems really buggy. I would be very happy if someone wanted to investigate / make a bug-fix PR!