English
If an algebra homomorphism f is defined over a larger base ring S, and there is a tower of scalar actions R ≤ S, then f can be regarded as a nonunital R-algebra homomorphism by restricting scalars.
Русский
Если отображение \(f\) задано над большим основанием кольца, и есть каскад скаляров, то \(f\) можно рассматривать как неединичный гомоморфизм, ограничивая скаляры.
LaTeX
$$$f:A\\to_{S} B\\Rightarrow f:A\\to_{R} B\\text{ (ограничение скаляров)}$$$
Lean4
/-- If a monoid `R` acts on another monoid `S`, then a non-unital algebra homomorphism
over `S` can be viewed as a non-unital algebra homomorphism over `R`. -/
def restrictScalars (f : A →ₙₐ[S] B) : A →ₙₐ[R] B :=
{ (f : A →ₙ+* B) with map_smul' := fun r x ↦ by have := map_smul f (r • 1) x; simpa }
