Puzzle: noncommutative RingHom as typeclasses

Stream: maths

[Junyan Xu]

Algebra R A is the typeclass to designate a preferred RingHom from a CommSemiring R to a Semiring A whose image lies in the center. How can we specify a preferred RingHom whose image doesn't necessarily lie in the center using existing mathlib typeclasses, even better, for not necessarily commutative Semiring R?

Hint 1

The typeclasses do not include the data of a map from R to A.

Hint 2

Two typeclasses are enough.

[Eric Wieser]

Isn't the answer to this in the docs for Algebra?

[Junyan Xu]

Indeed, though not very explicitly. That's a better hint than my Hint 3, so I removed it.
Here's another puzzle that eventually led me to discover this:

Puzzle

Let B be an A-module and let C be a B-module and A-module such that C/B/A is a tower. Suppose C is free as a B-module, so there's a B-LinearEquiv between Finsupp I B and C for some indexing type I. Show that any such LinearEquiv must also be an A-LinearEquiv. (When I is nonempty we deduce that B/B/A is also a tower.)

[Junyan Xu]

Puzzle 1 (statement formalized)

import Mathlib.Algebra.Module.Basic

example {R A} [Semiring R] [Semiring A] :
(R →+* A) ≃ { inst : Module R A // IsScalarTower R A A } := sorry

Puzzle 2 (statement formalized)

import Mathlib.LinearAlgebra.Basis

example {ι R S M} [Semiring R] [Semiring S] [AddCommMonoid M]
[Module R S] [Module R M] [Module S M] [IsScalarTower R S M]
(f : M ≃ₗ[S] ι →₀ S) : IsLinearMap R f := sorry

[Junyan Xu]

Do you know if this (the first puzzle) can be found in the mathematical literature? My impression is that one of the typeclasses involved is the mathlib community's invention.

[Junyan Xu]

I've minimized Puzzle 2 down to the statement that M/S/R being a tower implies that any S-linear map from S to M is also R-linear.

[Eric Wieser]

Aren't you just describing docs#LinearMap.restrictScalars ?

[Junyan Xu]

You don't a priori have the CompatibleSMul condition. Proving the condition is exactly (minimized) Puzzle 2.

[Junyan Xu]

I just opened #9046

[Junyan Xu]

Aren't you just describing docs#LinearMap.restrictScalars ?

This is a good point though, I should be adding CompatibleSMul instance rather than IsLinearMap lemmas ...