Base change of algebra morphism

Stream: Is there code for X?

[Dion Leijnse]

Given a ring R, two R-modules M and N and an R-algebra A, the definition LinearMap.baseChange extends f to a morphism of A-modules

baseChange A f : A ⊗[R] M →ₗ[A] A ⊗[R] N.

I was wondering if there is an extension of this to algebra morphisms. Here is a mwe of what I want:

variable (R A B : Type) [CommRing R] [Ring A] [Algebra R A] [CommRing B] [Algebra R B]
variable (S : Type) [CommRing S] [Algebra R S]
variable (f : A →ₐ[R] B)

-- Base extension as Linear map
noncomputable example : TensorProduct R S A →ₗ[S] TensorProduct R S B := LinearMap.baseChange S f

-- How do I get an algebra morphism?
noncomputable example : TensorProduct R S A →ₐ[S] TensorProduct R S B := sorry

[Andrew Yang]

docs#Algebra.TensorProduct.map

[Dion Leijnse]

Thanks!